Kripke–Platek set theory with urelements
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  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 letters for sets may appear on both sides of , while those for urelements may only appear on the left, i.e. the following are examples of valid expressions: , . 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. Axioms

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

 Extensionality: 
 Foundation: This is an axiom schema where for every formula  we have . Pairing: 
 Union: 
 Δ0-Separation: This is again an axiom schema, where for every -formula  we have the following . Δ0-SCollection: This is also an axiom schema, for every -formula  we have . Set Existence:

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. See also 
 Axiomatic set theory
 Admissible set
 Admissible ordinal
 Kripke–Platek set theory

References 
 . . External links 

 Logic of Abstract Existence

Systems of set theory
Urelements