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) )$.

• $\Delta_0$-Collection: 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.

See also

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

References

• .
• .

External links

• Logic of Abstract Existence