Ordre et quantifications bornées dans l'arithmétique de Peano

Une formule $\exists z\, (z + t = u)$ s'obtient, par l'introduction du point (iii) de Calcul à variables libres, de toute égalité $s + t = u$ où $s$ est un terme : $z$ n'est sous aucun quantificateur dans $z + t = u$. On dit qu'on introduit $t \leqslant u$ avec le témoin $s$. Inversement, sous une hypothèse $t \leqslant u$, le point (i) de Récurrence dans PA, avec une variable nouvelle, permet de raisonner sous l'hypothèse $a + t = u$ : c'est l'élimination avec le témoin $a$.

(i) Les témoins sont $0$, $t$, $u$ et $u$ : $0 + t = t$, $t + 0 = t$, $u + t = u + t$ et $u + t = t + u$, par les points (i) de Lois de + et × et (vi) de Calcul à variables libres.

(ii) Sous l'hypothèse $a + t = 0$, le point (ii) de Lois de + et × donne $t = 0$ ; sous l'hypothèse $t = 0$, le remplacement d'un terme et $0 \leqslant 0$ donnent $t \leqslant 0$.

Sous l'hypothèse $a + t = S\,u$, on raisonne par cas sur l'instance de $\mathrm Q_3$ pour $a$, avec une variable nouvelle $b$. Si $a = 0$, la chaîne $t = 0 + t = a + t = S\,u$ donne $t = S\,u$. Si $a = S\,b$, la chaîne $S(b + t) = S\,b + t = a + t = S\,u$ et $\mathrm Q_2$ donnent $b + t = u$, et l'on introduit $t \leqslant u$ avec le témoin $b$. Réciproquement, sous l'hypothèse $a + t = u$, la chaîne $S\,a + t = S(a + t) = S\,u$ donne $t \leqslant S\,u$, avec le témoin $S\,a$ ; sous l'hypothèse $t = S\,u$, le remplacement et $S\,u \leqslant S\,u$ donnent $t \leqslant S\,u$.

(iii) Sous les hypothèses $a + t = u$ et $b + u = r$, la chaîne $b + a + t = b + (a + t) = b + u = r$ donne $t \leqslant r$, avec le témoin $b + a$. Sous les hypothèses $a + t = u$ et $b + u = t$, la chaîne $b + a + t = b + u = t = 0 + t$ et (ii) de Lois de + et × donnent $b + a = 0$, puis $a = 0$, et la chaîne $t = 0 + t = a + t = u$ conclut. Dans les deux cas, on élimine $b$, puis $a$.

(iv) Soit $x$ et $y$ deux variables distinctes, différentes des variables liées $z$ et $z'$ des deux formules $x \leqslant y$ et $y \leqslant x$. Montrons $x \leqslant y \vee y \leqslant x$ par récurrence sur $y$ ; le point (iv) de Récurrence dans PA donnera le cas de termes quelconques, puisque seules $z$ et $z'$ sont quantifiées. Pour $0$, c'est (i). Sous l'hypothèse $x \leqslant y \vee y \leqslant x$, on raisonne par cas. Si $x \leqslant y$, alors $x \leqslant S\,y$ par (ii). Sous l'hypothèse $a + y = x$, on raisonne par cas sur $a$ : si $a = 0$, la chaîne $x = a + y = 0 + y = y$, le point (i) et le remplacement donnent $x \leqslant y$, puis $x \leqslant S\,y$ par (ii) ; si $a = S\,b$, la chaîne $b + S\,y = S(b + y) = S\,b + y = x$ donne $S\,y \leqslant x$, avec le témoin $b$. Dans tous les cas, $x \leqslant S\,y \vee S\,y \leqslant x$, et le point (iii) de Récurrence dans PA conclut.

(v) Sous l'hypothèse $a + S\,t = u$, la chaîne $S\,a + t = S(a + t) = a + S\,t = u$ donne $t \leqslant u$ ; si de plus $t = u$, la chaîne $S\,a + t = u = t = 0 + t$ et la simplification donnent $S\,a = 0$, ce que $\mathrm Q_1$ exclut. Réciproquement, sous les hypothèses $a + t = u$ et $\neg(t = u)$ : si $a = 0$, alors $t = u$, ce qui est exclu ; si $a = S\,b$, la chaîne $b + S\,t = S(b + t) = S\,b + t = u$ donne $t < u$. On obtient la première équivalence.

Par (ii), $S\,t \leqslant 0$ donnerait $S\,t = 0$, contraire à $\mathrm Q_1$. Sous l'hypothèse $a + S\,t = S\,u$, la chaîne $S(a + t) = a + S\,t = S\,u$ et $\mathrm Q_2$ donnent $a + t = u$ ; sous l'hypothèse $a + t = u$, la chaîne $a + S\,t = S(a + t) = S\,u$ donne $S\,t \leqslant S\,u$. La trichotomie découle de (iv) et de la première équivalence, appliquée à $t \leqslant u$ et à $u \leqslant t$, par la symétrie de l'égalité, qui fait passer de $u = t$ à $t = u$, et la règle des tautologies. Enfin, $t < u$ et $u \leqslant t$ donneraient $t \leqslant u$, puis $t = u$ par (iii), contre $\neg(t = u)$.

