ATLAS Ouvrir dans l'atlas →

AxiomeAxiomes de ZF

Axiome de l'infini

C'est le seul axiome qui affirme l'existence d'un ensemble infini ; sans lui, tous les ensembles construits seraient finis, au sens qui sera défini au nœud « Finitude sans les entiers » de ce graphe.

Énoncé

Il existe un ensemble inductif, c'est-à-dire un ensemble II qui a un élément sans élément et qui, avec chacun de ses éléments xx, contient l'ensemble dont les éléments sont ceux de xx et xx lui-même : ∃I [∃e (e∈I∧∀z z∉e)∧∀x (x∈I⇒∃y (y∈I∧∀z (z∈y⇔(z∈x∨z=x))))].\begin{aligned} \exists I\, \Big[&\exists e\, \big(e \in I \wedge \forall z\, z \notin e\big) \\ &\wedge \forall x\, \Big(x \in I \Rightarrow \exists y\, \big(y \in I \\ &\quad \wedge \forall z\, (z \in y \\ &\qquad \Leftrightarrow (z \in x \vee z = x))\big)\Big)\Big]. \end{aligned}

Remarque

L'axiome est écrit dans le langage pur, parce que l'ensemble vide, la paire et la réunion ne sont introduits qu'après lui. Avec les notations des nœuds Ensemble vide et Opérations booléennes, il se lit plus simplement : il existe un ensemble II tel que ∅∈I\varnothing \in I et x∪{x}∈Ix \cup \{x\} \in I pour tout x∈Ix \in I.

Remarque

Il fonde la construction de ℕ\mathbb N, plus petit ensemble inductif. Que cet ensemble soit infini au sens du nœud Ensembles finis, sans les entiers, le nœud Ensembles finis et principe des tiroirs le montrera.

Repose sur

Langage de ZF

Sert à

Aucune fiche de ce graphe ne l'utilise encore.
Ouvrir dans l'atlas interactif →