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

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

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

Axioms

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

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

Additional assumptions

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

$\forall p\forall a(p\neq a)$
$\forall p\forall x(x\notin p)$

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.

References

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.

External links

"Logic of Abstract Existence". Archived from the original on 2007-09-30.

"Admissible Set Theory". Archived from the original on 2003-09-02.