Rel, bicategory of relations, allegory
left and right euclidean;
extensional, well-founded relations.
A (binary) relation on a set is called well-founded if it is valid to do induction on over .
Let be a set, and let be a binary relation on . A subset of is -inductive if
The relation is well-founded if the only -inductive subset of is itself.
Note that this is precisely what is necessary to validate induction over : if we can show that a statement is true of an element of whenever it is true of everything that precedes () , then it must be true of everything in . In the presence of excluded middle it is equivalent to other commonly stated definitions; see Formulations in classical logic below.
While the definition above follows how a well-founded relation is generally used (namely, to prove properties of elements of by induction), it is complicated. Two alternative formulations are given by the following:
The relation has no infinite descent (usually attributed to Pierre de Fermat) if there exists no sequence in . (Such a sequence is called an infinite descending sequence.)
The relation is classically well-founded if every inhabited subset of has a member such that no satisfies . (Such an is called a minimal element of .)
In classical mathematics, both of these conditions are equivalent to being well-founded. In constructive mathematics, we may prove that a well-founded relation has no infinite descent (see Proposition ), but not the converse, and that a classically well-founded relation is well-founded (see Proposition ), but not the converse.
The classical notion of well-foundedness enforces classical logic onto us, in the following sense.
If is an inhabited well-founded relation in a classical sense, then the unrestricted law of excluded middle holds.
For a topos-theoretic proof see here.
Suppose there are and such that , and let be an arbitrary proposition. Consider then a set defined as . Clearly, the set is inhabited, thus by classical well-foundedness it has a minimal element . By intuitionistic reasoning, either is in , i.e. , or , i.e. . In the latter case we immediately see that holds. So, suppose that is the minimal element of ; we will show that holds. For suppose that holds; then and , violating the condition that is a minimal element of .
Since was an arbitrary proposition, we can deduce .
We note that classical well-foundedness is really too strong for constructive (i.e., intuitionistic) mathematics, due to Proposition . On the other hand, the infinite descent condition is too weak to be of much use in constructive mathematics. It is the inductive notion of well-foundedness that is just right.
Note however that in predicative mathematics, the definition of well-founded may be impossible to even state, and so either of these alternative definitions would be preferable, provided classical logic is used.
Even in constructive predicative mathematics, (1) is strong enough to establish the Burali-Forti paradox (when applied to linear orders). In material set theory, (2) is traditionally used to state the axiom of foundation, although the impredicative definition could also be used as an axiom scheme (and must be in constructive versions). In any case, either (1) or (2) is usually preferred by classical mathematicians as simpler.
To round out the discussion we prove the following two results, both valid in intuitionistic mathematics:
If is a well-founded relation and has no minimal element, then is empty.
This result makes it trivial to infer (under classical logic) that classical well-foundedness is a consequence of well-foundedness. It also shows that well-foundedness rules out infinite descent (intuitionistically), since an infinite descent sequence has no minimal element.
Let . Clearly . We show is inductive, so that under well-foundedness and , as desired.
So, suppose is an element such that whenever . We must show . Claim: . For if , then would be a minimal element of (as ). But this negates the assumption that has no minimal element.
Thus , and , so that . This completes the proof.
In intuitionistic set theory, classical well-foundedness implies (inductive) well-foundedness.
Let be a classically well-founded relation on , and let be an inductive subset. We must show that every element belongs to . Since is inductive, it suffices to show that every belongs to , i.e. we may assume given a such that and show . But under this assumption we have that is inhabited, so according to Remark , the law of excluded middle follows and we might as well then argue classically. The argument is well-known but we include it for completeness: under classical well-foundedness, if an inductive subset is not the entirety of , then the complement has a minimal element . In that case, implies , but then since is inductive, contradiction. Hence and in particular , which is what we wanted.
To bring us full circle: in classical set theory we may prove that if has no infinite descent, then is classically well-founded. For suppose an inhabited subset (say with an element ) failed to have a least element. Then we can find an infinite descent sequence with , by choosing at each stage such that . Technically this requires the use of dependent choice, but generally this is felt to be a mild choice principle (that is true even for intuitionistic mathematics).
Many inductive or recursive notions may also be packaged in coalgebraic terms. For the concept of well-founded relation, first observe that a binary relation on a set is the same as a coalgebra structure for the covariant power-set endofunctor on , where if and only if .
In this language, a subset is -inductive, or -inductive, if in the pullback
the map factors through . (Note that is necessarily monic, since preserves monos.) Unpacking this a bit: for any , if belongs to , that is if , then . This says the same thing as .
Then, as usual, the -coalgebra is well-founded if every -inductive subset is all of .
Other relevant notions may also be packaged; for example, the -coalgebra is extensional if is monic. See also well-founded coalgebra.
Given two sets and , each equipped with a well-founded relation , a function is a simulation of in if
whenever and
given , there exists with .
Then sets so equipped form a category with simulations as morphisms. See extensional relation for more uses of simulations.
For example, a simulation between two well-ordered sets is an isomorphism of onto an initial segment of .
In coalgebraic language, a simulation is simply a -coalgebra homomorphism . Condition (1), that is merely -preserving, translates to the condition that is a colax morphism of coalgebras, in the sense that there is an inclusion
If is well-founded and is (weakly) extensional, then there is at most one simulation .
It is enough to show that if are -coalgebra morphisms, then is an inductive subset. Suppose is an element such that whenever . Then ; since are -coalgebra maps, this is the same as the equality . By extensionality, we infer , so that . Thus is inductive.
Every well-founded relation is irreflexive; that is, . Sometimes one wants a reflexive version of a well-founded relation; let if and only or . Then the requirement that be a minimal element of a subset states that only if . But infinite descent or direct proof by induction still require rather than .
A well order may be defined as a well-founded linear order, or alternatively as a transitive, extensional, well-founded relation.
A well-quasi-order is a well-founded preorder (referring to the reflexive version of well-foundedness above) that in addition has no infinite antichains.
The axiom of foundation in material set theory states precisely that the membership relation on the proper class of all pure sets is well-founded. In structural set theory, accordingly, one uses well-founded relations in building structural models of well-founded pure sets.
Let be a finite set. Then any relation on whose transitive closure is irreflexive is well-founded.
Let be the set of natural numbers, and let if is the successor of : . That this relation is well-founded is the usual principle of mathematical induction.
Again let be the set of natural numbers, but now let if in the usual order. That this relation is well-founded is the principle of strong induction.
More generally, let be a set of ordinal numbers (or even the proper class of all ordinal numbers), and let if in the usual order. That this relation is well-founded is the principle of transfinite induction.
Similarly, let be a set of pure sets (or even the proper class of all pure sets), and let if . That this relation is well-founded is the axiom of foundation.
Let be the set of integers, and let mean that properly divides : is an integer other than . This relation is also well-founded, so one can prove properties of integers by induction on their proper divisors.
Last revised on August 10, 2018 at 13:45:31. See the history of this page for a list of all contributions to it.