Kripke-Platek set theory: Difference between revisions

no edit summary
(Created page with "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...")
 
No edit summary
 
(2 intermediate revisions by the same user not shown)
Line 3:
The axioms of KP are the following:
 
* The axiomAxiom 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)\).