(vi) Sous l'hypothèse $a + t = u$, la chaîne $a + (t + r) = a + t + r = u + r$ donne $t + r \leqslant u + r$, et la chaîne $a \times r + t \times r = (a + t) \times r = u \times r$ donne $t \times r \leqslant u \times r$. Sous l'hypothèse $a + (t + r) = u + r$, la chaîne $a + t + r = a + (t + r) = u + r$ et la simplification donnent $a + t = u$. Sous les hypothèses $\neg(r = 0)$ et $r = S\,b$, la chaîne $t \times b + t = t \times S\,b = t \times r$ donne $t \leqslant t \times r$, avec le témoin $t \times b$ ; l'élimination de $b$ et l'instance de $\mathrm Q_3$ concluent.

(vii) (a) La formule $\forall x \leqslant t\ \varphi$ est $\forall x\, (\exists z\, (z + x = t) \to \varphi)$. Le terme $u$ y est substituable à $x$ dans la formule qui suit $\forall x$ : les occurrences libres de $x$ y sont dans $z + x = t$, sous le seul quantificateur $\exists z$, et $z$ ne figure pas dans $u$, ou dans $\varphi$, où $u$ est substituable. Comme $x \neq z$ et que $x$ ne figure pas dans $t$, le résultat est $u \leqslant t \to \varphi[u/x]$, et l'axiome (2) donne la première formule. La seconde s'obtient en appliquant la première à $\neg\varphi$, avec l'instance $(P \to (Q \to \neg R)) \to (Q \to (R \to \neg P))$.

(b) Le théorème de la déduction donne $\Gamma \vdash_{\mathsf{PA}} x \leqslant t \to \varphi$, et la généralisation du point (i) de Récurrence dans PA donne la première assertion. Pour la seconde, (c) ci-dessous ramène l'hypothèse à $\exists x\, (x \leqslant t \wedge \varphi)$, et la formule $(x \leqslant t \wedge \varphi)[b/x]$ est $b \leqslant t \wedge \varphi[b/x]$ ; l'élimination avec la variable nouvelle $b$, du même point (i), conclut.

(c) La formule $\exists x \leqslant t\ \varphi$ est $\neg\forall x\, (B \to \neg\varphi)$, avec $B = (x \leqslant t)$, et $\exists x\, (B \wedge \varphi)$ est $\neg\forall x\, \neg\neg(B \to \neg\varphi)$, puisque $B \wedge \varphi$ abrège $\neg(B \to \neg\varphi)$. Les instances $P \to \neg\neg P$ et $\neg\neg P \to P$ et la monotonie du point (ii) de Récurrence dans PA donnent $\vdash \forall x\, (B \to \neg\varphi) \leftrightarrow \forall x\, \neg\neg(B \to \neg\varphi)$, et la contraposition conclut.

(d) Sous l'hypothèse $\forall x \leqslant S\,t\ \varphi$ : (a), avec le terme $S\,t$ et $S\,t \leqslant S\,t$, donne $\varphi[S\,t/x]$ ; sous l'hypothèse supplémentaire $x \leqslant t$, le point (ii) donne $x \leqslant S\,t$, et (a), avec le terme $x$, donne $\varphi$ ; comme $x$ n'est pas libre dans $\forall x \leqslant S\,t\ \varphi$, (b) donne $\forall x \leqslant t\ \varphi$. Réciproquement, sous les hypothèses $\forall x \leqslant t\ \varphi$, $\varphi[S\,t/x]$ et $x \leqslant S\,t$, le point (ii) donne $x \leqslant t$ ou $x = S\,t$ : dans le premier cas, (a) donne $\varphi$ ; dans le second, le remplacement d'un terme, appliqué à $\varphi$ avec les termes $S\,t$ et $x$, et la symétrie donnent $\varphi$. Le point (b) conclut. Pour la borne $0$, on raisonne de même avec $t \leqslant 0 \leftrightarrow t = 0$. La formule existentielle s'obtient en appliquant la formule universelle à $\neg\varphi$, avec $(\neg\varphi)[S\,t/x] = \neg\,\varphi[S\,t/x]$ et l'instance $(A \leftrightarrow (B \wedge \neg C)) \to (\neg A \leftrightarrow (\neg B \vee C))$.

(e) Sous les hypothèses de $\Gamma$, $\forall x \leqslant t\ \varphi$ et $x \leqslant t$, le point (a), avec le terme $x$, donne $\varphi$, puis $\psi$, et (b) donne $\forall x \leqslant t\ \psi$. Pour la borne, sous les hypothèses $t \leqslant u$, $\forall x \leqslant u\ \varphi$ et $x \leqslant t$, (iii) donne $x \leqslant u$, puis (a) donne $\varphi$, et (b) conclut, $x$ n'étant libre ni dans $t \leqslant u$ ni dans $\forall x \leqslant u\ \varphi$. Les formules existentielles s'obtiennent en appliquant les formules universelles à $\neg\psi \to \neg\varphi$ et à $\neg\varphi$, par contraposition.