Les instances de tautologies forment un ensemble primitif récursif

(i) $\mathrm{Prem}(N) \iff \mathrm{At}(N) \vee \big(\mathrm{Fm}(N) \wedge (N)^0 = 3\big)$, par Formules.

(ii) Notons $l = \mathrm{lg}(N)$ et $d = \mathrm{dec}(N)$ (Formules, (iii)), et définissons $G(s, N, h)$ par cas :

$\mathrm{bit}(s, N)$ si $\mathrm{Prem}(N)$ ;

$1 \mathbin{\dot{-}} (h)^{\mathrm{sm}(N, 1, l)}$ si $\mathrm{Fm}(N)$ et $(N)^0 = 1$ ;

$1 \mathbin{\dot{-}} \big((h)^{\mathrm{sm}(N, 1, d)} \cdot (1 \mathbin{\dot{-}} (h)^{\mathrm{sm}(N, d, l)})\big)$ si $\mathrm{Fm}(N)$ et $(N)^0 = 2$ ;

$0$ dans tous les autres cas.

Ces quatre relations partagent $\mathbb N^3$, et $G$ est primitive récursive par la définition par cas (Clôture, (ii)). La récurrence de valeurs, avec le paramètre $s$, fournit une fonction primitive récursive $\mathrm{Val}$ telle que $\mathrm{Val}(s, N) = G(s, N, \overline{\mathrm{Val}}(s, N))$.

Montrons $\mathrm{Val}(s, \ulcorner \varphi \urcorner) = \bar v_s(\varphi)$ par récurrence forte sur le code. Si $\varphi$ est première, c'est la définition de $v_s$. Si $\varphi = \neg\varphi_1$, le facteur $\mathrm{sm}(N, 1, l)$ est $\ulcorner \varphi_1 \urcorner < N$, et la valeur est $1 - \bar v_s(\varphi_1)$ par hypothèse de récurrence.

Si $\varphi = {\to}\, \varphi_1\, \varphi_2$, le point (iii) de Formules donne $\mathrm{sm}(N, 1, d) = \ulcorner \varphi_1 \urcorner$ et $\mathrm{sm}(N, d, l) = \ulcorner \varphi_2 \urcorner$, codes plus petits que $N$. La valeur $1 - a(1 - b)$, avec $a = \bar v_s(\varphi_1)$ et $b = \bar v_s(\varphi_2)$, vaut $0$ si et seulement si $a = 1$ et $b = 0$ : c'est $\bar v_s(\varphi)$.

(iii) La relation écrite est primitive récursive : la quantification est bornée par la fonction primitive récursive $N \mapsto 2^{N+1}$ (Clôture, (i) et (iii)). Montrons qu'elle définit les instances de tautologies.

Si $\varphi$ en est une, $\bar v(\varphi) = 1$ pour toute valuation $v$ par le point (iii) de Instances de tautologies, en particulier pour chaque $v_s$, et (ii) conclut.

Réciproquement, soit $\varphi$ une formule de code $N$ qui vérifie la condition, et $v$ une valuation quelconque des formules premières. Soit $A$ l'ensemble des entiers $c \leqslant N$ qui codent une formule première $\pi$ telle que $v(\pi) = 1$, et $$s = \sum_{c \in A} 2^c \leqslant 2^{N+1} - 1.$$

Pour $c \leqslant N$, la somme des termes $2^{c'}$, $c' \in A$, $c' < c$, est au plus $2^c - 1$ ; par l'unicité de la division euclidienne, $q(s, 2^c)$ est la somme des $2^{c' - c}$ pour $c' \in A$, $c' \geqslant c$, qui est impaire si et seulement si $c \in A$. Ainsi $v_s(\pi) = v(\pi)$ pour toute formule première $\pi$ de code au plus $N$.

C'est le cas des formules premières qui sont des facteurs de $\varphi$, par le point (ii) du codage des mots. Par le point (ii) de Instances de tautologies, $\bar v(\varphi) = \bar v_s(\varphi) = \mathrm{Val}(s, N) = 1$. Toute valuation donne donc la valeur $1$ à $\varphi$, qui est une instance de tautologie par le point (iii) du même nœud.