Kripke–Platek set theory with urelements
Kripke–Platek set theory with urelements (KPU) is a small, workable foundation for mathematics that extends Kripke–Platek set theory to include urelements. It is much weaker than the better-known ZFU.
Urelements are objects that can be members of sets but are not themselves sets. Including urelements lets us talk about very large or complex objects inside transitive models without upsetting the usual order and recursion properties we like in the constructible universe. But KP on its own is too weak to handle these ideas easily, so adding urelements helps.
To state KPU, we use a two-sorted first-order language with a single relation symbol ∈. One sort, denote by p, q, r, …, stands for urelements; another sort, denote by a, b, c, …, stands for sets. The relation ∈ can relate any two sets or a urelement to a set, but urelements themselves cannot appear on the right side of ∈ (they may only appear on the left, for example p ∈ a is allowed, but a ∈ p is not).
The formulas we use are Δ0-formulas. These are built from constants, the relation ∈, negation, conjunction, disjunction, and bounded quantification of the form ∀x ∈ a or ∃x ∈ a, where a is a given set. They are the basic, “computable” kind of formulas.
The axioms of KPU are the universal closures of a small set of formulas. In plain terms, they say how objects split into sets and urelements and how sets behave with respect to Δ0-definable properties. They capture the essential, lightweight rules about what sets can be built from what and how urelements interact with sets.
KPU can be used in model theory for infinitary languages, and when you take a transitive model of KPU inside a larger universe, such a model is called an admissible set. Admissible sets are important in studying the foundations of mathematics and the structure of constructible-like universes.
This page was last edited on 3 February 2026, at 04:37 (CET).