{"history":[],"article":{"id":"8c849f1d-9953-47e4-a2e8-c809b72aca69","title":"Epsilon-induction","slug":"epsilon-induction","content":":::summary\n:::\n\n# \nIn [set theory](https://bliptext.com/articles/axiomatic-set-theory), **\\in-induction**, also called **epsilon-induction** or **set-induction**, is a principle that can be used to prove that all [sets](https://bliptext.com/articles/set-mathematics) satisfy a given property.\nConsidered as an [axiomatic principle](https://bliptext.com/articles/axiom-schema), it is called the **axiom schema of set induction**.\nThe principle implies [transfinite induction](https://bliptext.com/articles/transfinite-induction) and recursion.\nIt may also be studied in a general context of induction on [well-founded relations](https://bliptext.com/articles/well-founded-relation).\n\n# Statement\nThe schema is for any given property \\psi of sets and states that, if for every set x, the truth of \\psi(x) follows from the truth of \\psi [for all](https://bliptext.com/articles/for-all) elements of x, then this property \\psi holds [for all](https://bliptext.com/articles/for-all) sets.\nIn symbols:\nNote that for the \"bottom case\" where x denotes the [empty set](https://bliptext.com/articles/empty-set) \\{\\}, the subexpression is [vacuously true](https://bliptext.com/articles/vacuously-true) for all propositions and so that implication is proven by just proving \\psi(\\{\\}).\nIn words, if a property is persistent when collecting any sets with that property into a new set and is true for the empty set, then the property is simply true for all sets.\nSaid differently, persistence of a property with respect to set formation suffices to reach each set in the domain of discourse.\n\n## In terms of classes\nOne may use the language of classes to express schemata.\nDenote the universal [class](https://bliptext.com/articles/class-set-theory) by {\\mathbb U}.\nLet \\Psi be and use the informal as abbreviation for.\nThe principle then says that for any \\Psi,\nHere the quantifier ranges over all sets.\nIn words this says that any class that contains all of its subsets is simply just the class of all sets.\nAssuming [bounded separation](https://bliptext.com/articles/axiom-schema-of-predicative-separation), {\\mathbb U} is a proper class.\nSo the property is exhibited only by the proper class {\\mathbb U}, and in particular by no set.\nIndeed, note that any set is a subset of itself and under some more assumptions, already the self-membership will be ruled out.\nFor comparison to another property, note that for a class \\Sigma to be \\in-[transitive](https://bliptext.com/articles/transitive-set) means\nThere are many transitive sets - in particular the set theoretical [ordinals](https://bliptext.com/articles/ordinal-number).\n\n# Related notions of induction\nExportation proves.\nIf \\psi(x) is for some predicate P, it thus follows that\nwhere is defined as.\nIf \\Sigma is the universal class, then this is again just an instance of the schema.\nBut indeed if \\Sigma is any \\in-transitive class, then still and a version of set induction for P holds inside of \\Sigma.\n\n## Ordinals\nOrdinals may be defined as transitive sets of transitive sets.\nThe induction situation in the first infinite ordinal \\omega, the set of [natural numbers](https://bliptext.com/articles/set-theoretic-definition-of-natural-numbers), is discussed in more detail below.\nAs set induction allows for induction in transitive sets containing \\omega, this gives what is called [transfinite induction](https://bliptext.com/articles/transfinite-induction) and definition by transfinite recursion using, indeed, the whole [proper class](https://bliptext.com/articles/proper-class) of ordinals.\nWith ordinals, induction proves that all sets have ordinal rank and the rank of an ordinal is itself.\nThe theory of [Von Neumann ordinals](https://bliptext.com/articles/von-neumann-ordinal) describes such sets and, there, y\\in x models the order relation y < x, which classically is provably [trichotomous](https://bliptext.com/articles/law-of-trichotomy) and [total](https://bliptext.com/articles/total-relation).\nOf interest there is the successor operation that maps ordinals to ordinals.\nIn 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 \\in-well-founded.\n\n## Well-founded relations\nFor a binary relation R_D on a set D, [well-foundedness](https://bliptext.com/articles/well-founded-relation) can be defined by requiring a tailored induction property: y\\in x in the condition is abstracted to R_D(y, x), i.e. one always assumes in place of the intersection used in the statement above.\nIt can be shown that for a well-founded relation R_D, there are no infinite descending R_D-sequences and so also.\nFurther, function definition by recursion with R_D can be defined on their domains, and so on.\nClassically, well-foundedness of a relation on a set can also be characterized by the strong property of [minimal element existence for every subset](https://bliptext.com/articles/well-order).\nWith dependent choice, it can also be characterized by the weak property of non-existence of infinite descending chains.\n\n# For negative predicates\nThis section concerns the case of set induction and its consequences for predicates which are of a negated form,.\n[Constructively](https://bliptext.com/articles/intuitionistic-logic), the resulting statements are generally weaker than set induction for general predicates.\nTo establish equivalences, valid principles such as is commonly made use of, both sides saying that two predicates A and B can not, for any value, be validated simultaneously.\nThe situation when double-negation elimination is permitted is discussed in the section right after.\nDenoting the class by \\Sigma, this amounts to the special case of above with, for any x, P(x) equal to the false statement x\\neq x. One has denoting.\nWriting \\Sigma=\\{\\} for the statement that all sets are not members of the class \\Sigma, the induction schema reduces to In words, a property (a class) such that there is no \\in-minimal set for it is simply the false property (the empty set).\n(A minimal x for a relation R is one for which there does not exist another y with R(y, x). Here the membership relation restricted to \\Sigma is considered, i.e. a minimal element with respect to \\Sigma is one without a .)\n\n## Infinite descending chains\nThe [antecedent](https://bliptext.com/articles/antecedent-logic) in the above implication may be expressed as.\nIt holds for empty set [vacuously](https://bliptext.com/articles/vacuous-truth).\nIn the presence of any descending membership chain as a function on \\omega, the [axiom of replacement](https://bliptext.com/articles/axiom-of-replacement) proves existence of a set \\Sigma that also fulfills this.\nSo assuming the induction principle makes the existence of such a chain contradictory.\nIn this paragraph, assume the [axiom of dependent choice](https://bliptext.com/articles/axiom-of-dependent-choice) in place of the induction principle.\nAny consequences of the above antecedent is also implied by the -statement obtained by removing the double-negation, which constructively is a stronger condition.\nConsider a set \\Sigma with this -property.\nAssuming the set is [inhabited](https://bliptext.com/articles/inhabited-set), dependent choice implies the existence of an infinite descending membership chain as sequence, i.e. a function on the naturals.\nSo 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 \\Sigma=\\{\\}.\nSo set induction relates to the postulate of non-existence of infinite descending chains.\nBut given the extra assumptions required in the latter case, the mere non-existence postulate is relatively weak in comparison.\n\n### Self-membership\nFor a contradiction, assume there exists an inhabited set s with the particular property that it is equal to its own singleton set, s=\\{s\\}.\nFormally,, from which it follows that s\\in s, and also that all members of s share all its properties, e.g. . From the previous form of the principle it follow that s=\\{\\}, a contradiction.\nDiscussed using the other auxiliary terminologies above, one studies set induction for the class \\Psi of sets that are not equal to such an s. So in terms of the negated predicate, S(x) is the predicate x=s, meaning a set that exhibits S has the defining properties of s. Using the set builder notation, one is concerned with.\nAssuming the special property of s, any empty intersection statement simplifies to just s\\notin x. The principle in the formulation in terms of \\Sigma reduces to s\\notin s, again a contradiction.\nBack to the very original formulation, it is concluded that and \\Psi is simply the domain of all sets.\nIn a theory with set induction, a s with the described recursive property is not actually a set in the first place.\nA similar analysis may be applied also to more intricate scenarios.\nFor example, if u=\\{0,v\\} and v=\\{1,u\\} were both sets, then the inhabited \\{v,u\\} would exists by [pairing](https://bliptext.com/articles/axiom-of-pairing), but this also has the -property.\n\n## Contrapositive\nThe contrapositive of the form with negation is constructively even weaker but it is only one double negation elimination away from the regularity claim for \\Sigma,\nWith double-negations in antecedent and conclusion, the antecedent may equivalently be replaced with.\n\n# Classical equivalents\n\n## Disjunctive form\nThe excluded middle statement for a universally quantified predicate can classically be expressed as follows: Either it holds for all terms, or there exist a term for which the predicate fails\nWith this, using the disjunctive syllogism, ruling out the possibility of counter-examples classically proves a property for all terms.\nThis purely logical principle is unrelated to other relations between terms, such elementhood (or succession, see below).\nUsing that is classically an equivalence, and also using double-negation elimination, the induction principle can be translated to the following statement:\nThis expresses that, for any predicate P, either it holds for all sets, or there is some set x for which P does not hold while P is at the same time true for all elements of x. Relating it back to the original formulation: If one can, for any set x, prove that implies P(x), which includes a proof of the bottom case P(\\{\\}), then the failure case is ruled out and, then, by the [disjunctive syllogism](https://bliptext.com/articles/disjunctive-syllogism) the disjunct holds.\nFor the task of proving P 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.\n\n## Relation to regularity\nThe derivation in a previous section shows that set induction classically implies\nIn words, any property that is exhibited by some set is also exhibited by a \"minimal set\" x, as defined above.\nIn terms of classes, this states that every non-empty class \\Sigma has a member x that is disjoint from it.\nIn [first-order](https://bliptext.com/articles/list-of-first-order-theories) set theories, the common framework, the set induction principle is an axiom schema, granting an axiom for any predicate (i.e. class).\nIn contrast, the [axiom of regularity](https://bliptext.com/articles/axiom-of-regularity) is a single axiom, formulated with a universal quantifier only over elements of the domain of discourse, i.e. over sets.\nIf \\Sigma is a set and the induction schema is assumed, the above is the instance of the axiom of regularity for \\Sigma.\nHence, assuming set induction over a classical logic (i.e. assuming the [law of excluded middle](https://bliptext.com/articles/law-of-excluded-middle)), all instances of regularity hold.\nIn a context with an [axiom of separation](https://bliptext.com/articles/axiom-of-separation), regularity also implies excluded middle (for the predicates allowed in ones separation axiom).\nMeanwhile, the set induction schema does not imply excluded middle, while still being strong enough to imply strong induction principles, as discussed above.\nIn turn, the schema is, for example, adopted in the [constructive set theory](https://bliptext.com/articles/constructive-set-theory) CZF, which has type theoretic models.\nSo within such a set theory framework, set induction is a strong principle strictly weaker than regularity.\nWhen adopting the [axiom of regularity](https://bliptext.com/articles/axiom-of-regularity) and full Separation, C[ZF](https://bliptext.com/articles/zermelo-fraenkel-set-theory) equals standard [ZF](https://bliptext.com/articles/zermelo-fraenkel-set-theory).\n\n### History\nBecause of its use in the set theoretical treatment of ordinals, the axiom of regularity was formulated by [von Neumann](https://bliptext.com/articles/john-von-neumann) in 1925.\nIts motivation goes back to [Skolem](https://bliptext.com/articles/thoralf-skolem)'s 1922 discussion of infinite descending chains in [Zermelo set theory](https://bliptext.com/articles/zermelo-set-theory) {\\mathsf Z}, a theory without regularity or replacement.\nThe theory {\\mathsf Z} does not prove all set induction instances.\nRegularity is classically equivalent to the contrapositive of set induction for negated statements, as demonstrated.\nThe bridge from sets back to classes is demonstrated below.\n\n### Set induction from regularity and transitive sets\nAssuming regularity, one may use classical principles, like the reversal of a contrapositive.\nMoreover, an induction schema stated in terms of a negated predicate \\neg S is then just as strong as one in terms of a predicate variable P, as the latter simply equals.\nAs 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 \\Sigma.\nIt works in the end because the [axiom of separation](https://bliptext.com/articles/axiom-of-separation) allows for intersection between sets and classes.\nRegularity only concerns intersection inside a set and this can be flattened using transitive sets.\nThe proof is by manipulation of the regularity axiom instance\nfor a particular subset of the class \\Sigma.\nObserve that given a class \\Sigma and any transitive set t, one may define which has and also.\nWith this, the set s may always be replaced with the class \\Sigma in the conclusion of the regularity instance.\nThe 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.\nSo assume there is some z\\in\\Sigma, together with the existence of some transitive set t that has z as subset.\nAn intersection s_z may be constructed as described and it also has.\nConsider excluded middle for whether or not t is disjoint from \\Sigma, i.e. s_z=\\{\\}.\nIf s_z is empty, then also and x=z itself always fulfills the principle.\nOtherwise, by regularity and one can proceed to manipulate the statement by replacing s_z with \\Sigma as discussed.\nIn this case, one even obtains a slightly stronger statement than the one in the previous section, since it carries the sharper information that x\\in s_z and not just x\\in\\Sigma.\n\n### Transitive set existence\nThe proof above assumes the existence of some transitive set containing any given set.\nThis may be postulated, the transitive containment axiom.\nExistence of the stronger [transitive closure](https://bliptext.com/articles/transitive-set) with respect to membership, for any set, can also be derived from some stronger standard axioms.\nThis needs the [axiom of infinity](https://bliptext.com/articles/axiom-of-infinity) for \\omega as a set, recursive functions on \\omega, the [axiom of replacement](https://bliptext.com/articles/axiom-of-replacement) on \\omega and finally the [axiom of union](https://bliptext.com/articles/axiom-of-union).\nI.e. it needs many standard axioms, just sparing the [axiom of powerset](https://bliptext.com/articles/axiom-of-powerset).\nIn a context without strong separation, suitable function space principles may have to be adopted to enable recursive function definition.\nminus infinity also only proves the existence of transitive closures when [Regularity](https://bliptext.com/articles/axiom-of-foundation) is promoted to Set induction.\n\n# Comparison of epsilon and natural number induction\nThe transitive [von Neumann model](https://bliptext.com/articles/set-theoretic-definition-of-natural-numbers) \\omega of the [standard](https://bliptext.com/articles/non-standard-model-of-arithmetic) natural numbers is the first infinite ordinal.\nThere, the binary membership relation \"\\in\" of set theory exactly models the strict ordering of natural numbers \"<\".\nThen, the principle derived from set induction is [complete induction](https://bliptext.com/articles/mathematical-induction).\nIn this section, quantifiers are understood to range over the domain of [first-order Peano arithmetic](https://bliptext.com/articles/peano-axioms) (or [Heyting arithmetic](https://bliptext.com/articles/heyting-arithmetic) ).\nThe [signature](https://bliptext.com/articles/signature-logic) includes the constant symbol \"0\", the successor function symbol \"S\" and the addition and multiplication function symbols \"+\" resp \"*\".\nWith it, the naturals form a [semiring](https://bliptext.com/articles/semiring), which always come with a canonical non-strict preorder \"\\le\", and the [irreflexive](https://bliptext.com/articles/irreflexive) < may be defined in terms of that.\nSimilarly, the binary ordering relation k < n is also definable as.\nFor any predicate Q, the complete induction principle reads\nMaking use of, the principle is already implied by [standard form of the mathematical induction schema](https://bliptext.com/articles/mathematical-induction).\nThe latter is expressed not in terms of the decidable order relation \"<\" but the primitive symbols,\nLastly, a statement may be proven that merely makes use of the successor symbol and still mirrors set induction: Define a new predicate as.\nIt holds for zero by design and so, akin to the bottom case in set induction, the implication is equivalent to just Q(0).\nUsing induction, proves that every n is either zero or has a computable unique predecessor, a q with Sq = n. Hence.\nWhen n is the successor of n-1, then expresses Q(n-1).\nBy case analysis, one obtains\n\n## Classical equivalents\nUsing the classical principles mentioned above, the above may be expressed as It expresses that, for any predicate Q, either Q hold for all numbers, or there is some natural number n for which Q does not hold despite Q holding for all predecessors.\nInstead of, one may also use and obtain a related statement.\nIt constrains the task of ruling out counter-examples for a property of natural numbers: If the bottom case Q(0) is validated and one can prove, for any number n, that the property Q is always passed on to Sn, then this already rules out a failure case.\nMoreover, if a failure case exists, one can use the [least number principle](https://bliptext.com/articles/least-number-principle) to even prove the existence of a minimal such failure case.\n\n## Least number principle\nAs in the set theory case, one may consider induction for negated predicates and take the contrapositive.\nAfter use of a few classical logical equivalences, one obtains a conditional existence claim.\nLet \\Theta denote the set of natural numbers validating a property T. In the Neumann model, a natural number n is extensionally equal to, the set of numbers smaller than n. The [least number principle](https://bliptext.com/articles/least-number-principle), obtained from complete induction, here expressed in terms of sets, reads\nIn words, if it cannot be ruled out that some number has the property T, then it can also not be consistently ruled out that a least such number n exists.\nIn classical terms, if there is any number validating T, then there also exists a least such number validating T. Least here means that no other number k