Editing Kripke–Platek set theory (section)

=== Transitive containment ===

Transitive containment is the principle that every set is contained in some [[transitive set]]. It does not hold in certain set theories, such as [[Zermelo set theory]] (though its inclusion as an axiom does not add consistency strength<ref>{{cite journal | last=Mathias | first=A.R.D. | title=The strength of Mac Lane set theory | journal=Annals of Pure and Applied Logic | volume=110 | issue=1-3 | date=2001 | doi=10.1016/S0168-0072(00)00031-2 | doi-access=free | pages=107–234}}</ref>).

'''Theorem:'''
If ''A'' is a set, then there exists a transitive set ''B'' such that ''A'' is a member of ''B''.

'''Proof:'''

We proceed by '''induction''' on the formula:
:<math>\phi(A) := \exist B (A \in B \land \bigcup B \subseteq B)</math>
Note that <math>\bigcup B \subseteq B</math> is another way of expressing that ''B'' is transitive.

The inductive hypothesis then informs us that
:<math>\forall a \in A \, \exist b(a \in b \land \bigcup b \subseteq b)</math>.
By '''Δ<sub>0</sub>-collection''', we have:
:<math>\exist C \, \forall a \in A \, \exist b \in C (a \in b \land \bigcup b \subseteq b)</math>
By '''Δ<sub>0</sub>-separation''', the set <math>\{c \in C \mid \bigcup c \subseteq c\}</math> exists, whose '''union''' we call ''D''.

Now ''D'' is a union of transitive sets, and therefore itself transitive. And since <math>A \subseteq D</math>, we know <math>D \cup \{A\}</math> is also transitive, and further contains ''A'', as required. Q.E.D.