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.
Preliminaries
The usual way of stating the axioms presume a two sorted first order language with a single binary relation symbol . Letters of the sort designate urelements, of which there may be none, whereas letters of the sort designate sets. The letters may denote both sets and urelements.
The letters for sets may appear on both sides of , while those for urelements may only appear on the left, i.e. the following are examples of valid expressions: , .
The statement of the axioms also requires reference to a certain collection of formulae called -formulae. The collection consists of those formulae that can be built using the constants, , , , , and bounded quantification. That is quantification of the form or where is given set.
Axioms
The axioms of KPU are the universal closures of the following formulae:
- Foundation: This is an axiom schema where for every formula we have .
- -Separation: This is again an axiom schema, where for every -formula we have the following .
- -Collection: This is also an axiom schema, for every -formula we have .
External links
- Admissible Set Theory
- Logic of Abstract Existence
- Jon Barwise, Admissible Sets and Structures, Springer, ISBN 3540074511