Théorème de définition par récurrence

Appelons approximation une application $h$ définie sur un entier $k \neq 0$, à valeurs dans $E$, telle que $h(0) = a$ et $h(S(m)) = g(h(m))$ dès que $S(m) \in k$. Cette condition a un sens : si $S(m) \in k$, alors $m \in k$, puisque $m \in S(m)$, $k$ étant transitif (Entiers transitifs).

Unicité. Deux approximations $h$ et $h'$ coïncident sur l'intersection de leurs domaines : par récurrence sur $m$, si $m$ est dans les deux domaines, $h(m) = h'(m)$, car $h(0) = a = h'(0)$ et, si $S(m)$ est dans les deux domaines, $m$ l'est aussi, ces domaines étant transitifs, d'où $h(S(m)) = g(h(m)) = g(h'(m)) = h'(S(m))$.

Existence. Par récurrence, pour tout $n$ il existe une approximation de domaine $S(n)$ : pour $n = 0$, c'est $\{(0, a)\}$ ; si $h$ convient pour $n$, alors $h \cup \{(S(n), g(h(n)))\}$ est une application de domaine $S(S(n))$, puisque $S(n) \notin S(n)$ (fondation), et elle convient pour $S(n)$, l'injectivité de $S$ (Axiomes de Peano) garantissant que la nouvelle condition ne porte que sur le point ajouté.

On pose alors $f(n) = h(n)$, pour $h$ une approximation de domaine $S(n)$. Ces approximations forment un ensemble, partie de ${\mathcal P}(\omega \times E)$, et $f$, réunion de leurs graphes, est une application d'après l'unicité. Elle vérifie les deux relations, et toute application qui les vérifie coïncide avec $f$ par récurrence.