Le graphe de la fonction β, formule Δ₀ fonctionnelle dans l'arithmétique de Peano

On écrit $m$ pour le terme $m(b, i)$, qui n'est pas nul par $\mathrm Q_1$. Par le point (v) de Ordre dans PA, $t < m$, qui est $t < S(S\,i \times b)$, équivaut à $t \leqslant S\,i \times b$ pour tout terme $t$. Une hypothèse $B(a, b, i, u)$ s'élimine, avec deux variables nouvelles $g$ et $e$, sous la forme $a = g \times m + u$ et $e + u = S\,i \times b$.

(i) Sous les hypothèses $a = g \times m + u$ et $e + u = S\,i \times b$, le point (vi) de Ordre dans PA, avec $\neg(m = 0)$, donne $g \leqslant g \times m$, le point (i) donne $g \times m \leqslant g \times m + u$, et la transitivité et le remplacement donnent $g \leqslant a$. Le point (vii) (a) du même nœud, avec le terme $g$, donne $\exists q \leqslant a\ (a = q \times m + u)$. De même, $e \leqslant e + u$ et le remplacement donnent $e \leqslant S\,i \times b$, puis $\exists r \leqslant S\,i \times b\ (r + u = S\,i \times b)$. On élimine $e$ et $g$, ce qui donne $B \to B_0$. Réciproquement, le point (vii) (c) du même nœud ramène chacun des deux membres de $B_0$ à une formule $\exists q\, (q \leqslant a \wedge \cdots)$, et la monotonie de Récurrence dans PA, (ii), donne $\exists q\, (a = q \times m + u)$ et $\exists r\, (r + u = S\,i \times b)$ ; sous les hypothèses $a = g \times m + u$ et $e + u = S\,i \times b$, deux introductions donnent $B$, et deux éliminations concluent.

(ii) Existence. Le point (iii) de Plus petit élément, division, appliqué au terme $a$ et au module $m$, avec deux variables nouvelles, et l'élimination fournissent $g$ et $d$ tels que $g \times m + d = a$ et $d < m$. Alors $d \leqslant S\,i \times b$, et l'élimination fournit $e$ tel que $e + d = S\,i \times b$. Avec la symétrie de l'égalité, $a = g \times m + d$, et trois introductions de l'existentiel, avec les termes $e$, $g$ et $d$, donnent $\exists u\, B(a, b, i, u)$. On élimine $e$, $d$ et $g$.

Unicité. Sous les hypothèses $B(a, b, i, u)$ et $B(a, b, i, u')$, l'élimination fournit $a = g \times m + u$, $e + u = S\,i \times b$, $a = g' \times m + u'$ et $e' + u' = S\,i \times b$. Les deux dernières égalités de chaque paire donnent $u \leqslant S\,i \times b$ et $u' \leqslant S\,i \times b$, donc $u < m$ et $u' < m$. La chaîne $g \times m + u = a = g' \times m + u'$ et l'unicité de la division (Plus petit élément, division, (iii)) donnent $u = u'$.

(iii) Sous les hypothèses $a = g \times m + u$ et $e + u = S\,i \times b$, la symétrie donne $g \times m + u = a$, d'où $u \leqslant a$, avec le témoin $g \times m$, et $u \leqslant S\,i \times b$, avec le témoin $e$.

(iv) L'élimination des hypothèses fournit $c + p \times m = u + p' \times m$ et $e + u = S\,i \times b$, pour des variables nouvelles $p$, $p'$ et $e$. Le point (iii) de Plus petit élément, division, appliqué au terme $c$ et au module $m$, fournit $g$ et $d$ tels que $g \times m + d = c$ et $d < m$. La chaîne $$\begin{aligned} &(g + p) \times m + d \\ &\quad = g \times m + d + p \times m \\ &\quad = c + p \times m \\ &\quad = u + p' \times m \\ &\quad = p' \times m + u, \end{aligned}$$ avec $d < m$ et $u < m$, et l'unicité de la division donnent $d = u$. Alors $c = g \times m + u$ par le remplacement et la symétrie, et deux introductions, avec les termes $g$ et $e$, donnent $B(c, b, i, u)$. On élimine les variables introduites, qui ne figurent pas dans la conclusion.