Help:FAQ/Questions about House Conventions

Questions about House Conventions

Definition or Statement of Equivalence

"Some concepts have many Definition pages: Definition 1, Definition 2, and so on.

Other concepts have few such pages, but instead implement a number of theorem-and-proof pages demonstrating that the concept is logically equivalent to another form of the concept, but do not actually express that other form as a definition.

Why are some logical equivalences implemented on $\mathsf{Pr} \infty \mathsf{fWiki}$ as actual alternative definitions, whereas others merely as a theorem-and-proof page?"

There are often many ways you can express a concept in an equivalent way. However, not all of these are "useful" as definitions, as such.

That is, in order to demonstrate that an object is an instance of a particular concept, it may be difficult, tedious or unwieldy to manipulate such an object into a form such that it can be used as a definition.

There can never be a consensus based on an intuitive "feel" for whether such a definition is suboptimally useful, so in order to decide whether to instantiate as a definition or an equivalence proof, we use the criterion:

Can this concept be found in a hard copy of a source work in this specific form?

If so, then implement it as a definition.

If not, then implement it as an equivalence theorem.

It is of course to be noted that if you do implement such a concept as a definition, then it is essential that there be an independent proof that this definition is equivalent to every other definition in the group of existing definitions to the concept.

That can of course be done by showing that it is equivalent to just one of those definitions, as there will already be such an equivalence proof demonstrating the existing definitions are all equivalent.

--prime mover (talk) 07:59, 23 June 2022 (UTC)