Epsilon-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. The schema is for any given property of sets and states that, if for every set , the truth of follows from the truth of for all elements of , then this property holds for all sets. In symbols: Note that for the "bottom case" where denotes the empty set , the subexpression is vacuously true for all propositions and so that implication is proven by just proving . In words, if a property is persistent when collecting any sets with that property into a new set (and this also requires establishing the property for the empty set), then the property is simply true for all sets. Said differently, persistence of a property with respect to set formation suffices to reach each set in the domain of discourse. One may use the language of classes to express schemata. Denote the universal class by . Let be and use the informal as abbreviation for . The principle then says that for any , Here the quantifier ranges over all sets. In words this says that any class that contains all of its subsets is simply just the class of all sets. Assuming bounded separation, is a proper class. So the property is exhibited only by the proper class , and in particular by no set. Indeed, note that any set is a subset of itself and under some more assumptions, already the self-membership will be ruled out. For comparison to another property, note that for a class to be -transitive means There are many transitive sets - in particular the set theoretical ordinals. If is for some predicate , then with , 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 .