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