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>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:

  • Extensionality: <math>\forall x (x \in a \leftrightarrow x\in b)\rightarrow a=b</math>
  • Foundation: This is an 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>.
  • Pairing: <math>\exists a\, (x\in a \land y\in a )</math>
  • Union: <math>\exists a \forall c \in b. \forall y\in c (y \in a)</math>
  • &Delta;<sub>0</sub>-Separation: This is again an 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>.
  • &Delta;<sub>0</sub>-SCollection: This is also an 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. 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

  • .
  • .