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.

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.

...
Wikipedia