Théorie des ensembles de Kripke-Platek

• Axiome d'extensionnalité : Deux ensembles qui ont les mêmes éléments sont égaux.
• Axiome d'induction : φ(x) étant une formule du premier ordre :

${\displaystyle [\forall x[\forall y\in x,\varphi (y)\Rightarrow \;\varphi (x)]]\Rightarrow \;\forall x\varphi (x)}$.

• Axiome de l'ensemble vide : Il existe un ensemble sans élément.
• Axiome de la paire : Si x et y sont des ensembles, il existe un ensemble noté {x, y} ayant exactement pour éléments x et y.
• Axiome de la réunion : Pour tout ensemble X il y a un ensemble UX dont les éléments sont ceux des éléments de X.
• Axiome de Σ₀-séparation : Pour tout ensemble X et toute Σ₀-formule φ(x), il y a un ensemble des éléments de X qui satisfont φ(x).
• Axiome de Σ₀-collection : Soit une Σ₀-formule φ(x, y) telle que pour tout x existe un y satisfaisant φ(x, y) ; alors pour tout X il y a un ensemble Y des y tels que φ(x, y) pour un x de X.

Ici, une Σ₀-formule est une formule dans laquelle toute quantification est de la forme ${\displaystyle \forall u\in v}$ ou ${\displaystyle \exists u\in v}$, les variables sur lesquelles portent les quantificateurs décrivent un ensemble.

Ainsi cette théorie est significativement plus faible que la théorie usuelle ZFC, puisque ne comportant pas les axiomes de l'ensemble des parties, de l'infini et du choix, et utilisant des formes affaiblies des schémas de compréhension et de remplacement.

L'axiome d'induction est plus fort que l'axiome de fondation de ZF.

L'existence du produit cartésien suit du schéma de collection, du schéma de séparation, et des axiomes de la paire et de la réunion.

Un ensemble E est dit admissible s'il est transitif et si ${\displaystyle \langle E,\in \rangle \,\!}$ est un modèle de la théorie de Kripke-Platek.

Un ordinal α est dit admissible si L_α est un ensemble admissible.