-induction, also called epsilon-induction or set-induction, is a principle that can be used to prove that all sets satisfy a given property.
Considered as an axiomatic principle, it is called the axiom schema of set induction.
In the classical case, the induction step for successor ordinals can be simplified so that a property must merely be preserved between successive ordinals (this is the formulation that is typically understood as transfinite induction.)
Classically, well-foundedness of a relation on a set can also be characterized by the strong property of minimal element existence for every subset.
With dependent choice, it can also be characterized by the weak property of non-existence of infinite descending chains.
This section concerns the case of set induction and its consequences for predicates which are of a negated form,
To establish equivalences, valid principles such as is commonly made use of, both sides saying that two predicates
In this paragraph, assume the axiom of dependent choice in place of the induction principle.
Assuming the set is inhabited, dependent choice implies the existence of an infinite descending membership chain as sequence, i.e. a function
So set induction relates to the postulate of non-existence of infinite descending chains.
But given the extra assumptions required in the latter case, the mere non-existence postulate is relatively weak in comparison.
This purely logical principle is unrelated to other relations between terms, such elementhood (or succession, see below).
is classically an equivalence, and also using double-negation elimination, the induction principle can be translated to the following statement: This expresses that, for any predicate
by ruling out the existence of counter-examples, the induction principle thus plays a similar role as the excluded middle disjunction, but the former is commonly also adopted in constructive frameworks.
In turn, the schema is, for example, adopted in the constructive set theory CZF, which has type theoretic models.
When adopting the axiom of regularity and full Separation, CZF equals standard ZF.
Because of its use in the set theoretical treatment of ordinals, the axiom of regularity was formulated by von Neumann in 1925.
Its motivation goes back to Skolem's 1922 discussion of infinite descending chains in Zermelo set theory
Regularity is classically equivalent to the contrapositive of set induction for negated statements, as demonstrated.
As the equivalences with the contrapositive of set induction have been discussed, the task is to translate regularity back to a statement about a general class
It works in the end because the axiom of separation allows for intersection between sets and classes.
The remaining aim is to obtain a statement that also has it replaced in the antecedent, that is, establish the principle holds when assuming the more general
In this case, one even obtains a slightly stronger statement than the one in the previous section, since it carries the sharper information that
minus infinity also only proves the existence of transitive closures when Regularity is promoted to Set induction.
In this section, quantifiers are understood to range over the domain of first-order Peano arithmetic
, the principle is already implied by standard form of the mathematical induction schema.
It holds for zero by design and so, akin to the bottom case in set induction, the implication
It constrains the task of ruling out counter-examples for a property of natural numbers: If the bottom case
As in the set theory case, one may consider induction for negated predicates and take the contrapositive.
Moreover, adopting Markov's principle in arithmetic allows removal of double-negation for decidable