Well-founded relation

In mathematics is one of a quantity defined binary relation is well-founded if there is no infinite chains are in this relation, d. H. when there is no infinite sequence of elements in with for all . In particular, a well-founded relation does not contain any cycles. ${\displaystyle M}$ ${\displaystyle \prec }$ ${\displaystyle a_{0},a_{1},a_{2},a_{3},\dots }$ ${\displaystyle M}$ ${\displaystyle a_{i+1}\prec a_{i}}$ ${\displaystyle i}$

properties

Well-founded relations are always irreflexive .

Using the theorem of the excluded third party and the axiom of dependent choice , the following statements about are equivalent: ${\displaystyle {\prec }\subseteq M\times M}$

• ${\displaystyle \prec }$ is well founded.
• The transitive envelope of is well founded. ${\displaystyle \prec }$
• Every non-empty subset has a minimal element; H. one for which there is no with . ${\displaystyle X\subseteq M}$ ${\displaystyle a\in X}$ ${\displaystyle a'\in X}$ ${\displaystyle a'\prec a}$
• Well-founded induction over is a valid principle to prove statements about all elements of . ${\displaystyle \prec }$ ${\displaystyle M}$

Examples

• The predecessor relation to , defined by , is well founded. The induction principle that goes with it is that of complete induction . Its transitive envelope is the usual -relation with the associated induction principle of strong (complete) induction ; with classical logic equivalent to infinite descent . ${\displaystyle \mathbb {N} }$ ${\displaystyle n\prec m:\Longleftrightarrow n+1=m}$ ${\displaystyle \prec }$ ${\displaystyle <}$
• All well-founded orders and all well -founded relationships are well-founded relations if one only looks at the non-reflective part. The inversions do not apply, since well-founded relations do not have to be transitive.
• A model of the Zermelo-Fraenkel set theory defines a relation that is well-founded due to the axiom of foundation . The associated induction principle is called epsilon induction . ${\displaystyle V}$ ${\displaystyle \epsilon \subseteq V\times V}$

Relationships between the definitions

With the following definitions are possible for that it is well founded: ${\displaystyle {\prec }\subseteq M\times M}$ ${\displaystyle \prec }$

1. ${\displaystyle \prec }$is classically well-founded ( inhabited subsets have a minimal element) . ${\displaystyle M}$ ${\displaystyle \forall X\subseteq M.\ \forall x_{0}\in X.\ \exists x\in X.\ \forall y\in X.\ y\not \prec x}$
2. ${\displaystyle \prec }$is well-founded (well-founded induction is valid) . ${\displaystyle \forall X\subseteq M.\ (\forall x\in M.\ (\forall y\prec x.\ y\in X)\to x\in X)\to \forall x\in M.\ x\in X}$
3. Regarding there is no infinite descent (formulated relational) : . ${\displaystyle \prec }$ ${\displaystyle \lnot \exists X\subseteq M.\ \exists x_{0}\in X.\ \forall x\in X.\ \exists y\in X.\ y\prec x}$
4. Regarding there is no infinite descent : . ${\displaystyle \prec }$ ${\displaystyle \lnot \exists f\colon \mathbb {N} \to M.\ \forall n\in \mathbb {N} .\ f(n+1)\prec f(n)}$

Obviously, (1) and (3) are equivalent to each other when using classical logic.

Constructively can each member of the Implikationskette prove but the other direction generally not. ${\displaystyle (1)\implies (2)\implies (3)\implies (4)}$

${\displaystyle (4)\implies (3)}$requires an instance of the axiom of dependent choice .

For classical logic is needed, in a very strong sense: The existence of a classically well-founded relation and elements with already follows the law of the excluded . In this sense, the classical well-foundedness (1) is too strong for constructive mathematics. Since there are usually inhabited relations well-founded according to (2), classical logic implies . ${\displaystyle (3)\implies (1)}$ ${\displaystyle \prec }$ ${\displaystyle x,y}$ ${\displaystyle x\prec y}$ ${\displaystyle (3)\implies (1)}$

See also

• Descent function

literature

• Paul Taylor: Practical Foundations of Mathematics , Cambridge University Press, 1999, ISBN 0-521-63107-6 , pp. 97ff