Opérations arithmétiques

Pour $m \in \omega$ fixé, le théorème de définition par récurrence fournit des applications $n \mapsto m + n$ et $n \mapsto m \cdot n$ caractérisées par $$\begin{aligned} m + 0 &= m, \\ m + S(n) &= S(m + n), \\ m \cdot 0 &= 0, \\ m \cdot S(n) &= m \cdot n + m. \end{aligned}$$ On a alors $S(n) = n + 1$, puisque $n + 1 = n + S(0) = S(n + 0) = S(n)$.

Ces applications se rassemblent en deux lois sur $\omega$. En effet, $p = m + n$ équivaut à l'existence d'une approximation, au sens de la preuve de Définition par récurrence, pour $a = m$ et $g = S$, de domaine $S(n)$ et valant $p$ en $n$ : le graphe de l'addition est donc une partie de $(\omega \times \omega) \times \omega$ définie par séparation. Il en va de même pour la multiplication.