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^{*}}${\displaystyle L^{*}} with a single binary relation symbol ${\displaystyle \in }${\displaystyle \in }. Letters of the sort ${\displaystyle p,q,r,...}${\displaystyle p,q,r,...} designate urelements, of which there may be none, whereas letters of the sort ${\displaystyle a,b,c,...}${\displaystyle a,b,c,...} designate sets. The letters ${\displaystyle x,y,z,...}${\displaystyle x,y,z,...} may denote both sets and urelements.

The letters for sets may appear on both sides of ${\displaystyle \in }${\displaystyle \in }, while those for urelements may only appear on the left, i.e. the following are examples of valid expressions: ${\displaystyle p\in a}${\displaystyle p\in a}, ${\displaystyle b\in a}${\displaystyle b\in a}.

The statement of the axioms also requires reference to a certain collection of formulae called ${\displaystyle \Delta _{0}}${\displaystyle \Delta _{0}}-formulae. The collection ${\displaystyle \Delta _{0}}${\displaystyle \Delta _{0}} consists of those formulae that can be built using the constants, ${\displaystyle \in }${\displaystyle \in }, ${\displaystyle \neg }${\displaystyle \neg }, ${\displaystyle \wedge }${\displaystyle \wedge }, ${\displaystyle \vee }${\displaystyle \vee }, and bounded quantification. That is quantification of the form ${\displaystyle \forall x\in a}${\displaystyle \forall x\in a} or ${\displaystyle \exists x\in a}${\displaystyle \exists x\in a} where ${\displaystyle a}${\displaystyle a} is given set.

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

• Extensionality: ${\displaystyle \forall x(x\in a\leftrightarrow x\in b)\rightarrow a=b}${\displaystyle \forall x(x\in a\leftrightarrow x\in b)\rightarrow a=b}
• Foundation: This is an axiom schema where for every formula ${\displaystyle \phi (x)}${\displaystyle \phi (x)} we have ${\displaystyle \exists a.\phi (a)\rightarrow \exists a(\phi (a)\wedge \forall x\in a,円(\neg \phi (x)))}${\displaystyle \exists a.\phi (a)\rightarrow \exists a(\phi (a)\wedge \forall x\in a,円(\neg \phi (x)))}.
• Pairing: ${\displaystyle \exists a,円(x\in a\land y\in a)}${\displaystyle \exists a,円(x\in a\land y\in a)}
• Union: ${\displaystyle \exists a\forall c\in b.\forall y\in c(y\in a)}${\displaystyle \exists a\forall c\in b.\forall y\in c(y\in a)}
• Δ₀-Separation: This is again an axiom schema, where for every ${\displaystyle \Delta _{0}}${\displaystyle \Delta _{0}}-formula ${\displaystyle \phi (x)}${\displaystyle \phi (x)} we have the following ${\displaystyle \exists a\forall x,円(x\in a\leftrightarrow x\in b\wedge \phi (x))}${\displaystyle \exists a\forall x,円(x\in a\leftrightarrow x\in b\wedge \phi (x))}.
• Δ₀-SCollection: This is also an axiom schema, for every ${\displaystyle \Delta _{0}}${\displaystyle \Delta _{0}}-formula ${\displaystyle \phi (x,y)}${\displaystyle \phi (x,y)} we have ${\displaystyle \forall x\in a.\exists y.\phi (x,y)\rightarrow \exists b\forall x\in a.\exists y\in b.\phi (x,y)}${\displaystyle \forall x\in a.\exists y.\phi (x,y)\rightarrow \exists b\forall x\in a.\exists y\in b.\phi (x,y)}.
• Set Existence: ${\displaystyle \exists a,円(a=a)}${\displaystyle \exists a,円(a=a)}

Technically these are axioms that describe the partition of objects into sets and urelements.

• ${\displaystyle \forall p\forall a(p\neq a)}${\displaystyle \forall p\forall a(p\neq a)}
• ${\displaystyle \forall p\forall x(x\notin p)}${\displaystyle \forall p\forall x(x\notin p)}

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.

• Axiomatic set theory
• Admissible set
• Admissible ordinal
• Kripke–Platek set theory

• Barwise, Jon (1975), Admissible Sets and Structures, Springer-Verlag, ISBN 3-540-07451-1 .
• Gostanian, Richard (1980), "Constructible Models of Subsystems of ZF", Journal of Symbolic Logic , 45: 237–250, doi:10.2307/2273185, JSTOR 2273185 .

• "Logic of Abstract Existence". Archived from the original on 2007年09月30日.

• "Admissible Set Theory". Archived from the original on 2003年09月02日.

• Systems of set theory
• Urelements

• Articles with short description
• Short description is different from Wikidata