Un problème avec NF

Bonjour à tous,

Je suis em...bêté avec NF (New Foundations for Mathematical Logic) de Quine. Je ne sais pas s'il y a parmi vous des spécialistes de NF, mais il y a un truc qui m'échappe. Voilà ce qu'il faut savoir pour comprendre ma question.

NF est une théorie monosortée du premier ordre, avec pour notions primitives l'égalité et l'appartenance. Elle comporte deux axiomes : l'extensionnalité, et la compréhension pour les formules stratifiées. En gros, une formule est stratifiée si on peut assigner un type $t(v)$ (qui est un nombre entier) à chacune de ses variables, de sorte que, dans toute sous-formule du type $x=y$, on ait $t(y)=t(x)$, et dans toute sous-formule de la forme $x \in y$, $t(y)=t(x)+1$.

Du coup, comme $x=x$ est stratifiée, $V$ est un ensemble, $V \in V$ et $\mathscr P(V)=V$ (ouch !).

On définit la "fonction" $\iota$ par $\iota(x)=\{x\}$.

On pose $\iota[x]=\{\iota(y):y \in x\}$.

La formule stratifiée $x \neq x$ permet de définir l'ensemble vide, qui est noté $\Lambda$.

On pose $0= \{x : \forall y (y \notin x)\}=\{\Lambda\}$.

Si $x$ est un ensemble, on pose $S(x)=\{z : (\exists w \in z) [z \setminus \{w\} \in x]\}$. En d'autres termes, $S(x)=\{y \cup \{w\} : y \in x, w \in V\}$.

Puis on note $S[x]=\{S(y) : y \in x\}$.

$\mathbb{N} = \bigcap \{x : 0 \in x \land S[x] \subseteq x\}$.

Le cardinal de $x$, noté $|x|$, est l'ensemble de tous les objets qui ont la même taille que $x$. On note $NC$ l'ensemble de tous les cardinaux.

Si $x$ est un ensemble, on pose $T(|x|)=|\iota[x]|=|\{\iota(y) : y \in x \}| = \{\{y\} : y \in x\}$.

Jusque là tout va bien. C'est là que les ennuis commencent, quand on définit le Counting Axiom, noté AxCount, qui dit que $\forall n \in \mathbb{N}, T(n)=n$.

Mon problème est que je ne vois pas comment AxCount pourrait être vrai, puisque déjà, à mon sens, on a

$$T(0)=|\iota[0]|= |\{\iota(x) : x \in 0\}| = |\{\iota(\Lambda)\}| = |\{\{\Lambda\}\}|=1.$$

Où est-ce que je délire ?

Merci d'avance

Martial