Kripke–Platek set theory with urelements

Kripke–Platek set theory with urelements

The Kripke–Platek set theory with urelements (KPU) is an axiom system for set theory with urelements that is considerably weaker than the familiar system ZF.


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: pin a, bin 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, eg, 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.


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

* Extensionality: forall x (x in a leftrightarrow xin b) ightarrow a=b

* Foundation: This is an axiom schema where for every formula phi(x) we have exists x phi(x) ightarrow exists x, (phi(x) wedge forall yin x,( eg phi(y))).

* Pairing: exists a, (xin a land yin a )

* Union: exists a forall x in b forall yin x, (y in a)

* Δ0-Separation: This is again an axiom schema, where for every Delta_0-formula phi(x) we have the following exists a forall x ,(xin a leftrightarrow xin 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 aexists y, phi(x,y) ightarrow exists bforall x in aexists yin 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 eq a)

* forall p forall x , (x otin p)


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 ordinal
* Kripke–Platek set theory


* Gostanian, Richard, 1980, "Constructible Models of Subsystems of ZF," "Journal of Symbolic Logic 45" (2): .
* Jon Barwise, "Admissible Sets and Structures". Springer Verlag. ISBN 3540074511

External links

* [ Logic of Abstract Existence]

Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Kripke–Platek set theory — The Kripke–Platek axioms of set theory (KP) (IPAEng|ˈkrɪpki ˈplɑːtɛk) are a system of axioms of axiomatic set theory, developed by Saul Kripke and Richard Platek. The axiom system is written in first order logic; it has an infinite number of… …   Wikipedia

  • Set theory — This article is about the branch of mathematics. For musical set theory, see Set theory (music). A Venn diagram illustrating the intersection of two sets. Set theory is the branch of mathematics that studies sets, which are collections of objects …   Wikipedia

  • List of set theory topics — Logic portal Set theory portal …   Wikipedia

  • Urelement — In set theory, a branch of mathematics, an urelement or ur element (from the German prefix ur , primordial ) is an object (concrete or abstract) which is not a set, but that may be an element of a set. Urelements are sometimes called atoms or… …   Wikipedia

  • List of mathematics articles (K) — NOTOC K K approximation of k hitting set K ary tree K core K edge connected graph K equivalence K factor error K finite K function K homology K means algorithm K medoids K minimum spanning tree K Poincaré algebra K Poincaré group K set (geometry) …   Wikipedia

  • List of mathematical logic topics — Clicking on related changes shows a list of most recent edits of articles to which this page links. This page links to itself in order that recent changes to this page will also be included in related changes. This is a list of mathematical logic …   Wikipedia

  • Axiom schema of specification — For the separation axioms in topology, see separation axiom. In axiomatic set theory and the branches of logic, mathematics, and computer science that use it, the axiom schema of specification, axiom schema of separation, subset axiom scheme or… …   Wikipedia

  • KPU — is an abbreviation that can mean:* Kripke–Platek set theory with urelements, an axiom system for set theory * Kwantlen Polytechnic University, University in British Columbia. * [ Korea Polytechnic University] …   Wikipedia

  • Mathematical logic — (also known as symbolic logic) is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic.[1] The field includes both the mathematical study of logic and the… …   Wikipedia