Puissances de 2, parité et décomposition 2ⁿ(2k + 1) dans l'arithmétique de Peano

Par le point (ii) (b) de Termes fonctionnels, il suffit d'établir chaque formule pour des variables distinctes $x$, $y$, … à la place des termes. On raisonne par chaînes d'égalités, comme au nœud Lois de + et ×, entre termes fonctionnels : le point (ii) (c) du nœud Termes fonctionnels justifie la symétrie, la transitivité et le remplacement d'un sous-terme par un terme égal.

(i) Par le point (iv) de Fonctions p.r. dans PA, $\mathrm{pw}(x, 0) = w$ équivaut à $\mathbf 1(x) = w$, c'est-à-dire à $w = S\,0$ par le point (ii) de Fonctions usuelles dans PA. Sous l'hypothèse $\mathrm{pw}(x, y) = u$, la seconde équation du même point et le point (i) de Termes fonctionnels ramènent $\mathrm{pw}(x, S\,y) = w$ à $\mathrm{mul}(u, x) = w$, c'est-à-dire, par les points (i) et (ii) de Fonctions usuelles dans PA, à $w = u \times x$ : écrite avec la valeur $u$, c'est la deuxième égalité. Pour $x = S\,S\,0$, la première donne $2^0 = S\,0$, et la seconde donne $2^{S\,y} = 2^y \times S\,S\,0 = 2^y \times S\,0 + 2^y = 2^y + 2^y$, par $\mathrm Q_7$ et le point (iii) de Lois de + et ×.

(ii) Somme des exposants. Récurrence sur $y$, avec le paramètre $x$. Pour $0$, $\mathrm Q_4$ donne $2^{x + 0} = 2^x = 2^x \times S\,0 = 2^x \times 2^0$. Pour le pas, sous l'hypothèse $2^{x + y} = 2^x \times 2^y$, on a, par $\mathrm Q_5$, (i) et la distributivité, $$\begin{aligned} 2^{x + S\,y} &= 2^{S(x + y)} \\ &= 2^{x + y} + 2^{x + y} \\ &= 2^x \times 2^y + 2^x \times 2^y \\ &= 2^x \times (2^y + 2^y) \\ &= 2^x \times 2^{S\,y}. \end{aligned}$$ Non-nullité. Récurrence sur $y$ : $2^0 = S\,0$ n'est pas nul par $\mathrm Q_1$, et, si $2^{S\,y} = 0$, alors $2^y + 2^y = 0$, puis $2^y = 0$ par le point (ii) de Lois de + et ×, contrairement à l'hypothèse de récurrence.

Majoration. Récurrence sur $y$ : $0 < S\,0$, c'est-à-dire $S\,0 \leqslant S\,0$, est la réflexivité. Sous l'hypothèse $y < 2^y$, c'est-à-dire $S\,y \leqslant 2^y$, la non-nullité et le point (v) de Ordre dans PA, avec $0 \leqslant 2^y$, donnent $0 < 2^y$, c'est-à-dire $S\,0 \leqslant 2^y$. La compatibilité de l'ordre avec l'addition, point (vi) du même nœud, appliquée deux fois avec la commutativité, et la transitivité donnent $S\,y + S\,0 \leqslant 2^y + 2^y$, c'est-à-dire $S\,S\,y \leqslant 2^{S\,y}$, puisque $S\,y + S\,0 = S(S\,y + 0) = S\,S\,y$ : c'est $S\,y < 2^{S\,y}$.

(iii) Imparité. Montrons $\forall u\, \neg(x + x = \mathrm O(u))$ par récurrence sur $x$, où $u$ est une variable distincte de $x$. Pour $0$, $0 + 0 = 0$, et $\mathrm O(u) = 0$ contredirait $\mathrm Q_1$. Pour le pas, raisonnons sous l'hypothèse de récurrence et sous $S\,x + S\,x = \mathrm O(u)$. Par le point (i) de Lois de + et × et $\mathrm Q_5$, $S\,x + S\,x = S(x + S\,x) = S\,S(x + x)$, et $\mathrm Q_2$ donne $S(x + x) = u + u$. Si $u = 0$, alors $S(x + x) = 0$, contraire à $\mathrm Q_1$. Sinon, l'instance $\neg(u = 0) \to \exists a\, (u = S\,a)$ de $\mathrm Q_3$ et l'élimination fournissent $a$ tel que $u = S\,a$ ; le même calcul donne $u + u = S\,S(a + a)$, puis $x + x = S(a + a) = \mathrm O(a)$ par $\mathrm Q_2$, ce que l'hypothèse de récurrence, instanciée par $a$, exclut. La généralisation en $u$, qui n'est pas libre dans l'hypothèse de récurrence, et le point (iii) de Récurrence dans PA concluent.

