∈-induction
   HOME

TheInfoList



OR:

In set theory, \in-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.


Statement

The 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 elements of x, then this property \psi holds for all sets. In symbols: :\forall x. \Big(\big(\forall (y \in x). \psi(y)\big)\,\to\,\psi(x)\Big)\,\to\,\forall z. \psi(z) Note that for the "bottom case" where x denotes the
empty set In mathematics, the empty set is the unique set having no elements; its size or cardinality (count of elements in a set) is zero. Some axiomatic set theories ensure that the empty set exists by including an axiom of empty set, while in other ...
\, the subexpression \forall(y\in x).\psi(y) is vacuously true for all propositions and so that implication is proven by just proving \psi(\). 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.


In terms of classes

One may use the language of classes to express schemata. Denote the universal
class Class or The Class may refer to: Common uses not otherwise categorized * Class (biology), a taxonomic rank * Class (knowledge representation), a collection of individuals or objects * Class (philosophy), an analytical concept used differentl ...
\ by . Let \Psi be \ and use the informal \Psi= as abbreviation for \forall z. z\in\Psi. The principle then says that for any \psi, :\forall (x\subseteq \Psi). x\in \Psi\,\,\leftrightarrow\,\,\Psi= 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 \forall (x\subseteq \Psi). x\in \Psi 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-memberhship will be ruled out. For comparison to another property, note that for a class \Sigma to be \in- transitive means :\forall (x\in \Sigma). x\subseteq\Sigma There are many transitive sets - in particular the set theoretical ordinals.


Related notions of induction

If \psi(x) is (x\in\Sigma)\to P(x) for some predicate P, then with (A\to(B\to C))\leftrightarrow(B\to(A\to C)), :\forall (x\in\Sigma). \Big(\big(\forall (y \in (x\cap\Sigma)). P(y)\big)\,\to\,P(x)\Big)\,\to\,\forall (z\in\Sigma). P(z) where y\in(x\cap\Sigma) defined as y\in x\land y\in\Sigma. If \Sigma is the universal class, then this is again just an instance of the schema. But indeed if \Sigma is any \in-transitive class, then still \forall(x\in\Sigma).(x\cap\Sigma=x) and a version of set induction for P holds inside of \Sigma.


Ordinals

