The Kripke–Platek set theory (KP), pronounced , is an axiomatic set theory developed by Saul Kripke and Richard Platek. The theory can be thought of as roughly the predicative part of Zermelo–Fraenkel set theory (ZFC) and is considerably weaker than it.
Axioms In its formulation, a Δ0 formula is one all of whose quantifiers are bounded. This means any quantification is the form ∀ u ∈ v {\displaystyle \forall u\in v} or ∃ u ∈ v . {\displaystyle \exists u\in v.} (See the Lévy hierarchy.)
Axiom of extensionality: Two sets are the same if and only if they have the same elements. So a set z which contains one of them x, contains the other y.
∀ z ∀ y ( ∃ x ∈ z [ ∀ w ∈ x ( w ∈ y ) ∧ ∀ w ∈ y ( w ∈ x ) ] ⟹ y ∈ z ) . {\displaystyle \forall z\forall y(\exists x\in z[\forall w\in x(w\in y)\land \forall w\in y(w\in x)]\implies y\in z).}
This axiom is a Π1 formula. In light of this axiom, we can define equality by a Δ0 formula:
x = y ≡ ∀ w ∈ x ( w ∈ y ) ∧ ∀ w ∈ y ( w ∈ x ) . {\displaystyle x=y\equiv \forall w\in x(w\in y)\land \forall w\in y(w\in x).}
Axiom of induction: φ(a) being a formula, if for all sets x the assumption that φ(y) holds for all elements y of x entails that φ(x) holds, then φ(x) holds for all sets x.
∀ w 1 , … , w n [ ∀ x ( ∀ y ∈ x φ ( w 1 , … , w n , y ) ⟹ φ ( w 1 , … , w n , x ) ) ⟹ ∀ x φ ( w 1 , … , w n , x ) ] . {\displaystyle \forall w_{1},\ldots ,w_{n}[\forall x(\forall y\in x\varphi (w_{1},\ldots ,w_{n},y)\implies \varphi (w_{1},\ldots ,w_{n},x))\implies \forall x\varphi (w_{1},\ldots ,w_{n},x)].}
Depending on the choice of φ, this axiom could be at level Δk for any k with 2 ≤ k < ω when n = 0 or Πk when n > 0.
Axiom of empty set: There exists a set with no members, called the empty set and denoted { } or ∅ or 0.
∃ x ∀ y ∈ x ( y ∉ x ) . {\displaystyle \exists x\forall y\in x(y\notin x).}
This axiom is a Σ1 formula. If, as in this case, there is a Δ0 formula definiens such that one has a proof that there is one unique set with that property, then we can introduce a symbol(s) for it and use it as a parameter in other Δ0 formulas.
Axiom of pairing: If x, y are sets, then so is {x, y}, a set containing x and y as its only elements.
∀ x ∀ y ∃ z ( x ∈ z ∧ y ∈ z ∧ ∀ w ∈ z ( w = x ∨ w = y ) ) . {\displaystyle \forall x\forall y\exists z(x\in z\land y\in z\land \forall w\in z(w=x\lor w=y)).}
This axiom is a Π2 formula.
Axiom of union: For any set x, there is a set y such that the elements of y are precisely the elements of the elements of x.
∀ x ∃ y ( ∀ z ∈ x ∀ w ∈ z ( w ∈ y ) ∧ ∀ w ∈ y ∃ z ∈ x ( w ∈ z ) ) . {\displaystyle \forall x\exists y(\forall z\in x\forall w\in z(w\in y)\land \forall w\in y\exists z\in x(w\in z)).}
This axiom is a Π2 formula.
Axiom of Δ0-separation: Given any set and any Δ0 formula φ(x), there is a subset of the original set containing precisely those elements x for which φ(x) holds. (This is an axiom schema.)
∀ w 1 , … , w n ∀ a ∃ b [ ∀ x ∈ a ( φ ( w 1 , … , w n , x ) ⟹ x ∈ b ) ∧ ∀ x ∈ b ( x ∈ a ∧ φ ( w 1 , … , w n , x ) ) ] . {\displaystyle \forall w_{1},\ldots ,w_{n}\forall a\exists b[\forall x\in a(\varphi (w_{1},\ldots ,w_{n},x)\implies x\in b)\land \forall x\in b(x\in a\land \varphi (w_{1},\ldots ,w_{n},x))].}
This axiom is a Π2 formula.
… excerpt ends here. Continue reading the full article.
