Kripke–Platek set theory with urelements

The usual way of stating the axioms presumes a two sorted first order language ${\displaystyle L^{*}}$ with a single binary relation symbol ${\displaystyle \in }$. Letters of the sort ${\displaystyle p,q,r,...}$ designate urelements, of which there may be none, whereas letters of the sort ${\displaystyle a,b,c,...}$ designate sets. The letters ${\displaystyle x,y,z,...}$ may denote both sets and urelements.

The letters for sets may appear on both sides of ${\displaystyle \in }$, while those for urelements may only appear on the left, i.e. the following are examples of valid expressions: ${\displaystyle p\in a}$, ${\displaystyle b\in a}$.

The statement of the axioms also requires reference to a certain collection of formulae called ${\displaystyle \Delta _{0}}$-formulae. The collection ${\displaystyle \Delta _{0}}$ consists of those formulae that can be built using the constants, ${\displaystyle \in }$, ${\displaystyle \neg }$, ${\displaystyle \wedge }$, ${\displaystyle \vee }$, and bounded quantification. That is quantification of the form ${\displaystyle \forall x\in a}$ or ${\displaystyle \exists x\in a}$ where ${\displaystyle a}$ is given set.

The axioms of KPU are the universal closures of the following formulae:

• Extensionality: ${\displaystyle \forall x(x\in a\leftrightarrow x\in b)\rightarrow a=b}$
• Foundation: This is an axiom schema where for every formula ${\displaystyle \phi (x)}$ we have ${\displaystyle \exists a.\phi (a)\rightarrow \exists a(\phi (a)\wedge \forall x\in a\,(\neg \phi (x)))}$.
• Pairing: ${\displaystyle \exists a\,(x\in a\land y\in a)}$
• Union: ${\displaystyle \exists a\forall c\in b.\forall y\in c(y\in a)}$
• Δ₀-Separation: This is again an axiom schema, where for every ${\displaystyle \Delta _{0}}$-formula ${\displaystyle \phi (x)}$ we have the following ${\displaystyle \exists a\forall x\,(x\in a\leftrightarrow x\in b\wedge \phi (x))}$.
• Δ₀-SCollection: This is also an axiom schema, for every ${\displaystyle \Delta _{0}}$-formula ${\displaystyle \phi (x,y)}$ we have ${\displaystyle \forall x\in a.\exists y.\phi (x,y)\rightarrow \exists b\forall x\in a.\exists y\in b.\phi (x,y)}$.
• Set Existence: ${\displaystyle \exists a\,(a=a)}$

KPU can be applied to the model theory of infinitary languages. Models of KPU considered as sets inside a maximal universe that are transitive as such are called admissible sets.

• Axiomatic set theory
• Admissible set
• Admissible ordinal
• Kripke–Platek set theory

• Barwise, Jon (1975), Admissible Sets and Structures, Springer-Verlag, ISBN 3-540-07451-1.
• Gostanian, Richard (1980), "Constructible Models of Subsystems of ZF", Journal of Symbolic Logic, 45: 237–250, doi:10.2307/2273185, JSTOR 2273185.

• Logic of Abstract Existence