View source for Kripke–Platek set theory with urelements

{{Short description|System of mathematical set theory}}
The '''Kripke–Platek set theory with urelements''' ('''KPU''') is an axiom system for [[Set theory|set theory]] with urelements, based on the traditional (urelement-free) [[Kripke–Platek set theory]]. It is considerably weaker than the (relatively) familiar system [[Zermelo–Fraenkel set theory|ZFU]]. The purpose of allowing urelements is to allow large or high-complexity objects (such as [[Baire space (set theory)|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>L^*</math> with a single binary relation symbol  <math>\in</math>.
Letters of the sort <math>p,q,r,...</math> designate urelements, of which there may be none, whereas letters of the sort <math>a,b,c,...</math> designate sets. The letters <math>x,y,z,...</math> may denote both sets and urelements.

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

The statement of the axioms also requires reference to a certain collection of formulae called <math>\Delta_0</math>-formulae. The collection <math>\Delta_0</math> consists of those formulae that can be built using the constants, <math>\in</math>, <math>\neg</math>, <math>\wedge</math>, <math>\vee</math>, and bounded quantification. That is quantification of the form <math>\forall x \in a</math> or <math> \exists x \in a</math> where <math>a</math> is given set.

==Axioms==

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

* [[Axiom of extensionality|Extensionality]]: <math>\forall x (x \in a \leftrightarrow x\in b)\rightarrow a=b</math>
* [[Axiom of regularity|Foundation]]: This is an [[Axiom schema|axiom schema]] where for every formula <math>\phi(x)</math> we have <math>\exists a. \phi(a) \rightarrow \exists a (\phi(a) \wedge \forall x\in a\,(\neg \phi(x)))</math>.
* [[Axiom of pairing|Pairing]]: <math>\exists a\, (x\in a \land y\in a )</math>
* [[Axiom of union|Union]]: <math>\exists a \forall c \in b. \forall y\in c (y \in a)</math>
* [[Axiom schema of predicative separation|&Delta;<sub>0</sub>-Separation]]: This is again an [[Axiom schema|axiom schema]], where for every <math>\Delta_0</math>-formula <math>\phi(x)</math> we have the following <math>\exists a \forall x \,(x\in a \leftrightarrow x\in b \wedge \phi(x) )</math>.
* [[Axiom schema of replacement|&Delta;<sub>0</sub>-SCollection]]: This is also an [[Axiom schema|axiom schema]], for every <math>\Delta_0</math>-formula <math>\phi(x,y)</math> we have <math>\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>\exists a\, (a=a)</math>

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

* <math>\forall p \forall a (p \neq a)</math>
* <math>\forall p \forall x (x \notin p)</math>

==Applications==

KPU can be applied to the model theory of infinitary languages. [[Model theory|Models]] of KPU considered as sets inside a maximal universe that are [[Transitive set|transitive]] as such are called [[Admissible set|admissible set]]s.

== See also ==
* Axiomatic set theory
* [[Admissible set]]
* [[Admissible ordinal]]
* [[Kripke–Platek set theory]]

== References ==
* {{Citation | last = Barwise | first = Jon |  title = Admissible Sets and Structures | publisher = Springer-Verlag | year = 1975 | isbn = 3-540-07451-1}}.
* {{Citation | last = Gostanian | first = Richard | title = Constructible Models of Subsystems of ZF | jstor = 2273185 | journal = [[Journal of Symbolic Logic]] | volume = 45 | pages = 237&ndash;250 | year = 1980 | doi=10.2307/2273185}}.

== External links ==
<!--* [http://www.cs.bilkent.edu.tr/~akman/jour-papers/air/node7.html Admissible Set Theory] (broken?)-->
* [http://bureau.philo.at/phlo/199703/msg00185.html Logic of Abstract Existence]

{{DEFAULTSORT:Kripke-Platek Set Theory With Urelements}}
[[Category:Systems of set theory]]

{{Sourceattribution|Kripke–Platek set theory with urelements}}