Editing Kripke–Platek set theory (section)

== Theorems ==

=== Admissible sets ===
The ordinal ''α'' is an admissible ordinal if and only if ''α'' is a [[limit ordinal]] and there does not exist a ''γ''&nbsp;<&nbsp;''α'' for which there is a Σ<sub>1</sub>(L<sub>''α''</sub>) mapping from ''γ'' onto ''α''.  If ''M'' is a standard model of KP, then the set of ordinals in ''M'' is an admissible ordinal.

=== Cartesian products exist ===
'''Theorem:'''
If ''A'' and ''B'' are sets, then there is a set ''A''×''B'' which consists of all [[ordered pair]]s (''a'', ''b'') of elements ''a'' of ''A'' and ''b'' of ''B''.

'''Proof:'''

The singleton set with member ''a'', written {''a''}, is the same as the unordered pair {''a'', ''a''}, by the axiom of '''[[extensionality]]'''. 

The singleton, the set {''a'', ''b''}, and then also the ordered pair
:<math>(a,b) := \{ \{a\}, \{a,b\} \} </math>
all exist by '''pairing'''.
A possible Δ<sub>0</sub>-formula <math>\psi (a, b, p)</math> expressing that ''p'' stands for the pair (''a'', ''b'') is given by the lengthy
:<math>\exist r \in p\, \big(a \in r\, \land\, \forall x \in r\, (x = a) \big)</math>
::<math>\land\, \exist s \in p\, \big(a \in s \,\land\, b \in s\, \land\, \forall x \in s\, (x = a \,\lor\, x = b) \big)</math>
:::<math>\land\, \forall t \in p\, \Big(\big(a \in t\, \land\, \forall x \in t\, (x = a)\big)\, \lor\, \big(a \in t \land b \in t \land \forall x \in t\, (x = a \,\lor\, x = b)\big)\Big).</math>

What follows are two steps of collection of sets, followed by a restriction through separation. All results are also expressed using set builder notation.

Firstly, given <math>b</math> and collecting with respect to <math>A</math>, some superset of <math>A\times\{b\} = \{(a,b)\mid a\in A\}</math> exists by '''collection'''.

The Δ<sub>0</sub>-formula 
:<math>\exist a \in A \,\psi (a, b, p)</math> 
grants that just <math>A\times\{b\}</math> itself exists by '''separation'''.

If <math>P</math> ought to stand for this collection of pairs <math>A\times\{b\}</math>, then a Δ<sub>0</sub>-formula characterizing it is
:<math>\forall a \in A\, \exist p \in P\, \psi (a, b, p)\, \land\, \forall p \in P\, \exist a \in A\, \psi (a, b, p) \,.</math>
Given <math>A</math> and collecting with respect to <math>B</math>, some superset of <math>\{A\times \{b\} \mid b\in B\}</math> exists by '''collection'''.

Putting <math>\exist b \in B</math> in front of that last formula and one finds the set <math>\{A\times \{b\} \mid b\in B\}</math> itself exists by '''separation'''.

Finally, the desired
:<math>A\times B := \bigcup \{A\times \{b\} \mid b\in B\}</math>
exists by '''union'''.
[[Q.E.D.]]

=== 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.