# 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 “$\rightarrow$” can be replaced by “$\leftrightarrow$”, 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.