Epsilon-induction

Kind of transfinite induction
In set theory, 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. The principle implies transfinite induction and recursion. It may also be studied in a general context of induction on well founded relations.

Exportation proves If is for some predicate , it thus follows that

where is defined as
If is the universal class, then this is again just an instance of the schema. But indeed if is any transitive class, then still and a version of set induction for holds inside of .

Ordinals may be defined as transitive sets of transitive sets. The induction situation in the first infinite ordinal , the set of natural numbers, is discussed in more detail below. As set induction allows for induction in transitive sets containing , this gives what is called transfinite induction and definition by transfinite recursion using, indeed, the whole proper class of ordinals. With ordinals, induction proves that all sets have ordinal rank and the rank of an ordinal is itself. The theory of Von Neumann ordinals describes such sets and, there, models the order relation , which classically is provably trichotomous and total. Of interest there is the successor operation that maps ordinals to ordinals. 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.) The sets are well founded.

For a binary relation on a set , well foundedness can be defined by requiring a tailored induction property: in the condition is abstracted to , i. e. one always assumes in place of the intersection used in the statement above. It can be shown that for a well founded relation , there are no infinite descending sequences and so also Further, function definition by recursion with can be defined on their domains, and so on. 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.

The antecedent in the above implication may be expressed as It holds for empty set vacuously. In the presence of any descending membership chain as a function on , the axiom of replacement proves existence of a set that also fulfills this. So assuming the induction principle makes the existence of such a chain contradictory. In this paragraph, assume the axiom of dependent choice in place of the induction principle. Any consequences of the above antecedent is also implied by the statement obtained by removing the double negation, which constructively is a stronger condition. Consider a set with this property. Assuming the set is inhabited, dependent choice implies the existence of an infinite descending membership chain as sequence, i. e. a function on the naturals. So establishing (or even postulating) the non existence of such a chain for a set with the property implies the assumption was wrong, i. e. also
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.

For a contradiction, assume there exists an inhabited set with the particular property that it is equal to its own singleton set, Formally, , from which it follows that , and also that all members of share all its properties, e. g. From the previous form of the principle it follow that , a contradiction. Discussed using the other auxiliary terminologies above, one studies set induction for the class of sets that are not equal to such an So in terms of the negated predicate, is the predicate , meaning a set that exhibits has the defining properties of Using the set builder notation, one is concerned with Assuming the special property of , any empty intersection statement simplifies to just The principle in the formulation in terms of reduces to , again a contradiction. Back to the very original formulation, it is concluded that and is simply the domain of all sets. In a theory with set induction, a with the described recursive property is not actually a set in the first place. A similar analysis may be applied also to more intricate scenarios. For example, if and were both sets, then the inhabited would exists by pairing, but this also has the property.

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 , a theory without regularity or replacement. The theory does not prove all set induction instances. Regularity is classically equivalent to the contrapositive of set induction for negated statements, as demonstrated. The bridge from sets back to classes is demonstrated below.

The proof above assumes the existence of some transitive set containing any given set. This may be postulated, the transitive containment axiom. Existence of the stronger transitive closure with respect to membership, for any set, can also be derived from some stronger standard axioms. This needs the axiom of infinity for as a set, recursive functions on , the axiom of replacement on and finally the axiom of union. I. e. it needs many standard axioms, just sparing the axiom of powerset. In a context without strong separation, suitable function space principles may have to be adopted to enable recursive function definition. minus infinity also only proves the existence of transitive closures when Regularity is promoted to Set induction.