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.
Contents
Preliminaries
The usual way of stating the axioms presumes a two sorted first order language
The letters for sets may appear on both sides of
The statement of the axioms also requires reference to a certain collection of formulae called
Axioms
The axioms of KPU are the universal closures of the following formulae:
Additional assumptions
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.