# Kripke–Platek set theory with urelements

Template:Expert-subject The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements, based on the traditional (urelement-free) Kripke-Platek set theory. It is considerably weaker than the (relatively) familiar system ZFU. The purpose of allowing urelements is to allow large or high-complexity objects (such as the set of all reals) to be included in the theory's transitive models without disrupting the usual well-ordering and recursion-theoretic properties of the constructible universe; KP is so weak that this is hard to do by traditional means.

## Preliminaries

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.

## Axioms

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

Technically these are axioms that describe the partition of objects into sets and urelements.

## Applications

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.