View source for Kripke-Platek

{{DISPLAYTITLE: The axioms of Kripke-Platek set theory}}
Kripke-Platek set theory ($\text{KP}$) is a collection of axioms that is considerably weaker than [[ZFC]]. The formal language used to express each axiom is first-order with equality ($=$) together with one binary relation symbol, $\in$, intended to denote set membership.

$L_\alpha$ is a model of $\mathrm{KP}$ for [[admissible]] $\alpha$.

==Axiom of Extensionality== 
Sets are determined uniquely by their elements. This is expressed formally as $$ \forall x \forall y \big(\forall z (z\in x\leftrightarrow z\in y)\rightarrow x=y\big).$$ 

The &ldquo;$\rightarrow$&rdquo; can be replaced by &ldquo;$\leftrightarrow$&rdquo;, but the $\leftarrow$ direction is a theorem of logic.

==Axiom of Null Set==
There exists some set. In fact, there is a set which contains no members. 
This is expressed formally $$ \exists x \forall y (y\not\in x).$$ 

Such an $x$ is unique by extensionality and this set is denoted by $\emptyset$.

==Axiom of Pairing== 
For any two sets $x$ and $y$ (not necessarily distinct) there is a further set $z$ whose members are exactly the sets $x$ and $y$.
  
$$ \forall x \forall y \exists  z \forall w \big(w\in z\leftrightarrow (w=x\vee w=y)\big).$$ 

Such a $z$ is unique by extensionality and is denoted as $\{x,y\}$.

==Axiom of Union==
For any set $x$ there is a further set $y$ whose members are exactly all the members of the members of $x$. That is, the union of all the members of a set exists. This is expressed formally as 

$$\forall x \exists y \forall z \big(z\in y \leftrightarrow \exists w (w\in x \wedge z\in w)\big).$$ 

Such a $y$ is unique by extensionality and is written as $y = \bigcup x$.

==Axiom Schema of Foundation==
Suppose that a given property $P$ is true for some set $x$. Then there is a $\in$-minimal set for which $P$ is true.
In more detail, given a formula $\varphi(x_1,\dots,x_n,x)$ the following is an instance of the induction schema:
$$\forall x_1, \ldots, x_n \big[ \exists x \varphi(x_1, \ldots, x_n, x) \rightarrow \exists y \big( \varphi(x_1, \ldots, x_n, y) \wedge \forall z \in y \neg \varphi(x_1, \ldots, x_n, z) \big) \big]$$

==Axiom Schema of $\Sigma_0$-Separation== 
For any set $a$ and any $\Sigma_0$-predicate $P(x)$ written in the language of ZFC, the set $\{x\in a: P(x)\}$ exists. In more detail, given any $\Sigma_0$-formula $\varphi$ with free variables $x_1,x_2,\dots,x_n$ the following is an instance of the $\Sigma_0$-seperation schema: 
$$ \forall a \forall x_1 \forall x_2\dots \forall x_n \exists y \forall z \big(z\in y \leftrightarrow (z\in a \wedge \varphi(x_1,x_2,\dots,x_n,z)\big) $$ 

Such a $y$, unique by extensionality and is written (for fixed sets $a, x_1\dots, x_n$) $y=\{z\in a: \varphi(x_1,x_2,\dots,x_n,z)\}$.

==Axiom Schema of $\Sigma_0$-Collection==
If $a$ is a set and for all $x\in a$ there's a some $y$ such that $(x,y)$ satisfies a given $\Sigma_0$-property, then there is some set $b$ such that for all $x \in a$ there is some $y \in b$ such that $(x,y)$ satisfies that property. In more detail, given a $\Sigma_0$-formula $\varphi(x_1,\dots,x_n,x,y)$ the following is an instance of the $\Sigma_0$-collection schema:
$$ \forall a \forall x_1 \dots \forall x_n \big[\big( \forall x\in a \exists y \varphi(x_1,\dots,x_n,x,y)\big)\rightarrow \big(\exists b \forall x \in a \exists y \in b \varphi(x_1, \ldots, x_n, x,y) \big) \big].$$

==Axiom of Infinity==
Some authors include the axiom of infinity in Kripke-Platek set theory which states that there is an [[inductive set]] – a canonical example of an infinite set. More precisely:
$$ \exists x \big( \emptyset \in x \wedge \forall y \in x (y \cup \{y \} \in x) \big).$$
The axiom of infinity combined with an instance of $\Sigma_0$-separation imply the axiom of null set so that it be dropped if one assumes the axiom of infinity.