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.
The usual way of stating the axioms presumes a two sorted first order language with a single binary relation symbol . Letters of the sort designate urelements, of which there may be none, whereas letters of the sort designate sets. The letters may denote both sets and urelements.
The statement of the axioms also requires reference to a certain collection of formulae called -formulae. The collection consists of those formulae that can be built using the constants, , , , , and bounded quantification. That is quantification of the form or where is given set.
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.