Epsilon-induction

In mathematics, ${\displaystyle \in }$-induction (epsilon-induction or set-induction) is a variant of transfinite induction.

Considered as a set theory axiom schema, it is called the Axiom schema of set induction.

It can be used in set theory to prove that all sets satisfy a given property. This is a special case of well-founded induction.

Statement[]

It states, for any given property ${\displaystyle \Phi }$, that if for every set ${\displaystyle x}$, the truth of ${\displaystyle \Phi (x)}$ follows from the truth of ${\displaystyle \Phi }$ for all elements of ${\displaystyle x}$, then this property ${\displaystyle \Phi }$ holds for all sets. In symbols:

${\displaystyle \forall x.{\Big (}\left(\forall y\in x.\Phi (y)\right)\rightarrow \Phi (x){\Big )}\ \rightarrow \ \forall z.\Phi (z)}$

Note that for the "bottom case" where ${\displaystyle x}$ denotes the empty set, the subexpression ${\displaystyle \forall y\in x.\Phi (y)}$ is vacuously true for all propositions.

Comparison with natural number induction[]

The above can be compared with ${\displaystyle \omega }$-induction over the natural numbers ${\displaystyle n\in \{0,1,2,\dots \}}$ for number properties ${\displaystyle \phi }$. This may be expressed as

${\displaystyle {\Big (}\phi (0)\land \forall n.(\phi (n)\to \phi (n+1)){\Big )}\ \to \ \forall m.\phi (m)}$

or, using the symbol for the tautologically true statement, ${\displaystyle \top }$,

${\displaystyle {\Big (}(\top \to \phi (0))\land \forall n.(\phi (n)\to \phi (n+1)){\Big )}\ \to \ \forall m.\phi (m)}$

Fix a predicate ${\displaystyle Q}$ and define a new predicate equivalent to ${\displaystyle Q}$, except with an argument offset by one and equal to ${\displaystyle \top }$ for ${\displaystyle n=0}$. With this we can also get a statement equivalent to induction for ${\displaystyle Q}$, but without a conjunction. By abuse of notation, letting "${\displaystyle Q(-1)}$" denote ${\displaystyle \top }$, an instance of the ${\displaystyle \omega }$-induction schema may thus be expressed as

${\displaystyle \forall n.{\Big (}Q(n-1)\to Q(n){\Big )}\ \to \ \forall m.Q(m)}$

This now mirrors an instance of the Set-Induction schema.

Conversely, Set-Induction may also be treated in a way that treats the bottom case explicitly.

Classical equivalents[]

With classical tautologies such as ${\displaystyle (A\to B)\iff (\neg A\lor B)}$ and ${\displaystyle (\neg A\lor B)\iff \neg (A\land \neg B)}$, an instance of the ${\displaystyle \omega }$-induction principle can be translated to the following statement:

${\displaystyle \exists n.{\Big (}Q(n-1)\land \neg Q(n){\Big )}\ \lor \ \forall m.Q(m)}$

This expresses that, for any property ${\displaystyle Q}$, either there is any (first) number ${\displaystyle n}$ for which ${\displaystyle Q}$ does not hold, despite ${\displaystyle Q}$ holding for the preceding case, or - if there is no such failure case - ${\displaystyle Q}$ is true for all numbers.

Accordingly, in classical ZF, an instance of the set-induction can be translated to the following statement, clarifying what form of counter-example prevents a set-property ${\displaystyle P}$ to hold for all sets:

${\displaystyle \exists x.{\Big (}\left(\forall y\in x.P(y)\right)\,\land \,\neg P(x){\Big )}\ \lor \ \forall z\,P(z)}$

This expresses that, for any property ${\displaystyle P}$, either there a set ${\displaystyle x}$ for which ${\displaystyle P}$ does not hold while ${\displaystyle P}$ being true for all elements of ${\displaystyle x}$, or ${\displaystyle P}$ holds for all sets. For any property, if one can prove that ${\displaystyle \forall y\in x.P(y)}$ implies ${\displaystyle P(x)}$, then the failure case is ruled out and the formula states that the disjunct ${\displaystyle \forall z.P(z)}$ must hold.

Independence[]

In the context of the constructive set theory CZF, adopting the Axiom of regularity would imply the law of excluded middle and also set-induction. But then the resulting theory would be standard ZF. However, conversely, the set-induction implies neither of the two. In other words, with a constructive logic framework, set-induction as stated above is strictly weaker than regularity.

See also[]

• Mathematical induction
• Transfinite induction
• Well-founded induction
• Constructive set theory
• Non-well-founded set theory