Simplification. Par $\mathrm Q_7$ et le point (iii) de Lois de + et ×, $x \times S\,S\,0 = x + x$ ; le point (iv) du même nœud, avec $r = S\,0$, donne $x \times S\,S\,0 = y \times S\,S\,0 \to x = y$.

(iv) Existence. Notons $\varphi$ la formule $\neg(N = 0) \to \exists n\, \exists k\, (N = 2^n \times \mathrm O(k))$, et appliquons la récurrence forte (Plus petit élément, division, (ii)), avec $\Gamma$ vide : il suffit de démontrer $\varphi$ sous l'hypothèse $H = \forall y \leqslant N\ (y = N \vee \varphi[y/N])$, où $y$ est nouvelle. Sous $H$ et $\neg(N = 0)$, la division euclidienne par $S\,S\,0$, point (iii) du même nœud, et l'élimination fournissent $g$ et $d$ tels que $g \times S\,S\,0 + d = N$ et $d < S\,S\,0$. Par le point (v) de Ordre dans PA, $d \leqslant S\,0$, et le point (ii) du même nœud, appliqué deux fois, donne $d = 0$ ou $d = S\,0$ ; d'autre part $g \times S\,S\,0 = g + g$.

Si $d = S\,0$, alors $N = (g + g) + S\,0 = \mathrm O(g)$ par $\mathrm Q_5$ et $\mathrm Q_4$, et $2^0 \times \mathrm O(g) = S\,0 \times \mathrm O(g) = \mathrm O(g)$ ; deux introductions, avec les termes $0$ et $g$, concluent. Si $d = 0$, alors $N = g + g$. On a $\neg(g = 0)$, sinon $N = 0 + 0 = 0$ ; $g \leqslant N$, par le point (i) de Ordre dans PA ; et $\neg(g = N)$, sinon $g + g = g + 0$ et la simplification donnerait $g = 0$. Le point (vii) (a) du même nœud, appliqué à $H$ avec le terme $g$, donne $g = N \vee \varphi[g/N]$, et $\neg(g = N)$ écarte le premier cas ; d'où $n$ et $k$ tels que $g = 2^n \times \mathrm O(k)$, par l'élimination. Alors, par la distributivité et (i), $$\begin{aligned} N &= 2^n \times \mathrm O(k) + 2^n \times \mathrm O(k) \\ &= (2^n + 2^n) \times \mathrm O(k) \\ &= 2^{S\,n} \times \mathrm O(k), \end{aligned}$$ et deux introductions, avec les termes $S\,n$ et $k$, concluent. Le raisonnement par cas et l'élimination des variables introduites donnent $\{H\} \vdash_{\mathsf{PA}} \varphi$.

Unicité. On note d'abord que, pour tout terme fonctionnel $c$, (i) et la distributivité donnent $2^{S\,m} \times c = 2^m \times c + 2^m \times c$, et $2^0 \times \mathrm O(k) = \mathrm O(k)$. Soit $\psi$ la formule $\forall n'\, \forall k\, \forall k'\, \big(2^n \times \mathrm O(k) = 2^{n'} \times \mathrm O(k') \to (n = n' \wedge k = k')\big)$ ; montrons-la par récurrence sur $n$. Dans chaque cas, on raisonne sous l'hypothèse de l'égalité, et l'on distingue $n' = 0$ et $n' = S\,m'$, par l'instance de $\mathrm Q_3$.

Pour $n = 0$ : si $n' = 0$, l'égalité est $\mathrm O(k) = \mathrm O(k')$, et $\mathrm Q_2$ et (iii) donnent $k = k'$ ; si $n' = S\,m'$, elle s'écrit $\mathrm O(k) = c' + c'$, avec $c' = 2^{m'} \times \mathrm O(k')$, ce que (iii) exclut. Pour le pas, sous l'hypothèse $\psi$, l'égalité s'écrit $c + c = 2^{n'} \times \mathrm O(k')$, avec $c = 2^n \times \mathrm O(k)$ : si $n' = 0$, (iii) l'exclut ; si $n' = S\,m'$, elle devient $c + c = c' + c'$, donc $c = c'$ par (iii), et $\psi$, instanciée par $m'$, $k$ et $k'$, donne $n = m'$ et $k = k'$, d'où $S\,n = n'$. La généralisation en $n'$, $k$, $k'$, puis le point (iii) de Récurrence dans PA et l'instanciation concluent.