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 [math]\displaystyle{ L^* }[/math] with a single binary relation symbol [math]\displaystyle{ \in }[/math]. Letters of the sort [math]\displaystyle{ p,q,r,... }[/math] designate urelements, of which there may be none, whereas letters of the sort [math]\displaystyle{ a,b,c,... }[/math] designate sets. The letters [math]\displaystyle{ x,y,z,... }[/math] may denote both sets and urelements.
The letters for sets may appear on both sides of [math]\displaystyle{ \in }[/math], while those for urelements may only appear on the left, i.e. the following are examples of valid expressions: [math]\displaystyle{ p\in a }[/math], [math]\displaystyle{ b\in a }[/math].
The statement of the axioms also requires reference to a certain collection of formulae called [math]\displaystyle{ \Delta_0 }[/math]-formulae. The collection [math]\displaystyle{ \Delta_0 }[/math] consists of those formulae that can be built using the constants, [math]\displaystyle{ \in }[/math], [math]\displaystyle{ \neg }[/math], [math]\displaystyle{ \wedge }[/math], [math]\displaystyle{ \vee }[/math], and bounded quantification. That is quantification of the form [math]\displaystyle{ \forall x \in a }[/math] or [math]\displaystyle{ \exists x \in a }[/math] where [math]\displaystyle{ a }[/math] is given set.
Axioms
The axioms of KPU are the universal closures of the following formulae:
- Extensionality: [math]\displaystyle{ \forall x (x \in a \leftrightarrow x\in b)\rightarrow a=b }[/math]
- Foundation: This is an axiom schema where for every formula [math]\displaystyle{ \phi(x) }[/math] we have [math]\displaystyle{ \exists a. \phi(a) \rightarrow \exists a (\phi(a) \wedge \forall x\in a\,(\neg \phi(x))) }[/math].
- Pairing: [math]\displaystyle{ \exists a\, (x\in a \land y\in a ) }[/math]
- Union: [math]\displaystyle{ \exists a \forall c \in b. \forall y\in c (y \in a) }[/math]
- Δ0-Separation: This is again an axiom schema, where for every [math]\displaystyle{ \Delta_0 }[/math]-formula [math]\displaystyle{ \phi(x) }[/math] we have the following [math]\displaystyle{ \exists a \forall x \,(x\in a \leftrightarrow x\in b \wedge \phi(x) ) }[/math].
- Δ0-SCollection: This is also an axiom schema, for every [math]\displaystyle{ \Delta_0 }[/math]-formula [math]\displaystyle{ \phi(x,y) }[/math] we have [math]\displaystyle{ \forall x \in a.\exists y. \phi(x,y)\rightarrow \exists b\forall x \in a.\exists y\in b. \phi(x,y) }[/math].
- Set Existence: [math]\displaystyle{ \exists a\, (a=a) }[/math]
Additional assumptions
Technically these are axioms that describe the partition of objects into sets and urelements.
- [math]\displaystyle{ \forall p \forall a (p \neq a) }[/math]
- [math]\displaystyle{ \forall p \forall x (x \notin p) }[/math]
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
- 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.
External links
 |  |