Ordinals may be defined as transitive sets of transitive sets. The induction situation in the first infinite ordinal \omega, the set of
natural numbers In mathematics, the natural numbers are those numbers used for counting (as in "there are ''six'' coins on the table") and ordering (as in "this is the ''third'' largest city in the country"). Numbers used for counting are called ''cardinal n ...
, is discussed in more detail below. As set induction allows for induction in transitive sets containing \omega, this gives what is called transfinite induction and definition by transfinite recursion using, indeed, the whole
proper class Proper may refer to: Mathematics * Proper map, in topology, a property of continuous function between topological spaces, if inverse images of compact subsets are compact * Proper morphism, in algebraic geometry, an analogue of a proper map for ...
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 ordinal In set theory, an ordinal number, or ordinal, is a generalization of ordinal numerals (first, second, th, etc.) aimed to extend enumeration to infinite sets. A finite set can be enumerated by successively labeling each element with the least n ...
s describes such sets and, there, y\in x models the order relation y < x, which ''classically'' is provably trichotomous and
total Total may refer to: Mathematics * Total, the summation of a set of numbers * Total order, a partial order without incomparable pairs * Total relation, which may also mean ** connected relation (a binary relation in which any two elements are comp ...
. Of interest there is the successor operation x\mapsto x\cup\ 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 \in-well-founded.


Well-founded relations

For a binary relation R_D on a set D, well-foundedness 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 R_D(y, x)\land y\in D in place of the intersection y\in(x\cap D) used in the statement above. It can be shown that for a well-founded relation R_D, there are no infinite descending R_D-sequences and so also \forall y.\neg R_D(y, y). Further, function definition by recursion with R_D 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, or, with dependent choice, by the weak property of non-existence of infinite descending chains.


Constructively weaker forms of set induction


Negated predicates

Consider set induction for \psi(x) a negated predicate \neg S(x). Denoting 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. With y\in(x\cap\Sigma) defined as y\in x \land y\in \Sigma, one has x\cap \Sigma=\ denoting \neg\exists(y\in\Sigma).y\in x. Writing \Sigma=\ for the statement that all sets are not members of the class \Sigma, one now finds :\forall(x\in\Sigma).x\cap \Sigma\neq\\,\to\,\Sigma=\ Consider the equivalence of separation statements :\forall x.\big(A(x)\to \neg B(x)\big)\,\leftrightarrow\,\neg \exists x.\big(A(x)\land B(x)\big), both saying that two predicates A and B can not, for any value, be validated simultaneously. Applied to the antecedent, we may write :\neg\exists(x\in\Sigma). x\cap \Sigma=\\,\to\,\Sigma=\ In words, a property such that there is no \in-minimal set for it is simply false for all sets. (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 y\in(x\cap \Sigma).)


Consequences

Lifting one double negation in the antecedent above, one finds the antecedent is certainly implied by the stronger \forall\exists-statement \forall(x\in\Sigma). \exists (y\in\Sigma). y\in x.


Infinite descending chains

Consider a context with dependent choice and a ''set'' \Sigma with the \forall\exists-property. Assuming the set is inhabited implies the existence of an infinite descending membership chain as sequence, i.e. a function on the naturals. So establishing the non-existence of such a chain implies \Sigma=\. Given the extra assumptions, the postulate of mere non-existence of infinite descending chains is relatively weak compared to set induction. For the other direction, note that in the presence of any such membership chain function, the axiom of replacement proves existence of a set \Sigma that fulfills the \forall\exists-property. So assuming the induction principle makes the chain existence contradictory also.


Self-membership

For a contradiction, assume there exists an ''inhabited'' set s with a particular property introduced below. One studies set induction for the class \Psi of sets that are not equal to s. 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. Characterized another way, \Sigma is the inhabited singleton set \. The peculiar property shall be that s is equal to its own singleton set, i.e. \forall y. (y\in s\leftrightarrow y=s). It follows that s\in s and any set contained in s also contains s, i.e. \forall (y\in s). s\in y. By the previous form of the principle it follow that s=\, a contradiction. Seen differently, any empty intersection statement x\cap s=\ simplifies to just x\notin s but used in the principle this does not go together with s\in s. Either way, \neg\exists s.s=\. It is concluded that \forall z.z\neq s and \Psi is simply the domain of all sets, also without any choice. In a theory with set induction, a s with the described recursive property is not actually a set in the first place.


Contrapositive

For a general predicate instance P of the set induction schema, taking the contrapositive reads :\neg \forall z.P(z)\,\to\,\neg\forall x.\Big(\big(\forall (y \in x). P(y)\big)\,\to\, P(x)\Big) The 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, :\Sigma\neq \\,\to\,\neg\neg\exists(x\in\Sigma). x\cap \Sigma=\ One may also obtain a further weakened principle by strengthening the assumption \Sigma\neq \ to \exists z.(z\in \Sigma).


Classical equivalents


Relation to regularity

Classically, the above shows that set induction implies :\Sigma\neq\\,\to\,\exists(x\in \Sigma). x\cap \Sigma=\ In words, any property that is exhibited by some set is also exhibited by a "minimal set", as defined above. In terms of classes, this states that every non-empty class \Sigma has a member x that is disjoint from it. If \Sigma is a set, this is the instance of the axiom of regularity for \Sigma. In a context with an axiom of separation, regularity also implies the law of excluded middle. Meanwhile, the set induction schema does not. In turn, the schema is, for example, adopted in the constructive set theory CZF. Within such a framework, set induction is a strong principle strictly weaker than regularity. When adopting the axiom of regularity and full Separation, CZF equals standard ZF.


History

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 Thoralf Albert Skolem (; 23 May 1887 – 23 March 1963) was a Norwegian mathematician who worked in mathematical logic and set theory. Life Although Skolem's father was a primary school teacher, most of his extended family were farmers. 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.


Set induction from regularity and transitive sets

Assuming regularity, one may use classical principles, like the reversal of a contrapositive. Moreover, 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 \neg(\neg P). 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 \Sigma. It works because the axiom of separation allows for intersection between sets and classes. Regularity only concerns intersection ''inside'' a set and this can be flattened using transitive sets. So observe that given a \Sigma and any transitive set t, one may define s=t\cap\Sigma which has x\in s\to (x\in\Sigma\land x\subseteq t). Combining this with (x\subseteq t)\to (x\cap s = x\cap \Sigma), the proof is by manipulation of the regularity statement for the subset s\subseteq\Sigma of the class \Sigma: The set s may be replaced with the class \Sigma in its conclusion. The aim is to obtain a statement that also has it replaced in the antecedent. So assume there is some z\in\Sigma together with a transitive set that has z as subset. An intersection s_z may be constructed as described and it also has (z\cap\Sigma)\subseteq s_z. Consider excluded middle for whether or not t is disjoint from \Sigma, i.e. s_z=\. If s_z is empty, then also z\cap\Sigma=\ and x=z itself fulfills the principle. Otherwise, \exists(x\in s_z) by regularity and one can proceed to manipulate the statement by replacing s_z with \Sigma as discussed. In this case, one even obtaines 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.


Transitive set existence

The existence of the required transitive sets can 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 \omega as a set, recursive functions on \omega, the axiom of replacement on \omega and finally the axiom of union. I.e. it needs many standard axioms, just sparing the
axiom of powerset In mathematics, the axiom of power set is one of the Zermelo–Fraenkel axioms of axiomatic set theory. In the formal language of the Zermelo–Fraenkel axioms, the axiom reads: :\forall x \, \exists y \, \forall z \, \in y \iff \forall w \ ...
. In a context without strong separation, suitable function space principles may have to be adopted to enable recursive function definition.


Forms without implication

Using (A\to B)\leftrightarrow(B\lor\neg A) and double-negation elimination, the contrapositive can be further translated to the following statement: :\exists x. \Big(\big(\forall(y\in x). P(y)\big)\,\land\,\neg P(x)\Big)\,\lor\,\forall z. P(z) This expresses that, for any predicate P, either there is some set x for which P does not hold while P being true for all elements of x, or the predicate P holds for all sets. Relating it back to the original formulation: If one can, for any set x, prove that \forall(y\in x).P(y) 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 the disjunct \forall z. P(z) holds.


As refinement of excluded middle

The excluded middle for predicates can be expressed as follows: Either there exist a term for which a predicate fails, or it holds for all terms :\exists x.\neg P(x)\,\lor\,\forall z. P(z) With this, using the disjunctive syllogism, ruling out the possibility of counter-examples classically proves a property for all terms. This purely logical principle is unrelated to other relations between terms, such elementhood (or succession, see below). The induction principle is a stronger tool for the task of proving P by ruling out the existence of counter-examples, and it is one often also adopted in constructive frameworks.


Comparison of epsilon and natural number induction

The transitive
von Neumann model The von Neumann architecture — also known as the von Neumann model or Princeton architecture — is a computer architecture based on a 1945 description by John von Neumann, and by others, in the ''First Draft of a Report on the EDVAC''. The ...
\omega of the standard natural numbers is the first infinite ordinal. There, the binary membership relation "\in" of set theory exactly models the ordering of natural numbers "<". Then, the principle derived from set induction complete induction. In this section, quantifiers are understood to range over the domain of first-order Peano arithmetic , a theory with a signature including the constant symbol "0", the successor function symbol "S" and the addition function symbol "+". Here the binary ordering relation k < n is, for example, definable as \exists m. k + Sm = n. For any predicate Q, the principle reads :\forall n. \Big(\big(\forall (k < n). Q(k)\big)\,\to\,Q(n)\Big)\,\to\,\forall m. Q(m) Making use of :\big(\forall (k < Sn). Q(k)\big)\,\,\leftrightarrow\,\,\big(\forall (k < n). Q(k)\big)\land Q(n), complete induction is already implied by standard form of the mathematical induction schema. The latter is expressed not in terms of the decidable order relation "<" but the primitive symbols, :\Big(\phi(0)\,\land\,\forall n.\big(\phi(n)\,\to\,\phi(Sn)\big)\Big)\,\to\,\forall m. \phi(m) Abstracting away the signature symbols, this can be demonstrated to still be close to set induction: Using induction, proves that every n is either zero or has a computable unique predecessor p with n = Sp. Define a new predicate Q_\mathrm(n) as n = 0\,\lor\,\exists p.\big(Sp = n\land Q(p)\big). By design this trivially holds for zero, and so, akin to the bottom case in set induction, the implication Q_\mathrm(0)\,\to\, Q(0) is equivalent to just Q(0). Otherwise, Q_\mathrm(Sn)\,\leftrightarrow\, Q(n) and so, for positive numbers, Q_\mathrm(n) expresses Q(n-1). Together one obtains :\forall n. \big(Q_\mathrm(n) \,\to\, Q(n)\big)\,\to\,\forall m. Q(m)


Classical equivalents

Using the classical principles mentioned above, the above may be expressed as :\exists n. \big(\big(\forall (k < n). Q(k)\big)\,\land\,\neg Q(n)\big)\,\lor\,\forall m. Q(m) It expresses that, for any predicate Q, either there is some natural number n for which Q does not hold, despite Q holding for all predecessors, or Q hold for all numbers. Instead of \forall (k < n). Q(k), one may also use Q_\mathrm(n) and obtain a related statement. It 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. Moreover, if a failure case exists, one can use the least number principle to even prove the existence of a ''minimal'' such failure case.


Least number principle

As in the set theory case, one may consider induction for negated predicates and take the contrapositive. After use of a few classical logical equivalences, one obtains a conditional existence claim. Let \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, obtained from complete induction, here expressed in terms of sets, reads :\Theta\neq\\,\to\,\neg\neg\exists (n\in \Theta). n\cap \Theta=\ If there is any number validating T, then there (classically) is a least such number n validating it such that no number k is validating it. This should be compared with regularity. For decidable T and any given m with T(m), all k can be tested. Moreover, adopting Markov's principle in arithemetic allows removal of double-negation for decidable T in general.


See also

* Constructive set theory * Mathematical induction * Non-well-founded set theory * Transfinite induction * Well-founded induction {{Mathematical logic Mathematical induction Wellfoundedness