Théorie des ensembles de Kripke-Platek
Cet article est une ébauche concernant les mathématiques.
Vous pouvez partager vos connaissances en l’améliorant (comment ?) selon les recommandations des projets correspondants.
La théorie des ensembles de Kripke-Platek est un système d'axiomes du premier ordre pour la théorie des ensembles, développé par Saul Kripke et Richard Platek. Il comporte trois schémas d'axiomes, dont chacun équivaut à une liste infinie d'axiomes du premier ordre.
Les axiomes
[modifier | modifier le code]- 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)}](https://wikimedia.org/api/rest_v1/media/math/render/svg/74b52cdc51796cca80736ea95f7bd70bbab0065d)
- 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 Σ0-séparation : Pour tout ensemble X et toute Σ0-formule φ(x), il y a un ensemble des éléments de X qui satisfont φ(x).
- Axiome de Σ0-collection : Soit une Σ0-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 Σ0-formule est une formule dans laquelle toute quantification est de la forme ou , 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.
Ensembles et ordinaux admissibles
[modifier | modifier le code]Un ensemble E est dit admissible s'il est transitif et si est un modèle de la théorie de Kripke-Platek.
Un ordinal α est dit admissible si Lα est un ensemble admissible.
