Kripke-Platek set theory

Kripke-Platek set theory, commonly abbreviated KP, is a weak foundation of set theory used to define admissible ordinals, which are immensely important in ordinal analysis and \(\alpha\)-recursion theory. In terms of proof-theoretic strength, its proof-theoretic ordinal is the BHO, and it is thus intermediate between \(\mathrm{ATR}_0\) and \(\Pi^1_1 \mathrm{-CA}_0\).

The axioms of KP are the following:

• Axiom of extensionality: two sets are the same if and only if they have the same elements.
• Axiom of induction: transfinite induction along the \(\in\)-relation (this implies the axiom of foundation)
• Axiom of empty set: There exists a set with no members.
• Axiom of pairing: If \(x\), \(y\) are sets, then so is \(\{x, y\}\).
• Axiom of union: For any set \(x\), there is a set \(y\) such that the elements of \(y\) are precisely the elements of the elements of \(x\).
• Axiom of infinity: there is an inductive set.
• Axiom of \(\Delta_0\)-separation: Given any set \(X\) and any \(\Delta_0\)-formula \(\varphi(x)\), \(\{x \in X: \varphi(x)\}\) is also a set.
• Axiom of \(\Delta_0\)-collection: If \(\varphi(x,y)\) is a \(\Delta_0\)-formula so that \(\forall x \exists y \varphi(x,y)\), then for all \(X\), there is some \(Y\) so that \(\forall x \in X \exists y \in Y \varphi(x,y)\).

These axioms lead to close connections between KP, \(\alpha\)-recursion theory, and the theory of admissible ordinals. A set \(M\) is admissible if, and only if, it satisfies KP. We say \(\alpha\) is admissible if \(L_\alpha\) is admissible. You can see that this holds if and only if \(\alpha > \omega\) is a limit ordinal and, for every \(\Delta_0(L_\alpha)\)-definable \(f: L_\alpha \to L_\alpha\) and \(x \in L_\alpha\), \(f''x \in L_\alpha\) as well. The least admissible ordinal is the Church-Kleene ordinal. Note that some authors drop the axiom of infinity and consider \(\omega\) an admissible ordinal too. Note that \(\Delta_0\)-collection actually implies \(\Sigma_1\)-collection.

Kripke-Platek set theory may be imagined as being the minimal system of set theory which has infinite sets and allows one to do "computable" and "predicative" definitions over sets. This is because the \(\Sigma_1(L_\alpha)\)-definable functions are considered analogues of computable ones, and, in the context of separation, \(\Delta_0\)-formulae are considered predicative or primitive due to not referencing the totality of the universe.