Chapitre 21

Introduction

Les mathématiques à rebours<fnref n="1" /> sont un ensemble d'outils provenant de la théorie de la preuve et de la calculabilité pour analyser le contenu calculatoire des théorèmes mathématiques. Elles permettent de répondre à des questions méta-mathématiques fondamentales telles que : « Quels sont les axiomes optimaux pour prouver les théorèmes ordinaires ? », ou bien : « Quel sens donner à l'implication d'un théorème par un autre ? »

1. Quête des axiomes optimaux

La quête des axiomes optimaux pour prouver les théorèmes usuels est la motivation historique des mathématiques à rebours, telles que conçues par Harvey Friedman en 1975-1976. Comme nous l'avons vu dans le chapitre 9 sur la crise des fondements, les développements de la théorie des ensembles repoussant les limites de l'intuition, on a vu naître des paradoxes semant le doute dans la solidité de l'édifice des mathématiques. La crise des fondements a connu son paroxysme avec le second théorème d'incomplétude de Gödel, énonçant qu'une théorie calculatoire énumérable cohérente capable de parler des entiers naturels,

<figure><img src="image_134.png" /><figcaption>Harvey Friedman, 1948–</figcaption></figure>

<footnote n="1">1. « Reverse mathematics », en anglais.</footnote>
ne pouvait prouver sa propre cohérence. Les mathématiciens sont donc condamnés à reléguer la cohérence des mathématiques au niveau de croyance, justifiée uniquement par l'absence de contradiction repérée à ce jour malgré un usage intensif des mathématiques au quotidien.

Les théorèmes peuvent donc être vus comme des édifices de connaissances construits sur la croyance en la cohérence d'un système d'axiomes. Plus la preuve d'un théorème fera appel à des axiomes forts, plus fragile sera cette connaissance. La démarche de Friedman consista donc à essayer de maîtriser ces risques, en déterminant quels théorèmes seraient invalidés si l'on devait renoncer à certains axiomes. En d'autre termes, il s'agissait de déterminer le niveau de fiabilité des théorèmes, en réponse directe à la crise des fondements. La question historique des mathématiques à rebours fut donc la suivante.

« Quels sont les *axiomes optimaux* permettant de prouver les théorèmes des *mathématiques ordinaires* ? »

Cette question comporte plusieurs composants importants sur lesquels il convient de s'arrêter.

Tout d'abord, qu'entend-on par « mathématiques ordinaires » ? Il est important de comprendre que la démarche de Friedman était avant tout empirique et ne recherchait pas l'exhaustivité : il ne s'agit pas d'être capable d'analyser la puissance axiomatique des tout derniers résultats de théorie des ensembles, qui est une branche méta-mathématique à puissance logique très éloignée des mathématiques traditionnelles. Il s'agit plutôt d'étudier les mathématiques « de la vie de tous les jours », comme les théorèmes usuels d'algèbre ou d'analyse.

Comment prouver qu'un ensemble d'axiomes est optimal pour prouver un théorème ? Analyser avec soin la preuve du théorème pour en identifier les hypothèses ou les axiomes ne suffit pas. Il peut très bien exister une nouvelle preuve faisant appel à des axiomes plus élémentaires. La notion d'axiome optimal n'est donc pas une propriété relative à une preuve, mais à un théorème. Soient $A_1, \dots, A_n$ des axiomes suffisants pour prouver un théorème $T$. Autrement dit, $A_1 \wedge \dots \wedge A_n \rightarrow T$. Pour s'assurer que les axiomes sont nécessaires, il suffit de prouver l'implication inverse (d'où le nom de « mathématiques à rebours »). On se retrouve alors avec l'équivalence

$$A_1 \wedge \dots \wedge A_n \leftrightarrow T$$

## 1.1. Choix d'une théorie de base

La démarche serait probablement vouée à l'échec si l'on se restreignait à l'implication logique sans fixer une théorie de base. L'implication logique est en effet une relation très fine qui placerait chaque théorème — et même différentes formulations d'un même théorème — dans des « degrés
logiques » différents. Il est naturel de chercher à s'abstraire des détails de
formulation et de travailler modulo des opérations « élémentaires » : nos
implications logiques pourront s'établir relativement à une théorie de base
permettant de réaliser ces opérations élémentaires. Il convient d'être pru-
dent dans le choix de cette théorie : si celle-ci est trop forte — par exemple si
elle permet déjà de prouver la plupart des théorèmes —, la valeur informa-
tive d'une implication $P \to Q$, relativement à cette théorie, sera affaiblie.

C'est là qu'intervient la calculabilité : nous allons fixer une théorie de
base, RCA₀, capturant les mathématiques calculables. Le choix de cette
théorie définit l'interprétation sémantique de la relation d'implication. Par
exemple, si l'on considère que la théorie de Zermelo-Fraekel (ZF) représente
les mathématiques consensuelles, c'est-à-dire les mathématiques largement
acceptées par la communauté, une implication ZF $\vdash P \to Q$ signifie que
consensuellement, si l'on admet P, alors on admettra Q. De la même
manière, une preuve de RCA₀ $\vdash P \to Q$ signifie que si l'on fait confiance
aux mathématiques calculables, et si l'on admet P, alors il est logique de
considérer Q comme vrai. En pratique, la théorie RCA₀ est beaucoup plus
faible que ZF, et en particulier beaucoup de théorèmes classiques ne sont
pas prouvables dans RCA₀, comme nous allons le voir.

## 1.2. Arithmétique du second ordre

Pour mener à bien le programme historique des mathématiques à rebours,
à savoir la quête des axiomes optimaux, il faut fixer un cadre formel, à com-
mencer par le choix d'un langage. À première vue, le choix le plus évident est
celui d'une théorie fondationnelle comme celle de la théorie des ensembles.
En effet, comme nous l'avons vu dans la section 9-4, le langage ensem-
bliste permet une formalisation unifiée de la totalité des mathématiques.
Le choix des mathématiques à rebours s'est cependant porté sur le langage
de l'arithmétique du second ordre, c'est-à-dire un langage où l'on manipule
et quantifie sur les entiers naturels et les ensembles d'entiers.

Ce choix peut paraître surprenant : les ensembles d'entiers naturels étant
par nature dénombrables, l'arithmétique du second ordre ne peut manipu-
ler que des objets dénombrables. Comment alors parler des objets usuels
qui ne le sont pas, comme les fonctions de $\mathbb{R}$ dans $\mathbb{R}$ ? Ce n'est de fait
pas possible en toute généralité, mais les travaux de Hilbert et Bernays,
*Grundlagen der Mathematik* (1934-1936), ont montré qu'une grande par-
tie des mathématiques pouvait être formalisée, modulo un codage appro-
prié, dans l'arithmétique du second ordre. Ainsi, par exemple les fonctions
*continues* — et même boréliennes — de $\mathbb{R}$ dans $\mathbb{R}$ admettent toutes une
représentation dénombrable. Rappelons que le but des mathématiques à
rebours n'est pas d'être exhaustif, mais de rendre compte d'une tendance
générale des mathématiques.
En contrepartie de cette légère perte de généralité, l'arithmétique du second ordre présente un avantage considérable : les objets mathématiques manipulés étant tous représentés par des entiers et des ensembles d'entiers, nous pouvons bénéficier des outils de la calculabilité pour parler de la complexité des axiomes. Il existe en effet une notion robuste de calculabilité sur les entiers, et notamment une caractérisation des ensembles calculables comme ceux définissables par des prédicats $Δ_1^0$. Les différentes représentations d'un même théorème dans l'arithmétique du second ordre à l'aide de différentes fonctions de codage n'auront en pratique pas d'impact sur la force du théorème, car la plupart des codages sont calculables, et donc équivalents dans la théorie de base $RCA_0$.

### 1.3. Phénomène de structure

Depuis le lancement des mathématiques à rebours, des centaines de théorèmes ont été analysés, provenant de toutes les branches des mathématiques. On retrouvera cette démarche dans l'excellent ouvrage de Steven Simpson, *Subsystems of Second-Order Arithmetics*. L'étude systématique des théorèmes classiques sous l'angle des mathématiques à rebours a laissé entrevoir deux observations empiriques :

*La plupart des théorèmes ordinaires requièrent une puissance axiomatique faible.* Cette observation peut être vue comme une réponse partielle à la crise des fondements, en délivrant un message d'optimisme : oui, la théorie de l'arithmétique est incomplète et nous devons nous contenter d'une croyance expérimentale en sa cohérence, oui, l'ajout d'axiomes à cette théorie ne fait potentiellement qu'empirer les risques, mais la plupart des théorèmes usuels ne requièrent qu'une partie « faible » de ces axiomes supplémentaires. Les mathématiques sont donc robustes face à d'éventuelles incohérences dues à des axiomes trop forts.

*Les mathématiques sont calculatoirement très structurées.* Plus précisément, il existe quatre grands systèmes d'axiomes, linéairement ordonnés par l'implication modulo $RCA_0$, tels que si l'on prend un théorème classique au hasard 2, il y a de fortes chances pour qu'il soit équivalent à l'un des quatre systèmes modulo $RCA_0$, ou bien même déjà prouvable dans $RCA_0$. On appelle cette observation le *phénomène du Club des cinq* (Big Five, en anglais).

Cette seconde observation est cependant à relativiser. Il existe des contre-exemples — provenant notamment de la théorie de Ramsey — se comportant de manière beaucoup plus chaotique. Cela a conduit certains chercheurs à soulever l'objection selon laquelle le phénomène de structure observé en mathématiques à rebours relève d'un biais humain, et que cette structure serait davantage celle du cerveau des mathématiciens que des mathématiques elles-mêmes.

<footnote n="2">2. « Hasard » est à prendre au sens informel du terme. Il s'agit d'une observation empirique et non d'un résultat de probabilités.</footnote>
## 2. Comparaison des théorèmes

Les mathématiques à rebours ont petit à petit évolué, et de nombreuses branches sont nées sur le terreau originel de la recherche de l'optimalité des axiomes. Une grande partie de la discipline consiste en la comparaison et en la classification des théorèmes. Il est courant en mathématiques d'entendre des énoncés comme « les théorèmes A et B sont équivalents », ou encore « le théorème A n'est pas une conséquence du théorème B ». Les mathématiques à rebours permettent de donner un sens précis à ces affirmations informelles.

D'un point de vue purement logique, tous les théorèmes sont équivalents, au sens où ils sont tous interprétés par la valeur de vérité vrai. Quel sens donner à l'intuition de l'implication ou de l'équivalence entre deux théorèmes ? On pourrait par exemple considérer qu'un théorème $T_0$ implique un autre théorème $T_1$ si la preuve de $T_1$ fait intervenir l'énoncé $T_0$. Cependant, il est possible de remplacer chaque occurrence de $T_0$ par sa preuve, dans la preuve de $T_1$ pour obtenir une nouvelle démonstration ne faisant pas intervenir $T_0$. Cette tentative de formalisation n'est donc pas la bonne.

Si l'on en revient à l'intuition première, un théorème $T_0$ implique un théorème $T_1$ si $T_1$ peut être prouvé de manière élémentaire, en faisant appel à $T_0$ comme une boîte noire. Les mathématiques à rebours permettent justement de formaliser la notion de raisonnement élémentaire à l'aide du système $RCA_0$. Il est alors possible de donner un sens formel à l'implication $T_0 \rightarrow T_1$ en la prouvant dans $RCA_0$. Les mathématiques à rebours, initialement conçues pour identifier les axiomes nécessaires aux mathématiques, deviennent un outil de classification de théorèmes.

**Exemple 2.1.** On trouvera dans la littérature des affirmations comme « Le théorème des valeurs intermédiaires est une conséquence de la propriété de la borne supérieure ». Une version faible du théorème des valeurs intermédiaires — le théorème de Bolzano — affirme que si une fonction $f : \mathbb{R} \rightarrow \mathbb{R}$ est continue sur un intervalle $[a, b]$ avec $f(a) < 0$ et $f(b) > 0$, alors il existe $c \in [a, b]$ tel que $f(c) = 0$. La propriété de la borne supérieure affirme que toute partie de $\mathbb{R}$ non vide et majorée admet une borne supérieure.

Supposons la propriété de la borne supérieure afin de montrer le théorème de Bolzano. Soit $f : \mathbb{R} \rightarrow \mathbb{R}$ une fonction continue telle que $f(a) < 0$ et $f(b) > 0$. Soit $S = \{x \in [a, b] : f(x) < 0\}$. L'ensemble $S$ contient $a$ et est majoré par $b$, donc il admet une borne supérieure $c$.

En supposant par l'absurde $f(c) \neq 0$, alors pour un intervalle ouvert $I$ tel que $f(c) \in I$ avec $\max I < 0$, on a par continuité de $f$ un intervalle ouvert $J$ contenant $c$ tel que $f(J) \subseteq I$.
L'inégalité $c < \sup J$ contredit la qualité de borne supérieure à $c$. Par conséquent, $f(c) = 0$.

L'exemple précédent est une démonstration « élémentaire » (RCA₀ donnera un sens précis à cela) du théorème de Bolzano à partir de la propriété de la borne supérieure. Du point de vue des mathématiques à rebours, ces théorèmes doivent se formaliser dans le langage de l'arithmétique du second ordre. Une fonction continue pourra être représentée par un encodage de tous les ouverts $f^{-1}([)a, b[)$, pour des rationnels $a < b$ quelconques. La propriété de borne supérieure ne peut pas se formaliser pour des ensembles de réels quelconques, mais on pourra la formaliser pour toutes les classes boréliennes, qui peuvent se coder par des objets dénombrables.

L'intérêt de l'implication dans RCA₀ pour classifier les théorèmes reste cependant relativement limité, dans la mesure où la plupart des théorèmes sont équivalents à cinq grands ensembles d'axiomes. Il existe toutefois des raffinements de l'implication où l'on va contrôler les utilisations de $T_0$ dans la preuve de $T_1$, ou même interdire les analyses de cas. Ces restrictions aboutissent respectivement à la réduction calculatoire et la réduction de Weihrauch, que nous verrons en détail dans cette partie. De nos jours, les mathématiques à rebours ont pris un sens plus large, et forment une bannière sous laquelle se regroupent la démarche fondationnelle de recherche des axiomes optimaux et la classification des théorèmes à travers différentes réductions calculatoires.
Chapitre 22

Arithmétique du second ordre

L'arithmétique du second ordre, no-
tée Z₂, est une théorie introduite par
Hilbert et Bernays dans *Grundlagen*
der *Mathematik*, permettant de parler
des entiers et des ensembles d'entiers.
Bien que la théorie ne manipule que des
objets dénombrables, Hilbert et Ber-
nays ont montré qu'une grande par-
tie des mathématiques classiques était
déjà prouvable dans Z₂. Les axiomes
de l'arithmétique du second ordre qui
sont relatifs aux entiers (et ne parlent
pas des ensembles d'entiers) coïncident
avec ceux de l'arithmétique de Peano.
La théorie Z₂ n'en est pas pour autant
une *extension conservative* de PA (voir
la définition 23-6.1) : il existe des for-
mules ne faisant intervenir que des entiers naturels qui sont prouvables
dans Z₂ mais pas dans PA, à commencer par l'énoncé de la cohérence
de PA.
Paul Bernays, 1888-1977

<figure><img src="image_135.png" /><figcaption>Paul Bernays, 1888-1977</figcaption></figure>

Dans ce chapitre, nous allons étudier plusieurs sous-systèmes de l'arithmé-
tique du second ordre qui se sont révélés particulièrement importants en
mathématiques à rebours.
# 1. Langage de $Z_2$

Le langage de l'arithmétique du second ordre correspond à celui de l'arithmétique de Peano, augmenté de variables sur les ensembles d'entiers, de quantificateurs sur ces ensembles, et de la relation binaire d'appartenance entre un entier et un ensemble.

**Définition 1.1.** Le langage $\mathcal{L}_{Z_2}$ de l'arithmétique du second ordre comprend :

(1) des symboles de variables du premier ordre $x, y, z, \dots$ pour les entiers naturels;

(2) des symboles de variables du second ordre $X, Y, Z, \dots$ pour les ensembles d'entiers;

(3) les symboles de connecteurs logiques : $\wedge, \vee, \to, \neg$ et les parenthèses ($$);

(4) les symboles de quantificateurs sur les entiers et sur les ensembles d'entiers : $\forall, \exists$;

(5) les symboles de fonctions binaires sur les entiers suivants : $+, \times$;

(6) les symboles de relations binaires sur les entiers suivants : $=, <$;

(7) le symbole de relation d'appartenance : $\in$;

(8) des symboles de constantes $0, 1$.

◇

Le langage de l'arithmétique du second ordre est dit à deux sortes, au sens où il manipule deux types d'objets distincts : les entiers (premier ordre), et les ensembles d'entiers (second ordre). On distingue donc deux types de termes : les termes du premier ordre et ceux du second ordre.

**Définition 1.2.** Les termes du premier ordre de $Z_2$ sont définis inductivement de la manière suivante.

(1) Une variable du premier ordre ou une constante est un terme du premier ordre.

(2) Si $t_1, t_2$ sont des termes du premier ordre, alors $(t_1+t_2)$ et $(t_1 \times t_2)$ en sont aussi.

Les termes du second ordre sont simplement les variables du second ordre. ◇

La simplicité des termes du second ordre provient de l'absence de fonctions sur les ensembles d'entiers dans le langage de l'arithmétique du second ordre. Si l'on avait ajouté le symbole de réunion $\cup$, on aurait alors considéré $(X \cup Y) \cup Z$ comme un terme du second ordre. Les opérations ensemblistes standard pourront toutefois être définies à l'aide de certains axiomes.
**Exemple 1.3.** Les expressions suivantes sont des termes du premier ordre : $x$, (((((x + ı) + ı) + ı) × ı) + ı), (ı + 0), (x + (y × z)). Les seuls termes du second ordre sont les variables du second ordre.

Comme pour l'arithmétique de Peano, si les symboles de fonction sont utilisés pour créer les termes du langage, les symboles de relation sont eux utilisés pour créer les *formules* du langage.

**Définition 1.4.** Les *formules de l'arithmétique du second ordre* sont définies de la manière suivante.

(1) Pour tous termes du premier ordre $t_1, t_2$ et tout terme du second ordre $X$, alors $t_1 = t_2$, $t_1 < t_2$, et $t_1 \in X$ sont des formules. Ces formules sont appelées *formules atomiques*.

(2) Pour toutes formules $F_1, F_2$, alors $(F_1 \land F_2), (F_1 \lor F_2), (F_1 \rightarrow F_2)$ et $\neg F_1$ sont des formules.

(3) Pour toute formule $F$, alors $\forall x F, \exists x F, \forall XF \text{ et } \exists XF$ sont des formules.

<figure><img src="image_136.png" /></figure>

**Exemple 1.5.** La formule

$$ \forall X (|0 \in X \land \forall y (y \in X \rightarrow y + ı \in X)| \rightarrow \forall z z \in X) $$

exprime l'induction.

Une formule est *close* si elle ne possède aucune variable libre. Sauf spécifié autrement, on ne supposera pas par défaut qu'une formule est close.

## Formules et variables libres

Souvenons-nous de la notation $F(x)$ signifiant que $x$ est libre dans $F$. Afin de ne pas alourdir certains énoncés, on ne rendra pas toujours explicites toutes les variables libres de $F$. Ce sera par exemple le cas pour des formules $F(x) \equiv G(X_1, \dots, X_s, a_1, \dots, a_t, x)$ où $X_1, \dots, X_s$ et $a_1, \dots, a_t$ sont des variables libres, respectivement du second et du premier ordre, qui auront vocation à être remplacées par des *paramètres* dans une certaine structure.

Rappelons que les formules de l'arithmétique du second ordre peuvent être hiérarchisées en fonction de leurs alternances de quantificateurs. En particulier, une formule *arithmétique* est une formule de $\mathcal{L}_{Z_2}$ où seuls les quantificateurs sur les entiers sont autorisés, bien que la formule puisse contenir des variables libres du premier ou du second ordre (voir la section 10-1).
## 2. La théorie $\mathbb{Z}_2$

Venons-en aux axiomes de l'arithmétique du second ordre. On y retrouve les axiomes de l'arithmétique de Robinson, pour régir le comportement des entiers naturels et des opérations usuelles (voir la section 9-2.3). Nous les redonnons ici à des fins de complétude :

(1) $\forall x \neg(x + \dot{i} = \dot{0})$

(2) $\forall x (x = \dot{0} \lor \exists y (x = y + \dot{i}))$

(3) $\forall x \forall y (x + \dot{i} = y + \dot{i} \rightarrow x = y)$

(4) $\forall x (x + \dot{0} = x)$

(5) $\forall x \forall y (x + (y + \dot{i}) = (x + y) + \dot{i})$

(6) $\forall x (x \times \dot{0} = \dot{0})$

(7) $\forall x \forall y (x \times (y + \dot{i}) = (x \times y) + x)$

(8) $\forall x \forall y (x < y \leftrightarrow (\exists z (z \neq \dot{0} \land x + z = y)))$

Rappelons que l'on note $\mathbb{Q}$ la théorie de l'arithmétique de Robinson constituée des axiomes (1)-(8), ci-dessus.

### 2.1. Schéma de compréhension

Jusqu'ici, nous n'avons spécifié que le comportement des entiers naturels. Nous allons maintenant définir un schéma d'axiomes qui nous permettra de « construire » des ensembles, autrement dit de s'assurer que ces ensembles existeront dans tout modèle. Nous avons vu dans la définition des axiomes de la théorie des ensembles (voir la section 9-4) le schéma de compréhension restreint. Nous allons ajouter un schéma similaire pour toute formule (avec variables libres) de l'arithmétique du second ordre $F(x)$ :

$$ \exists X \forall y (y \in X \leftrightarrow F(y)). \qquad (9) $$

On supposera que la variable $X$ n'apparaît pas librement dans la formule $F$.

#### Clôture universelle des variables libres

Le schéma de compréhension s'applique à toute formule avec variables libres : toute formule $F(x) \equiv G(X_1, \dots, X_s, a_1, \dots, a_t, x)$, où $X_1, \dots, X_s$ et $a_1, \dots, a_t$ sont des variables libres, respectivement du second et du premier ordre. L'idée est alors que le schéma de compréhension doit être vrai quelles que soient les valeurs possibles des variables libres. Pour être tout à fait formel, on devrait exprimer (9) sous la forme

$$ \forall Y_1 \dots \forall Y_s \forall a_1 \dots \forall a_t \exists X \forall y (y \in X \leftrightarrow G(Y_1, \dots, Y_s, a_1, \dots, a_t, y)). $$

Afin de garder un peu de légèreté dans nos notations, il sera entendu dans la suite que l'on ne note pas toujours explicitement les variables libres, qui doivent alors être quantifiées universellement si nécessaire.

Le schéma de compréhension ajoute des ensembles calculatoirement très complexes aux modèles de l'arithmétique du second ordre. On y retrouve
par exemple toute la hiérarchie arithmétique, à commencer par le problème de l'arrêt.

**Exemple 2.1.** Le prédicat $\Phi_z(X, z) \downarrow$ correspond à une formule $\Sigma_1^0(X)$ de l'arithmétique. Donc, l'axiome de compréhension appliqué à la formule $F(G, z) \equiv \Phi_z(G, z) \downarrow$ avec un ensemble que l'on suppose existant $X$ :

$$ \exists Y \forall z (z \in Y \leftrightarrow \Phi_z(X, z) \downarrow) $$

nous garantit l'existence de $X'$.

Notons que les formules $F$ peuvent aussi contenir des quantifications du second ordre. Cela nous donne un pouvoir définitionnel considérable, que nous aborderons dans la partie IV. À l'aide de quantifications du second ordre, il sera par exemple possible de montrer l'existence de l'ω-saut Turing défini par $\emptyset^{(\omega)} = \bigoplus_n \emptyset^{(n)}$. Notons que ces quantifications du second ordre permettent de faire des définitions auto-référentes, au sens où la formule $F(x)$ peut contenir un quantificateur universel sur les ensembles d'enseigners, et donc qui prendra notamment comme valeur l'ensemble que l'on est en train de définir. La théorie de l'arithmétique du second ordre est donc un système foncièrement *imprédicatif* au sens de Poincaré (voir la section 9-1 et l'exemple 8.5).

## 2.2. Schéma d'induction

Rappelons que pour définir l'arithmétique de Peano, nous avions ajouté le schéma d'induction pour toute formule arithmétique. La tentation serait d'étendre ce schéma d'axiomes à toutes les formules de l'arithmétique du second ordre $F(x)$ avec des variables libres, à savoir :

$$ (F(\dot{0}) \land (\forall x (F(x) \rightarrow F(x + \dot{1})))) \rightarrow \forall x F(x). \quad (10) $$

Nous allons cependant utiliser un axiome qui, combiné au schéma de compréhension, implique le schéma d'induction (10) pour toute formule du second ordre.

$$ \forall X ([\dot{0} \in X \land \forall y (y \in X \rightarrow y + \dot{1} \in X)] \rightarrow \forall z z \in X). \quad (11) $$

Notons que (11) n'est pas un schéma, mais un simple axiome, dans la mesure où il n'est pas paramétré par une formule.

**Exercice 2.2.** Montrer que l'axiome d'induction sur les ensembles (11) et le schéma de compréhension (9) impliquent le schéma d'induction (10) sur les formules de l'arithmétique du second ordre. ◇
### Notation

On note $Z_2$ la théorie de l'arithmétique du second ordre, composée de $\mathbb{Q}$ (les axiomes de Robinson (1)-(8), ci-dessus), du schéma de compréhension (9) et de l'axiome d'induction (11) sur les ensembles.

Comme expliqué précédemment, malgré la simplicité de ses axiomes, Hilbert et Bernays ont montré qu'une grande partie des mathématiques traditionnelles était déjà formalisable dans $Z_2$.

## 3. Sémantiques de l'arithmétique du second ordre

Le modèle intentionnel de l'arithmétique du second ordre est bien entendu $(\mathbb{N}, \mathcal{P}(\mathbb{N}), +, \times, <, 0, 1)$, c'est-à-dire les entiers naturels et ensembles d'entiers, munis des opérations standard.

### 3.1. Le second ordre

Il existe deux notions de structures pour interpréter l'arithmétique du second ordre : les structures de Henkin et les structures pleines. Dans toute sa généralité, une structure dans le langage de l'arithmétique du second ordre spécifie deux ensembles $M$ et $S$ représentant respectivement le premier et le second ordre, ainsi que des opérations $+$, $\times$ sur $M$, une relation d'ordre $<$ sur $M$, et une relation $\in$ entre $M$ et $S$. Les structures de Henkin se restreignent aux cas où $M$ et $S$ sont disjoints et où $S \subseteq \mathcal{P}(M)$, avec $\in$ dénotant la vraie relation d'appartenance.

**Définition 3.1.** Une *structure* (de Henkin) dans $\mathcal{L}_{Z_2}$ est donnée par un tuple $M = (M, S +^M, \times^M, <^M, 0^M, 1^M)$, où $M$ et $S$ sont deux ensembles disjoints tels que $S \subseteq \mathcal{P}(M)$, $+^M, \times^M : M \times M \to M$ sont deux opérations sur $M$ et $<^M \subseteq M \times M$ est une relation sur $M$. Nous avons également la relation d'égalité sur les éléments de $M$, ainsi qu'un élément $0^M \in M$ correspondant au symbole de constante $0$ et un élément $1^M \in M$ correspondant au symbole de constante $1$. $\diamond$

Notons qu'il n'y a pas de relation d'égalité sur les ensembles. Leon Henkin a prouvé que le théorème 9-2.22 de complétude était toujours valable dans les structures qui portent son nom : on peut essentiellement se ramener à des structures du premier ordre comme vues dans la section 9-2.4 et pour lesquelles la complétude est vérifiée. Les structures usuelles du premier ordre ne contiennent qu'un seul ensemble d'éléments $E$. Pour de telles structures, on peut ajouter des prédicats $M$ et $S$ permettant de
déterminer quels éléments de $E$ sont du premier ou du second ordre, et des axiomes pour simuler le fait que l'on ait une structure de Henkin, par exemple $\forall x (M(x) \land \neg S(x)) \lor (\neg M(x) \land S(x))$ indique que tout élément est soit du premier ordre, soit du second ordre.

La sémantique standard associée à l'arithmétique du second ordre se restreint au cas particulier des structures de Henkin où le second ordre contient tous les sous-ensembles de $M$.

**Définition 3.2.** Une structure pleine dans $\mathcal{L}_{Z_2}$ est une structure de Henkin de la forme $\mathcal{M} = (M, \mathcal{P}(M), +^M, \times^M, <^M, 0^M, 1^M)$, c'est-à-dire où le second ordre est $\mathcal{P}(M)$ tout entier. ◇

Dans une structure de Henkin avec $M$ et $S \subseteq \mathcal{P}(M)$, une phrase du type $\forall X \Phi(X)$ sera vérifiée si elle l'est pour tous les éléments de $S$. Au contraire, dans une structure pleine, la quantification universelle se fait réellement sur tous les sous-ensembles de $M$. Nous verrons le genre de conséquence que cette distinction peut avoir dans le chapitre 31.

On appelle généralement sémantique standard ou sémantique des modèles pleins l'étude de l'arithmétique du second ordre où l'interprétation est restreinte aux structures pleines. La sémantique standard ne satisfait pas d' aussi bonnes propriétés que la sémantique plus générale de Henkin. En effet, il existe une formule qui fixe de manière unique ce que peut être l'ensemble $M$ des éléments du premier ordre dans une structure pleine. Il s'agit simplement de la conjonction des axiomes de Q avec l'axiome d'induction (11), ci-dessus.

$$ \forall X ((\dot{0} \in X \land \forall y (y \in X \rightarrow y + \dot{1} \in X)) \rightarrow \forall z z \in X) \land Q. \quad (a) $$

Soit $\mathcal{M} = (M, \mathcal{P}(M), +^M, \times^M, <^M, 0^M, 1^M)$ une structure satisfaisant (a). Soit $\omega = \{0^M, 1^M, 1^M + 1^M, 1^M + 1^M + 1^M, \dots \}$. Notons que $\omega \subseteq M$. Il est possible de montrer que les axiomes de Q impliquent que

$$ (\omega, +^M \upharpoonright_\omega, \times^M \upharpoonright_\omega, <^M \upharpoonright_\omega) $$

est nécessairement isomorphe aux entiers standard. L'axiome d'induction assure quant à lui que $M$ ne possède aucun autre élément que ceux de $\omega$: en prenant $X = \omega$, on obtient $\forall z \ z \in \omega$, donc $M = \omega$. Le modèle est alors forcément le modèle standard des entiers avec l'addition et la multiplication. Ainsi, le seul modèle plein de (a) est, à isomorphisme près, celui des entiers standard. Une théorie ne possédant qu'un seul modèle à isomorphisme près est dite **catégorique**. Une conséquence du corollaire 9-2.26 est que toute théorie catégorique est nécessairement complète. Le théorème 9-3.10 d'incomplétude de Gödel-Rosser affirme qu'il n'existe pas de théorie c. e. complète et cohérente qui étend PA. On en déduit que la théorie PA+(a) n'est pas c. e., ce qui est absurde. Le problème dans ce
raisonnement est le corollaire 9-2.26 qui découle du théorème 9-2.22 de compléture de Gödel : ce dernier échoue pour la sémantique standard de l'arithmétique du second ordre.

Nous considérerons donc par défaut les structures de Henkin, que nous ap-
pellerons désormais tout simplement *structures*, et qui ne seront en général
pas pleines<fnref n="1" />.

**3.2. Le premier ordre**

Comme nous l'avons vu dans la section 9-3.3 la partie du premier ordre d'un modèle de Z₂, c'est-à-dire « les entiers » du modèle, ne correspond pas nécessairement aux « vrais entiers ».

Dans n'importe quel modèle $\mathcal{M} = (M, S, +, \times, <, 0, 1)$ de $Z_2$ — nous avons supprimé l'exposant $\mathcal{M}$ pour plus de clarté — on aura nécessairement $\omega \subseteq M$ pour $\omega = \{0, 1, 1+1, \dots\}$. Comme mentionné dans la section précédente, en utilisant le fait que $(M, +, \times, <, 0, 1)$ satisfait les axiomes Q de l'arithmétique de Robinson, on construit aisément depuis l'extérieur de $\mathcal{M}$ un isomorphisme (pour l'ordre, l'addition et la multiplication) entre nos vrais entiers $\mathbb{N}$ et $\omega \subseteq M$. Il est parfaitement possible dans un tel modèle d'avoir $\omega \subsetneq M$, auquel cas $\omega$ est nécessairement un segment initial de $M$ au sens de $<$ (voir le théorème 9-3.13).

**Définition 3.3 (Entiers standard et entiers non standard)**

Soit $\mathcal{M} = (M, S, +, \times, <, 0, 1)$ un modèle de la théorie $Z_2$. Les éléments de $\omega = \{0, 1, 1+1, \dots\} \subseteq S$ sont appelés *entiers standard*, par opposition aux éléments de $M \setminus \omega$ qui sont les *entiers non standard*. Un modèle vérifiant $M \setminus \omega \neq \emptyset$ est lui-même qualifié de *non standard*. $\diamond$

**Notation**

Dans un modèle de $Z_2$, les entiers standard seront simplement
notés $0, 1, 2, \dots$. Cette notation se justifie par l'existence d'un isomor-
phisme entre $\mathbb{N}$ et la partie standard de notre modèle.

**Comprendre les modèles non standard.** Un modèle non standard de $Z_2$ contient par définition des éléments plus grands que nos entiers usuels $0, 1, 2, 3, \dots$, et dans le même temps vérifie bien tous les axiomes de $Z_2$. Il peut être difficile au départ d'avoir les idées claires sur de tels objets, pour lesquels de nombreux points peuvent sembler paradoxaux. Voyons un exemple. Il devrait être parfaitement clair que toute suite d'entiers (non strictement) décroissante est constante à partir d'un certain rang.

<footnote n="1">1. Le théorème dit de Löwenheim-Skolem, bien connu en théorie des modèles, im-
plique par exemple qu'il existe des modèles dénombrables de l'arithmétique du second
ordre.</footnote>
L'intuition immédiate que cet énoncé est vrai repose sur notre vision du
modèle standard, mais peut bien entendu aussi se démontrer : tout en-
semble d'entiers non vide possède un plus petit élément (nous verrons avec
la proposition 23-3.4 qu'il s'agit d'une conséquence de l'induction). Soit $a_i$
le plus petit élément d'une suite d'entiers $(a_n)_{n \in \mathbb{N}}$. Par hypothèse sur notre
suite, les éléments suivants sont soit égaux soit strictement inférieurs à $a_i$.
Par minimalité de $a_i$, ils ne peuvent lui être strictement inférieur. Ils lui
sont donc tous égaux, et la suite est alors constante à partir du rang $i$.

Considérons à présent un modèle $\mathcal{M} = (M, S, +, \times, <, 0, 1)$ non standard de $Z_2$ et prenons un entier non standard $x \in M$. Comme

$$x > 1, x > 2, x > 3, \dots$$

alors pour tout entier standard $n$ l'élément $x-n$ est différent de 0. On peut
donc utiliser l'axiome (2) de l'arithmétique de Robinson pour construire
inductivement la suite décroissante $x, x-1, x-2, x-3, \dots$, qui est aussi
strictement décroissante. D'après le théorème de complétude et la preuve
du paragraphe précédent, toute suite décroissante d'éléments dans tout
modèle de $Z_2$ devrait pourtant être constante à partir d'un certain rang.
Il semble donc que nous arrivions à une contradiction. Que s'est-il passé ?
On peut effectivement définir la suite $a_0 = x$ pour $x \in M$ et $a_{n+1} = a_n - 1$
pour tout $n \in \mathbb{N}$. Cette suite-là n'est toutefois infinie (et même définie) que
de l'extérieur du modèle. En effet, de l'intérieur du modèle il n'y a pas de
distinction entre entiers standard et non standard : le modèle « pense » que
tous ses éléments sont des entiers standard. Donnons-en une explication un
peu plus précise. Une suite est une fonction $f : \mathbb{N} \to \mathbb{N}$, et donc un objet du
second ordre, dont l'existence est assurée par l'axiome de compréhension,
qui doit se baser sur une formule du premier ordre $F(n, y)$ telle que pour
tout $n \in M$ il existe exactement un élément $y$ (c'est-à-dire l'élément $a_n$ de
notre suite) tel que $\mathcal{M} \models F(n, y)$. Dans une preuve destinée à être lue par
les mathématiciens, la suite ci-dessus se définit via la fonction primitive
récursive $f(0) = x$ et $f(n + 1) = \max(0, f(n) - 1)$. Il convient toutefois
de formaliser cette définition dans le langage de l'arithmétique, pour lequel
nous devons utiliser le codage de Gödel des fonctions primitives récursives
par des formules de l'arithmétique. En reprenant la fonction $\beta(a, b, i)$ du
lemme 9-3.6 permettant de coder les suites d'entiers, la formule sera la
suivante (pour plus de clarté nous avons gardé les fonctions $\max$, $\beta$ et —
telles quelles plutôt que de leur substituer les formules qui les représentent) :

$$F(n,y) \equiv (n=0 \land y=x) \lor \exists a, b \left( \begin{array}{l} y = \beta(a,b,n) \land \beta(a,b,0) = x \land \forall i < n \\ \beta(a,b,i+1) = \max(0, \beta(a,b,i) - 1) \end{array} \right).$$

Dans notre modèle de $Z_2$, la formule $F$ ci-dessus définira bien une fonction
dont le domaine est l'ensemble $M$ tout entier et non plus simplement les
entiers standard.
La suite correspondante aura donc pour segment initial $a_0, a_1, a_2, a_3, \dots$ pour tous les entiers standard 0, 1, 2, 3, ..., et vérifiera effective-ment $a_0 = x, a_1 = x-1, a_2 = x-2, a_3 = x-3, \dots$, mais du point de vue du modèle, elle sera également définie pour tous les éléments de $M$. Ainsi, l'affirmation que $(a_y)_{y \in M}$ est constante à partir d'un certain rang sera bel et bien vérifiée, simplement elle sera constante à partir d'un rang non standard, qui du point de vue du modèle est un entier tout à fait valide. Notons pour finir que la partie standard de la suite $(a_y)_{y \in M}$, telle que définie initialement depuis l'extérieur du modèle n'est pas distinguable au sein du modèle. Nous verrons en effet dans la section 23-3.2 que l'axiome d'induction implique qu'il est impossible au sein d'un modèle de distinguer ses éléments non standard des autres.

**Les $\omega$-structures.** Dans cette partie, nous nous intéresserons particulièrement à des modèles de fragments de l'arithmétique du second ordre, au sein desquels le premier ordre correspond aux entiers standard $\omega$, munis des opérations usuelles.

**Définition 3.4**

Une $\omega$-structure est une structure $\mathcal{M} = (\omega, S, +, \times, <, 0, 1)$ où $\omega$ est l'ensemble des entiers standard, $S \subseteq \mathcal{P}(\omega)$, + et $\times$ sont les opérations d'addition et de multiplication usuelles, et $<$ est l'ordre naturel. Une $\omega$-structure est donc entièrement spécifiée par l'ensemble $S$. $\diamond$

En particulier, $(\omega, \mathcal{P}(\omega), +, \times, <, 0, 1)$ est une $\omega$-structure. On aura tendance à identifier un ensemble $S \subseteq \mathcal{P}(\omega)$ avec l'-$\omega$-structure dont $S$ est le second ordre.

### 3.3. Formules à paramètres

Au cours de cette partie, nous aurons régulièrement recours à des formules à paramètres dans une structure. Intuitivement, une formule à paramètres dans une structure est une formule qui fait directement intervenir des éléments de la structure.

**Définition 3.5**

Soit $\mathcal{M} = (M, S, +^\mathcal{M}, \times^\mathcal{M}, <^\mathcal{M}, 0^\mathcal{M}, 1^\mathcal{M})$ une structure de l'arithmétique du second ordre. Une formule de $\mathcal{L}_{Z_2}$ à paramètres dans $\mathcal{M}$ est une formule dans le langage $\mathcal{L}_{Z_2} \cup \{c_n : n \in M\} \cup \{c_X : X \in S^\mathcal{M}\}$, c'est-à-dire une formule dans le langage de l'arithmétique du second ordre augmenté d'un symbole de constante pour chaque élément de la structure. $\diamond$

On aura tendance à identifier le symbole de constante et son interprétation dans la structure, et directement noter $F(n, X)$ pour $F(c_n, c_X)$ avec $n \in M$ et $X \in S^\mathcal{M}$.
Les paramètres sont étroitement liés aux variables libres des schémas d'axiomes. En effet, dans ces schémas, les variables libres sont quantifiées universellement, or une structure $\mathcal{M}$ satisfait une formule de la forme $\forall XF(X)$ ssi $\mathcal{M}$ satisfait la formule close $F(Z)$ pour chaque paramètre $Z \in \mathcal{M}$.

**Exemple 3.6.** Soit $F(X, y)$ une formule de l'arithmétique du second ordre, avec pour seules variables libres la variable d'ensemble $X$ et la variable d'entier $y$. Soit $\mathcal{M} \models Z_2$. Par le schéma de compréhension, on a

$$ \mathcal{M} \models \forall X \exists Y \forall z (z \in Y \leftrightarrow F(X, z)). $$

En particulier, pour tout paramètre $Z \in \mathcal{M}$, on a

$$ \mathcal{M} \models \exists Y \forall z (z \in Y \leftrightarrow F(Z, z)). $$

Ici, $Z$ est un paramètre et non une variable libre, et $F(Z, z)$ est une formule à paramètre.

La même nomenclature pour les variables libres et les paramètres se justifie par le fait que les premières auront normalement vocation à être remplacées par les deuxièmes dans les structures considérées.

# 4. Formaliser l'analyse dans $Z_2$

Comme mentionné précédemment, Hilbert et Bernays ont montré qu'une grande partie des mathématiques classiques pouvait se faire dans $Z_2$. Nous montrons ici comment y formaliser quelques aspects d'analyse classique. Cela nous permettra par la suite d'illustrer la force de certains sous-systèmes axiomatiques de $Z_2$ par différents théorèmes d'analyse.

## 4.1. Les rationnels

Il est courant en calculabilité de manipuler des objets finis — comme les chaînes binaires — via un système de codage par des entiers. Nous utiliserons le codage suivant pour parler des rationnels.

**Définition 4.1.** Dans $Z_2$, un rationnel est un entier de la forme $\langle i, n, m \rangle$ où $i \in \{0, 1\}$ et $m \neq 0$. Le rationnel correspondant est $n/m$ si $i = 0$ et $-n/m$ si $i = 1$. ◇

Notons que nous avons plusieurs représentations possibles pour le même rationnel, ce qui n'est pas un problème, les points importants étant les suivants. En premier lieu, il existe une formule $F_Q(x)$ de $Z_2$ qui est vraie si $x$ est un rationnel (c'est-à-dire si $x$ est un entier qui satisfait la définition ci-dessus). Pour $x$ vérifiant $F_Q$, notons $\iota_Q(x)$ le rationnel représenté par $x$.
Les opérations usuelles de manipulation de rationnels doivent pouvoir s'ex-
primer dans $Z_2$. Il nous faudra par exemple une formule $F_<$ de $Z_2$ telle
que pour tout $n_1, n_2$ vérifiant $F_Q$ on a $\iota_Q(n_1) < \iota_Q(n_2)$ ssi $F_<(n_1, n_2)$,
ou encore une formule $F_+$ telle que pour tous $n_1, n_2$ vérifiant $F_Q$, la for-
mule $F_+(n_1, n_2, r)$ est vérifiée pour un unique entier $r$ tel que $F_Q(r)$ et tel
que $\iota_Q(r) = \iota_Q(n_1) + \iota_Q(n_2)$. Les conditions ci-dessus sur les formules $F_<$
et $F_+$ sont bien sûr exprimées de l'extérieur de $Z_2$ puisque $\iota_Q$ n'est pas un
objet de $Z_2$. De l'intérieur de $Z_2$, il faudra montrer que les formules per-
mettant de définir les fonctions et relations usuelles sur $\mathbb{Q}$ en font un corps
totalement ordonné et dense.

Il devrait être clair que les fonctions et relations usuelles sont primitives récursives sur l'ensemble des codes de rationnels. Nous verrons que cela implique automatiquement que les formules du type $F_<$ ou $F_+$, ci-dessus, peuvent être définies dans $Z_2$, et même dans le sous système $\mathbb{R}A_0$, dont nous montrerons avec le théorème 23-4.6 qu'il est suffisant pour définir toute fonction primitive récursive via une formule de l'arithmétique.

Nous manipulerons comme habituellement nos rationnels sans recours ex-
plicite au codage, étant entendu que les différentes opérations se formalisent
via ce codage dans le langage de l'arithmétique.

## 4.2. Nombres réels

Les nombres réels sont proches des ensembles d'entiers. On peut par exemple
représenter un réel par un couple $\langle n, X \rangle$ avec $n \in \mathbb{N}$ et $X \in 2^{\mathbb{N}}$, où $n$ in-
dique la partie entière du réel et $X$ sa partie fractionnaire. Ce genre de
représentation ne va toutefois pas nous convenir, car elle ne permet pas
d'étendre correctement les notions de calculabilité aux fonctions des réels
sur les réels. L'exemple suivant est donné via la représentation des réels
par leur développement décimal plutôt que binaire, afin d'en simplifier la
présentation.

**Exemple 4.2.** À supposer qu'une fonctionnelle dont l'objectif est d'ef-
fectuer la multiplication par 3 lise les chiffres 0,33333... , elle doit se
décider au bout d'un moment à sortir le premier chiffre du résultat
de cette multiplication, mais comment savoir si l'on doit commencer
par 0,99999... ou bien par 1,00000... ? Si la fonctionnelle opte pour
la première possibilité, il se pourrait alors qu'un 4 survienne dans le
développement décimal de notre entrée, rendant le début du calcul faux.
Si la machine opte pour la deuxième possibilité, il se pourrait qu'un 2
survienne dans le développement décimal de notre entrée, avec la même
conséquence...
L'écueil de l'exemple ci-dessus vient de la différence topologique entre $\mathbb{R}$ et $2^N$, et notamment du fait que certains réels admettent plusieurs représentations possibles via leur développement décimal ou binaire. Afin de régler le problème, la solution communément utilisée est de travailler via la représentation d'un réel $r$ par une suite de Cauchy de nombres rationnels de convergence suffisamment rapide. Formellement, cela s'exprime comme suit.

**Définition 4.3.** Dans $Z_2$, un réel est une suite de rationnels $(q_n)_{n \in \mathbb{N}}$ telle que $\forall n \forall m |q_n - q_{n+m}| \le 2^{-n}$. Le nombre $r \in \mathbb{R}$ correspondant à une telle suite est $\lim_{n \to +\infty} q_n$. ◇

Il est clair que tout réel $r \in \mathbb{R}$ a une représentation dans $Z_2$, et réciproquement que tout réel $\mathbb{R}$ du point de vue de $Z_2$ —c'est-à-dire toute suite $(q_n)_{n \in \mathbb{N}}$ respectant la définition ci-dessus — définit bien un unique réel.

Pourquoi se restreindre aux suites de Cauchy à convergence maîtrisée et ne pas considérer à la place des suites de Cauchy arbitraires ? c'est-à-dire telles que pour tout $n$ il existe $a$ pour lequel $|q_a - q_{a+b}| \le 2^{-n}$ pour tout $b$. De telles suites sont elles aussi convergentes, et définissent aussi sans ambiguïté un unique réel. La raison est que nous aimerions garder calculables un certain nombre de relations, afin de minimiser les axiomes de $Z_2$ utilisés dans nos démonstrations. Si $(q_n)_{n \in \mathbb{N}}$ et $(p_n)_{n \in \mathbb{N}}$ sont deux suites de Cauchy arbitraires représentant des réels $r_q$ et $r_p$ que l'on suppose distincts, on ne peut pas décider de manière calculable, à partir des représentations de nos réels, si $r_p < r_q$ ou si $r_q < r_p$. En revanche, l'ordre devient décidable dès lors que l'on considère les suites de Cauchy de convergence maîtrisée. Notons que la relation $r_p = r_q$ reste dans tous les cas $\Pi_1^0$: elle s'exprime par $\forall n |q_n - p_n| \le 2^{-n+1}$.

### 4.3. Les ensembles de réels

Les ensembles de réels sont trop gros pour être décrits par des objets dénombrables. On a notamment $|\mathcal{P}(\mathbb{R})| > 2^N$. On peut en revanche indirectement parler de classes boréliennes dans $Z_2$. Un ouvert $U \subseteq \mathbb{R}$ peut toujours être exprimé comme une réunion d'intervalles rationnels. Pour des raisons techniques, nous considérerons l'ensemble $\mathbb{Q}^\infty = \mathbb{Q} \cup \{-\infty, +\infty\}$ plutôt que $\mathbb{Q}$. Via une bijection de $\mathbb{N}$ vers $\mathbb{Q}^\infty$, nous définissons une bijection calculable de $\mathbb{N}$ vers les intervalles ouverts de la forme $]a, b[$, pour $a, b \in \mathbb{Q}^\infty$ avec $a < b$. La bijection induit une liste $(I_n)_{n \in \mathbb{N}}$ de ces intervalles. Tout comme nous l'avons expliqué dans la section sur les rationnels, il est là encore entendu que la bijection choisie nous garantit que les opérations usuelles (comme la réunion ou l'intersection de deux intervalles) ainsi que les relations usuelles (comme l'inclusion d'un intervalle dans un autre) sont toutes primitives récursives, et donc exprimables dans $Z_2$ — et même dans $\text{RCA}_0$ — par le théorème 23-4.6 à venir.
Un ouvert $\mathcal{U} \subseteq \mathbb{R}$ sera alors représenté par un ensemble d'entiers $X \in 2^N$ tel que $\mathcal{U} = \bigcup_{n \in X} I_n$. On définit de l'extérieur de $Z_2$ la fonction $\iota_{\Sigma}^1$ par $\iota_{\Sigma}^1(X)$ comme étant l'ouvert représenté par $X$. Un fermé étant simplement le complémentaire d'un ouvert, tout ensemble $X$ représente également un fermé et l'on définit $\iota_{\Pi}^1$ par $\iota_{\Pi}^1(X) = \mathbb{R} \setminus \iota_{\Sigma}^1(X)$. On peut continuer ainsi pour définir les boréliens. Une fois la représentation des classes $\Pi_n^0$ définie, une classe $\mathcal{B}$ qui est $\Sigma_{n+1}^0$ est représentée par $\bigoplus_m X_m$ tel que $\mathcal{B} = \bigcup_m \iota_{\Pi}^n(X_m)$. On a alors $\iota_{\Sigma}^{n+1}(\bigoplus_m X_m) = \mathcal{B}$ et $\iota_{\Pi}^{n+1}(\bigoplus_m X_m) = \mathbb{R} \setminus \iota_{\Sigma}^{n+1}(\bigoplus_m X_m)$.

## 4.4. Fonctions continues

Les fonctions $f: \mathbb{R} \to \mathbb{R}$ ne sont en général pas des objets dénombrables (en particulier $|\mathbb{R}^\mathbb{R}| > 2^{|\mathbb{N}|}$). En revanche, les fonctions *continues* le sont, et l'on peut les représenter sans ambiguïté par un élément de $2^\mathbb{N}$.

Une fonction $f: \mathbb{R} \to \mathbb{R}$ est continue ssi pour tout ouvert $\mathcal{U}$, la classe $f^{-1}(\mathcal{U})$ est ouverte. Reprenons notre liste $(I_n)_{n \in \mathbb{N}}$ d'intervalle de la forme $]a, b[$ pour $a, b \in \mathbb{Q}^\infty$. Une fonction continue $f: \mathbb{R} \to \mathbb{R}$ sera alors représentée par une suite $((a_{n,m})_{m \in \mathbb{N}}, b_n)_{n \in \mathbb{N}}$ telle que $f^{-1}(I_{b_n}) = \bigcup_{m \in \mathbb{N}} I_{a_{n,m}}$ pour tout $n$. Notons qu'une suite $((a_{n,m})_{m \in \mathbb{N}}, b_n)_{n \in \mathbb{N}}$ arbitraire ne représente pas toujours une fonction continue. Il y a certaines des règles à vérifier.

**Définition 4.4.** Dans $Z_2$, une fonction continue est une suite

$$((a_{n,m})_{m \in \mathbb{N}}, b_n)_{n \in \mathbb{N}}$$

telle que en considérant $f^{-1}(I_{b_n}) = \bigcup_{m \in \mathbb{N}} I_{a_{n,m}}$, pour tout $n$, on a :

(1) $I_{n_1} \cap I_{n_2} = \emptyset \to f^{-1}(I_{n_1}) \cap f^{-1}(I_{n_2}) = \emptyset$.

(2) Pour tout réel $(q_n)_{n \in \mathbb{N}}$ et tout $n$, il existe $k$ suffisamment grand et un intervalle $I_m$ avec $|I_m| \le 2^{-n}$ tels que $]q_k - 2^{-k}, q_k + 2^{-k} [ \subseteq f^{-1}(I_m)$.

◇

La première condition de la définition ci-dessus nous garantit que la relation induite par une représentation $((a_{n,m})_{m \in \mathbb{N}}, b_n)_{n \in \mathbb{N}}$ est bien fonctionnelle, et la deuxième que la fonction ainsi définie est bien totale. Étant donné une fonction continue $f$ représentée par $((a_{n,m})_{m \in \mathbb{N}}, b_n)_{n \in \mathbb{N}}$ et un réel $r$ représenté par $(q_n)_{n \in \mathbb{N}}$, le réel $f(r)$ est défini sans ambiguïté par l'algorithmes suivant.

▷ On cherche $k_0$ et $]x_0, y_0[$ tels que

$$|x_0 - y_0| \le 1 \text{ et } ]q_{k_0} - 2^{-k_0}, q_{k_0} + 2^{-k_0} [ \subseteq f^{-1}([x_0, y_0]).$$

Par (2) de la définition ci-dessus, la recherche aboutit nécessairement.

▷ Supposons $k_n$ et $x_n, y_n$ déjà définis avec $|x_n - y_n| \le 2^{-n}$.

Soit $m = (x_n + y_n)/2$; alors, on cherche $k_{n+1} > k_n$ tel que
$$ \triangleright ]q_{k_{n+1}} - 2^{-k_{n+1}}, q_{k_{n+1}} + 2^{-k_{n+1}}[ \subseteq f^{-1}(|x_n, m|) \text{ ou} $$

$$ \triangleright ]q_{k_{n+1}} - 2^{-k_{n+1}}, q_{k_{n+1}} + 2^{-k_{n+1}}[ \subseteq f^{-1}(|m, y_n|) \text{ ou} $$

$$ \triangleright ]q_{k_{n+1}} - 2^{-k_{n+1}}, q_{k_{n+1}} + 2^{-k_{n+1}}[ \subseteq f^{-1}(|m - 2^{-n-2}, m + 2^{-n-2}|). $$

Par (2) et (1) de la définition ci-dessus, la recherche aboutit nécessairement. Une fois $q_{k_{n+1}}$ trouvé, on définit $x_{n+1} = x_n$ et $y_{n+1} = m$ dans le premier cas, $x_{n+1} = m$ et $y_{n+1} = y_n$ dans le deuxième, et enfin $x_{n+1} = m - 2^{-n-2}$ et $y_{n+1} = m + 2^{-n-2}$ dans le troisième.

Le réel $f(r)$ calculé est donné par la suite $(x_n)_{n \in \mathbb{N}}$ de rationnels, qui vérifie bien $|x_n - x_{n+m}| \le 2^{-n}$ pour tous $n, m$ (on pourrait tout aussi bien choisir $(y_n)_{n \in \mathbb{N}}$ qui représente le même réel). Notons qu'étant donné une représentation de $f$ et une représentation de $r$, l'algorithme décrit calcule toujours une représentation de $f(r)$.

# 5. RCA₀ ou les mathématiques calculables

L'arithmétique du second ordre souffre des mêmes problèmes que la théorie des ensembles vis-à-vis de la crise des fondements : ce système manipule des objets mathématiques complexes, pour lesquels il est difficile de se fier à l'intuition. De plus, le schéma de compréhension autorise les quantifications sur les ensembles, ce qui rend le système imprédicatif. Nous avons déjà vu que l'imprédicativité était parfois source de paradoxes (voir la section 9-1), ce qui n'est pas très rassurant en ce qui concerne la cohérence des axiomes.

Le but original des mathématiques à rebours étant l'analyse des axiomes nécessaires pour montrer un résultat, afin de restaurer la confiance dans nos mathématiques, il est nécessaire de travailler modulo une théorie de base robuste, qui ne laisse pas place au doute quant à sa cohérence. L'infini étant potentiellement source de paradoxes, notamment à cause de certains comportements contre-intuitifs, notre théorie de base, RCA₀, se cantonnera aux axiomes nécessaires pour parler des ensembles calculables, qui en particulier peuvent être décrits par des moyens finitaires.

## 5.1. Schéma de compréhension $\Delta_1^0$

Nous avons vu que le schéma de compréhension permettait de construire tous les ensembles de la hiérarchie arithmétique, et bien au-delà. La première étape consiste à la restreindre pour ne permettre de construire que des ensembles calculables. Rappelons qu'une formule du second ordre (avec variables libres) est $\Sigma_n^0$ si elle peut s'exprimer sous la forme d'une alternance de $n$ quantificateurs sur les entiers en commençant par une quantification existentielle, suivie d'une formule $\Delta_0^0$, c'est-à-dire une formule n'ayant que des quantificateurs bornés. En particulier, les formules $\Sigma_1^0$ sont de la
forme $\exists x F(x)$ où $F$ est $\Delta_1^0$. Notons qu'en arithmétique du second ordre, la formule $F$ peut posséder des variables libres d'ensembles. De la même manière, une formule est $\Pi_n^0$ si elle peut s'exprimer sous la forme d'une alternance de $n$ quantificateurs sur les entiers en commençant cette fois par un quantificateur universel. Le théorème 10-1.2 établit une correspondance entre calculabilité et définissabilité par les formules de l'arithmétique. Nous le rappelons ci-après.

**Théorème (10-1.2)**

Soient $A \subseteq \mathbb{N}$ et $Z \in 2^{\mathbb{N}}$. Les énoncés suivants sont équivalents.

(1) L'ensemble $A \subseteq \mathbb{N}$ est $Z$-c. e.

(2) Il existe $F(X, n)$, formule $\Sigma_1^0$ de l'arithmétique du second ordre, telle que
$$A = \{n \in \mathbb{N} : \mathbb{N} \models F(Z, n)\}.$$

(3) Il existe une fonctionnelle Turing $\Phi(X, n)$ telle que
$$A = \{n \in \mathbb{N} : \Phi(Z, n) \downarrow\}.$$

Nous allons restreindre le schéma de compréhension aux prédicats $\Delta_1^0$, au-
trement dit aux prédicats à la fois $\Sigma_1^0$ et $\Pi_1^0$. Comme la notion de prédicat $\Delta_1^0$
n'est pas syntaxique, contrairement à celle de prédicat $\Sigma_1^0$ ou $\Pi_1^0$, nous al-
lons utiliser l'astuce suivante. Pour toute formule $\Sigma_1^0 F(x)$ et toute for-
mule $\Pi_1^0 G(x)$, définissons l'axiome :

$$ (\forall x (F(x) \leftrightarrow G(x))) \rightarrow \exists X \forall y (y \in X \leftrightarrow F(y)). \quad (12) $$

La prémisse $\forall x (F(x) \leftrightarrow G(x))$ s'assure que le prédicat est $\Delta_1^0$ avant de
définir l'ensemble $X$. Notons que les formules $F$ et $G$ peuvent contenir
d'autres variables libres, du premier ou du second ordre, sur lesquelles on
doit quantifier universellement comme expliqué dans 2.1. On obtient alors
en substance : pour toute substitution des paramètres aux variables libres,
si $F(x) \leftrightarrow G(x)$ avec ces paramètres-là, alors l'ensemble des éléments qui
vérifient $F(x)$ avec ces paramètres existe bien. On appelle (12) le schéma
de compréhension $\Delta_1^0$.

## 5.2. Schéma d'induction $\Sigma_1^0$

Concentrons-nous à présent sur le premier ordre, qui est régi par les axiomes
de l'arithmétique de Robinson et par le schéma d'induction. Dans une
démarche de doute face à ce qui touche à l'infini, il est légitime de ques-
tionner ce schéma, qui permet de déduire des propriétés pour tous les en-
tiers. On l'utilise par exemple pour montrer le théorème fondamental de
l'arithmétique : tout nombre entier se décompose de manière unique en
produit de nombres premiers. Il nous est impossible de vérifier entier par
entier que c'est effectivement le cas. Il faut pour cela faire confiance à l'induction. Le lecteur pourra éventuellement être choqué de voir l'induction ainsi remise en cause, et de fait, nous verrons dans la section 23-2.1 que si l'on ne s'autorise aucune forme d'induction, on ne peut pas montrer grand-chose d'intéressant. On peut en revanche montrer qu'un niveau d'induction relativement faible est déjà suffisant pour beaucoup de théorèmes usuels, et en particulier pour formaliser la notion de calcul et de fonctions calculables.

**Définition 5.2.** On appelle schéma d'induction $\Sigma_1^0$, le schéma d'induction (10) restreint à toute formule $\Sigma_1^0$ avec variables libres. ◇

En suivant le principe de ne pas utiliser plus que nécessaire, c'est ce schéma d'induction qui sera utilisé dans notre système de base.

Il est difficile au départ de développer une bonne intuition sur ce qu'implique l'absence, par exemple de l'induction pour les formules $\Sigma_2^0$. Cette difficulté vient du fait que la plupart des mathématiciens sont habitués à travailler avec les entiers standard, et à réfléchir en se basant sur ce modèle plutôt qu'en se basant sur les axiomes utilisés. Ainsi par exemple admet-on sans y prêter la moindre attention qu'un ensemble d'entiers non vide quelconque a un plus petit élément. Nous verrons dans la section 23-3.2 que cette propriété est équivalente à l'induction. Il est tout à fait possible de construire des modèles qui ne satisfont que l'induction $\Sigma_1^0$, et au sein desquels certains ensembles $\Pi_2^0$ non vides n'ont pas de plus petit élément.

Il est en fait nécessaire ou à défaut très utile, pour comprendre les conséquences de l'absence de certains niveaux d'induction, d'avoir en tête les modèles non standard de l'arithmétique, afin de se créer une intuition qui risque sinon de faire défaut. Nous verrons dans la section 23-3 plus de détails sur l'induction, l'absence d'induction et les modèles non standard qui vont avec.

**Exercice 5.3.** Montrer que le schéma d'induction (12) pour les formules (avec variables libres) $\Delta_0^0$ implique l'axiome d'induction (11). ◇

## 5.3. Théorie RCA₀

Nous avons à présent les éléments nécessaires pour définir notre théorie RCA₀.

**Définition 5.4.** On note RCA₀ le système composé des axiomes de l'arithmétique de Robinson augmentés du schéma de compréhension $\Delta_1^0$ (12) et du schéma d'induction (10) pour les formules $\Sigma_1^0$ avec variables libres. ◇

L'acronyme RCA₀ signifie « Recursive Comprehension Axiom ». Rappe-lons que *récursif* est un ancien terme pour calculable. Ce système doit son
nom à son schéma de compréhension $\Delta_1^0$ qui ne permet de construire que des ensembles calculables. L'indice $\prec 0 \succ$ de RCA₀ signifie que le schéma d'induction est restreint aux formules $\Sigma_1^0$. En effet, Friedman avait initialement défini le système RCA avec le schéma d'induction (10) pour toutes les formules.

Tout comme la restriction du schéma de compréhension permet de restreindre la complexité des ensembles *infinis* du système, nous verrons que le schéma d'induction permet — dans un sens qui sera clarifié dans la section 23-5 — de restreindre la complexité des ensembles *finis*. Dans le cas de RCA₀, nous aurons les ensembles *infinis* calculables, et les ensembles *finis* $\Sigma_1^0$. Le lecteur aura éventuellement l'impression que les ensembles *finis* peuvent tous être représentés par un entier, et que parler de leur complexité n'a pas vraiment de sens. Nous insistons une fois de plus sur le fait que les restrictions de l'induction doivent être appréhendées sous l'éclairage de modèles non standard. Dans un tel modèle, on a un élément *a* plus grand que tous les entiers dans la partie standard $\omega$ du modèle. De l'extérieur du modèle, il y a une infinité d'éléments plus petits que *a*, et donc une infinité indénombrable de sous-ensembles d'éléments plus petits que *a*. En particulier, si notre modèle non standard est dénombrable, il y aura fatalement certains de ces sous-ensembles qui ne pourront pas être « codés » par un élément de notre modèle.

## 5.4. Modèles de RCA₀

Rappelons qu'une $\omega$-structure est une structure de l'arithmétique du second ordre où le premier ordre est constitué des entiers standard munis des opérations usuelles. Les $\omega$-structures sont donc caractérisées par leur partie du second ordre. Les $\omega$-modèles de RCA₀ admettent une caractérisation très simple en termes d'idéaux Turing.

**Définition 5.5.** Un *idéal* Turing est une classe $\mathcal{I} \subseteq 2^\mathbb{N}$ possédant les deux propriétés suivantes :

(1) clôture par réduction Turing : $\forall X \in \mathcal{I} \forall Y \leq_T X \ Y \in \mathcal{I}$;

(2) clôture par jointure : $\forall X \in \mathcal{I} \forall Y \in \mathcal{I} \ X \oplus Y \in \mathcal{I}$.

<figure><img src="image_137.png" /></figure>

**Exemple 5.6.** La classe des ensembles calculables est un idéal Turing. De même, pour tout ensemble $A$, la classe $\{X \in 2^\mathbb{N} : X \leq_T A\}$ est un idéal Turing. Les $K$-triviaux, vus dans le chapitre 20, forment un idéal Turing.

**Exercice 5.7.** (*) Montrer que la classe des ensembles low ne forme par un idéal Turing.

Indication.– On pourra par exemple utiliser le théorème 10-3.31.

<figure><img src="image_138.png" /></figure>
**Exercice 5.8. (⋆⋆)** Montrer que la classe des ensembles calculatoirement dominés ne forme par un idéal Turing. ◇

Notons que par le théorème 14-2.7, tout idéal Turing dénombrable $\mathcal{I}$ admet une paire exacte, c'est-à-dire deux ensembles $A, B$ tels que

$$ \mathcal{I} = \{ X \in 2^{\mathbb{N}} : X \leq_T A \wedge X \leq_T B \}. $$

Il est aisé de montrer l'équivalence suivante.

**Proposition 5.9 (H. Friedman).** Une $\omega$-structure $\mathcal{M}$ est un modèle de RCA₀ si, et seulement si, son second ordre est un idéal Turing. ★

**PREUVE.** Supposons que $\mathcal{M} \models RCA_0$. Soit $\mathcal{I}$ son second ordre. Montrons que $\mathcal{I}$ est clos par réduction Turing. Soit $X \in \mathcal{I}$, et soit $Y \leq_T X$. Par le théorème 10-1.2, il existe une formule $\Sigma_1^0 F(X, x)$ et une formule $\Pi_1^0 G(X, x)$ telles que $Y = \{n \in \mathbb{N} : F(X, n)\} = \{n \in \mathbb{N} : G(X, n)\}$. Par le schéma de compréhension $\Delta_1^0$, l'ensemble $Y$ existe, donc $Y \in \mathcal{I}$. Montrons que $\mathcal{I}$ est clos par jointure. Soient $X, Y \in \mathcal{I}$, et soit $F(X, Y, x)$ la formule $\Delta_0^0$ définie par

$$ \exists y \leq x ((x = \langle 0, y \rangle \wedge y \in X) \lor (x = \langle 1, y \rangle \wedge y \in Y)). $$

Comme la formule $F$ est $\Delta_0^0$, le schéma de compréhension $\Delta_1^0$ garantit que l'ensemble $X \oplus Y = \{n \in \mathbb{N} : F(X, Y, n)\}$ existe, si bien que $X \oplus Y \in \mathcal{I}$. La classe $\mathcal{I}$ est donc un idéal Turing.

Inversement, supposons que $\mathcal{I}$ est un idéal Turing, et soit $\mathcal{M}$ l'ω-structure ayant $\mathcal{I}$ pour second ordre. Montrons que $\mathcal{M} \models RCA_0$. Les axiomes de l'arithmétique de Robinson et le schéma d'induction sont satisfaits, car $\mathcal{M}$ est une $\omega$-structure. Il suffit de montrer que $\mathcal{M}$ satisfait le schéma de compréhension $\Delta_1^0$. Soient $F(X_1, \dots, X_n, y)$ et $G(X_1, \dots, X_n, y)$ des formules respectivement $\Sigma_1^0$ et $\Pi_1^0$, avec $X_1, \dots, X_n \in \mathcal{I}$ comme paramètres du second ordre, tels que $\mathcal{M} \models \forall x (F(X_1, \dots, X_n, x) \leftrightarrow G(X_1, \dots, X_n, x))$. Comme $\mathcal{M}$ est une $\omega$-structure,

$$ \{m \in \mathbb{N} : F(X_1, \dots, X_n, m)\} = \{m \in \mathbb{N} : G(X_1, \dots, X_n, m)\}. $$

Appelons $A$ cet ensemble. Par le théorème 10-1.2, $A \leq_T X_1 \oplus \dots \oplus X_n$. Comme $X_1, \dots, X_n \in \mathcal{I}$, par clôture par jointure et réduction Turing de $\mathcal{I}$, on obtient $A \in \mathcal{I}$. ■

**Exercice 5.10.** Soit $\mathcal{I}_0 \subseteq \mathcal{I}_1 \subseteq \mathcal{I}_2 \subseteq \dots$ une suite d'idéaux Turing. Montrer que $\mathcal{I} = \bigcup_n \mathcal{I}_n$ est un idéal Turing. ◇

**Exercice 5.11.** Soit $Z_0 \leq_T Z_1 \leq \dots$ une suite d'ensembles croissante pour la réduction Turing. Montrer que $\mathcal{I} = \{X \in 2^{\mathbb{N}} : \exists n X \leq_T Z_n\}$ est un idéal Turing. ◇
### 5.5. Mathématiques dans RCA₀

Par la proposition 5.9, $RCA_0$ possède un $\omega$-modèle minimal pour l'inclusion, à savoir l'`$\omega$-structure $M_{CALC}$ dont le second ordre est l'idéal Turing des ensembles calculables. Il s'ensuit — d'après le théorème 9-2.22 de complétude — qu'il suffit, pour conclure qu'un théorème $T$ n'est pas prouvable dans $RCA_0$ de montrer que le théorème $T$ implique l'existence d'un ensemble non calculable. Voici un exemple.

**Proposition 5.12.** Le lemme de König n'est pas prouvable dans $RCA_0$. ★

PREUVE. Montrons que $M_{CALC}$ ne satisfait pas le lemme de König. Soit, à cet effet, $T \subseteq 2^N$ un arbre infini calculable n'ayant pas de chemins calculables. Par exemple, l'arbre dont tous les chemins sont de degré PA. L'arbre $T$ étant calculable, $T \in M_{CALC}$. Cependant, $T$ ne possède aucun chemin dans $M_{CALC}$ puisque $T$ n'a pas de chemin calculable. Il s'ensuit que $M_{CALC}$ n'est pas un modèle du lemme de König, donc que $RCA_0$ ne prouve pas le lemme de König. ■

Notons que pour une preuve de séparation dans les $\omega$-structures, il n'est pas nécessaire de se préoccuper du niveau d'induction utilisé dans la preuve. En effet, les $\omega$-structures satisfont le schéma d'induction complet. Les résultats de séparation sont donc souvent des arguments de calculabilité pure.

En revanche, montrer que $RCA_0$ implique un théorème requiert beaucoup plus d'attention sur la complexité des objets manipulés et le niveau d'induction utilisé. Rappelons que le théorème des valeurs intermédiaires<fnref n="2" /> affirme que si $f: \mathbb{R} \to \mathbb{R}$ est continue sur l'intervalle $[0,1]$ avec $f(0) < 0 < f(1)$, alors il existe $x \in ]0,1[$ tel que $f(x) = 0$. Nous allons montrer que le théorème des valeurs intermédiaires est prouvable dans $RCA_0$.

Nous renvoyons le lecteur à la section 4 pour quelques explications sur la manière de faire de l'analyse dans $Z_2$.

**Proposition 5.13 (Simpson [203]).** Le théorème des valeurs intermédiaires est prouvable dans $RCA_0$. ★

PREUVE. Nous allons formaliser la preuve standard du théorème, à savoir la preuve par recherche dichotomique. On suppose fixé une suite $(I_n)_{n \in \mathbb{N}}$ de tous les intervalles de la forme $]a, b[$, pour $a, b \in \mathbb{Q} \cup \{-\infty, +\infty\}$. Soit $f: [0,1] \to \mathbb{R}$ une fonction continue satisfaisant $f(0) < 0 < f(1)$ (la fonction nous est donnée via sa représentation, comme expliqué dans la section 4). Supposons que $f(q) \neq 0$ pour tout rationnel $q \in \mathbb{Q} \cap ]0,1[$, sinon $q$ est le réel désiré. Par le schéma de compréhension $\Delta_1^0$, les ensembles $X_-$, $X_+$ tels que $\bigcup_{n \in X_-} I_n = f^{-1}([)-\infty, 0[$) et $\bigcup_{n \in X_+} I_n = f^{-1}([0, \infty[$) existent (il

<footnote n="2">2. Ou sous cette version, théorème de Bolzano.</footnote>
suffit d'extraire les bonnes informations de la représentation de notre fonction $f$). Soit $]a_0, b_0[\underline{\cup}]a_1, b_1[\underline{\cup} \dots$ la suite d'intervalle aux bornes rationnelles, définie par $]a_0, b_0[=]0, 1[, et

$$ ]a_{n+1}, b_{n+1}[ = \begin{cases} ] \frac{a_n + b_n}{2} , b_n [ & \text{si } \frac{a_n + b_n}{2} \in \bigcup_{n \in X_-} I_n, \\ ] a_n, \frac{a_n + b_n}{2} [ & \text{si } \frac{a_n + b_n}{2} \in \bigcup_{n \in X_+} I_n. \end{cases} $$

Par notre hypothèse, $f(q) \neq 0$ pour tout rationnel $q \in \mathbb{Q} \cap ]0, 1[, \text{ la suite } \{]a_n, b_n[ : n \in \mathbb{N}\} \text{ est bien définie pour tout } n$. Elle est donc prouvablement $\Delta_1^0(X_- \oplus X_+)$ et existe par le schéma de compréhension $\Delta_1^0$. Par induction, $\Sigma_1^0, f(a_n) < 0 < f(b_n)$ pour tout $n \in \mathbb{N}$, et $|a_n - b_n| = 2^{-n}$. Il s'ensuit que $r = (a_n)_{n \in \mathbb{N}}$ est un réel.

Montrons à présent que $f(r) = 0$. Supposons $f(r) < 0$. Soit $n \in \mathbb{N}$ tel que $f(r) < -2^{-n}$. On recherche alors un intervalle $I_n$ avec $|I_n| < 2^{-n}$ et un entier $m$ tels que $f([a_m, b_m[) \subseteq I_n$ et $a_m < b_{m+1} < b_m$. La distance entre n'importe quels points $x, y$ de $I_n$, et donc de $f([a_m, b_m[)$, est bornée par $2^{-n}$. C'est en particulier le cas pour les points $f(b_{m+1})$ et $f(r)$. On a alors $f(b_{m+1}) < 0$. Cela qui contredit le fait que $f(b_{m+1}) > 0$. Le cas $f(r) > 0$ est similaire. ■

Notons que la preuve de la proposition 5.13 n'est pas uniforme, au sens où elle distingue le cas d'une solution rationnelle ou non. Nous verrons dans le chapitre 24 la réduction de Weihrauch, qui permet d'exprimer ces considérations d'uniformité.

Nous redirigeons le lecteur intéressé par un développement plus détaillé des mathématiques dans RCA₀, vers le très complet ouvrage de Simpson [203], *Subsystems of Second Order Arithmetic*.

# 6. ACA₀ et la hiérarchie arithmétique

Comme mentionné précédemment, $Z_2$ n'est pas une extension conservative de l'arithmétique de Peano (PA), au sens où il existe des énoncés formulés uniquement dans le langage de l'arithmétique du premier ordre, qui ne sont pas prouvables dans PA, mais le sont dans $Z_2$. Nous allons maintenant voir une restriction importante de l'arithmétique du second ordre, qui nous donne plus de pouvoir que RCA₀ mais qui, contrairement à $Z_2$, est conservative sur PA.

## Notation

On note ACA₀ le système composé des axiomes de l'arithmétique de Robinson, augmentés du schéma de compréhension (9) pour les formules
arithmétiques, et de l'axiome d'induction (11).

L'acronyme $\mathcal{ACA}_0$ signifie « Arithmetical Comprehension Axiom ». L'axiome d'induction et le schéma de compréhension pour les formules arithmétiques permettent de prouver le schéma d'induction (10) pour les formules arithmétiques. Le système $\mathcal{ACA}_0$ implique donc $\mathcal{RCA}_0$. Nous avions montré que $Z_2$ est un système imprédicatif, car le schéma de compréhension avec des formules arbitraires permet de construire des ensembles qui dépendent d'eux-mêmes (voir la section 9-1 et l'exemple 8.5). Restreindre le schéma de compréhension aux formules arithmétiques permet justement d'éviter cela, et rend le système prédicatif. Des systèmes équivalents à $\mathcal{ACA}_0$ avaient déjà été étudiés par le courant prédicativiste, notamment par Weyl en 1918 dans son livre *Das Kontinuum*, soit presque soixante ans avant le début des mathématiques à rebours.

Le système $\mathcal{ACA}_0$ fait partie des grands systèmes des mathématiques à rebours qui constituent le phénomène du Club des cinq. Notons qu'il n'est pas nécessaire de rajouter le schéma de compréhension pour toutes les formules arithmétiques pour obtenir le système $\mathcal{ACA}_0$. Il suffit d'ajouter le schéma pour les formules $\Sigma_1^0$, comme le montre la proposition suivante.

**Proposition 6.1 (Simpson [203]).** Le système $\mathcal{RCA}_0$ prouve que $\mathcal{ACA}_0$ est équivalent au schéma de compréhension $\Sigma_1^0$. ★

**PREUVE.** Les formules $\Sigma_1^0$ étant arithmétiques, $\mathcal{ACA}_0$ implique le schéma de compréhension $\Sigma_1^0$. Inversement, supposons que $\mathcal{ACA}_0$ prouve le schéma de compréhension $\Sigma_n^0$, pour un $n \in \mathbb{N}$ fixé. Montrons qu'il implique le schéma de compréhension $\Sigma_{n+1}^0$. Soit $F(x)$ une formule $\Sigma_{n+1}^0$ (avec des variables libres) ; elle peut s'exprimer sous la forme $\exists y G(x, y)$, où $G(x, y)$ est une formule $\Pi_n^0$. L'ensemble $Y = \{(x, y) \in \mathbb{N} \times \mathbb{N} : \neg G(x, y)\}$ existe, par le schéma de compréhension $\Sigma_n^0$. Par le schéma de compréhension $\Sigma_1^0$ paramétré par $Y$, l'ensemble $Z = \{x \in \mathbb{N} : \exists y \ G(x, y) \notin Y\}$ existe à son tour. En particulier, $Z = \{x \in \mathbb{N} : \exists y \ G(x, y)\}$ existe. Ainsi, $\mathcal{ACA}_0$ prouve le schéma de compréhension $\Sigma_{n+1}^0$. ■

Notons l'induction de la preuve précédente : on utilise $n$ applications successives de la compréhension $\Sigma_1^0$ pour montrer la compréhension $\Sigma_n^0$. De fait, on ne tient pas compte du nombre de fois qu'un axiome est utilisé dans une preuve. Ainsi, dès que l'on s'autorise la compréhension $\Sigma_1^0$, les différents niveaux de la hiérarchie arithmétique ne sont pas distinguables du point de vue de la prouvabilité. Nous verrons dans le chapitre 24 des outils permettant de mesurer de manière plus précise la puissance calculatoire des théorèmes, en contrôlant notamment le nombre d'applications d'un même axiome.
Le système ACA₀ nous fait sortir des mathématiques calculables. Il est en fait équivalent à l'existence du saut Turing de tout ensemble.

**Exercice 6.2.** (⋆) Montrer que ACA₀ est équivalent dans RCA₀ à l'énoncé

$$ \forall X \exists Y Y = X', $$

où $Y = X'$ est une notation pour $\forall e (e \in Y \leftrightarrow \Phi_e^X(e) \downarrow)$.

◇

## 6.1. Modèles de ACA₀

Tout comme avec RCA₀, les $\omega$-modèles de ACA₀ possèdent une belle caractérisation en termes d'idéaux Turing.

**Définition 6.3.** Un idéal de saut est un idéal Turing $\mathcal{I} \subseteq 2^\mathbb{N}$ tel que pour tout $X \in \mathcal{I}$, on a $X' \in \mathcal{I}$.

◇

L'équivalence suivante est un analogue de la proposition 5.9.

**Proposition 6.4 (Simspon [203]).** Une $\omega$-structure $\mathcal{M}$ est un modèle de ACA₀ si, et seulement si, son second ordre est un idéal de saut. ★

**PREUVE.** Supposons $\mathcal{M} \models ACA_0$. Soit $\mathcal{I}$ son second ordre. En particulier, $\mathcal{M} \models RCA_0$, donc par la proposition 5.9, $\mathcal{I}$ est un idéal Turing. Par l'exercice 6.2, pour tout $X \in \mathcal{I}$, on a $X' \in \mathcal{I}$, et $\mathcal{I}$ est donc un idéal de saut.

Inversement, supposons que $\mathcal{I}$ soit un idéal de saut. En particulier, $\mathcal{I}$ est un idéal Turing, donc par la proposition 5.9, $\mathcal{M} \models RCA_0$. Comme $\mathcal{I}$ est un idéal de saut, par l'exercice 6.2, $\mathcal{M}$ est un modèle de ACA₀. ■

En particulier, ACA₀ possède aussi un $\omega$-modèle minimal pour l'inclusion, à savoir l'-$\omega$-modèle dont le second ordre est exactement l'idéal de saut des ensembles arithmétiques. Il est aisé de voir que RCA₀ n'implique pas ACA₀, en considérant l'-$\omega$-structure $\mathcal{M}_{\text{CALC}}$ dont le second ordre est l'idéal Turing des ensembles calculables. L'-$\omega$-structure $\mathcal{M}_{\text{CALC}}$ est un modèle de RCA₀, mais les ensembles calculables ne formant pas un idéal de saut, $\mathcal{M}_{\text{CALC}}$ n'est pas un modèle de ACA₀.

## 6.2. Mathématiques dans ACA₀

Le système ACA₀ est très puissant, dans la mesure où il suffit à prouver une écrasante majorité de théorèmes. Commençons par montrer que ACA₀ est équivalent dans RCA₀ à un théorème d'analyse bien connu. Le théorème de Bolzano-Weierstrass affirme que pour toute suite $(x_n)_{n \in \mathbb{N}}$ de points dans le segment $[0, 1]$, il existe une sous-suite convergente, c'est-à-dire une fonction strictement croissante $f: \mathbb{N} \to \mathbb{N}$ telle que la suite $(x_{f(n)})_{n \in \mathbb{N}}$ converge vers un point.
Le théorème de Bolzano-Weierstrass énonce deux existences : celle d'une sous-suite convergente, et celle du point de convergence. Le système RCA₀ prouve que l'existence d'un point de convergence implique celle d'une sous-suite convergente : il suffit de calculer à partir de la suite et du point une sous-suite de plus en plus proche du point de convergence. L'inverse n'est cependant pas vrai : l'existence seule d'une sous-suite convergente est équivalente à un système nommé COH (voir la section 25-4.1), compris strictement entre RCA₀ et ACA₀.

**Proposition 6.5 (Simspon [203]).** Le système ACA₀ est équivalent dans RCA₀ au théorème de Bolzano-Weierstrass. ★

PREUVE DE BOLZANO-WEIERSTRASS DANS ACA₀. Soit $(x_n)_{n \in \mathbb{N}}$ une suite de réels dans $[0, 1]$. Soit $X \in 2^{\mathbb{N}}$ une représentation de cette suite. En utilisant $X''$, on définit une fonction $f : \mathbb{N} \to \mathbb{N}$ telle que

$$ \forall n \forall i \quad |x_{f(n)} - x_{f(n+i)}| \le 2^{-n}. $$

On calcule pour cela à partir de $X''$ une suite $[a_0, b_0] \supseteq [a_1, b_1] \supseteq \dots$ d'intervalle telle que chaque segment $[a_n, b_n]$ contient une infinité de $x_m$ et telle que $b_n - a_n \le 2^{-n}$. On commence par $[a_0, b_0] = [0, 1]$. Une fois $[a_n, b_n]$ calculé, s'il y a une infinité de points dans le segment $[a_n, (a_n + b_n)/2]$ on définit alors $[a_{n+1}, b_{n+1}] = [a_n, (a_n + b_n)/2]$. À défaut, on définit le segment $[a_{n+1}, b_{n+1}]$ comme $[(a_n + b_n)/2, b_n]$. Notons que la question : « il existe une infinité de points tels que... » est $\Pi_2^0$, et peut donc être résolue à l'aide de $X''$. En utilisant l'induction arithmétique, on montre conjointement que la suite $(a_n, b_n)_{n \in \mathbb{N}}$ est bien définie et que chaque $[a_n, b_n]$ contient bien une infinité de $x_m$. On peut alors définir $f(n)$ comme étant le premier $m$ trouvé tel que $x_m \in [a_n, b_n]$. Une fois $f$ définie, on construit aisément une représentation rationnelle $(q_n)_{n \in \mathbb{N}}$ de $\lim_{n \to \infty} f(n)$ telle que, pour tous $n, i \in \mathbb{N}$, on a $|q_n - q_{n+i}| \le 2^n$. ■

PREUVE DE ACA₀ DANS BOLZANO-WEIERSTRASS. Soit $X$ un ensemble, et soit $(x_n)_{n \in \mathbb{N}}$ la suite de réels définie par $x_n = 0.X'[n]$, où $X'[n]$ est l'approximation de $X'$ à l'étape de calcul $n$. Notons que la suite est bornée par 1. D'après le théorème de Bolzano-Weierstrass, cette suite possède une sous-suite convergente et une limite, qui ne peut être que $0.X'$. D'après l'exercice 6.2, on a donc ACA₀. ■

Les deux preuves précédentes illustrent bien l'insensibilité de ACA₀ aux itérations du saut Turing : nous avons utilisé le double saut Turing pour prouver le théorème de Bolzano-Weierstrass. En revanche, dans le sens inverse, une application du théorème de Bolzano-Weierstrass n'a permis de prouver l'existence que du simple saut. On n'obtient alors le double saut qu'en appliquant le théorème deux fois de suite. Il est naturel de se poser la question de la puissance calculatoire exacte d'une application du théorème
de Bolzano-Weierstrass. Il se trouve que sa puissance est exactement celle d'un degré PA relativement à $\emptyset'$, comme le montre l'exercice suivant.

**Exercice 6.6. (*)** Montrez que pour toute suite $(x_n)_{n \in \mathbb{N}}$ de réels dans $[0, 1]$, il existe un arbre $\emptyset'$-calculable dont tous les chemins infinis sont exactement des points de convergence de sous-suites de $(x_n)_{n \in \mathbb{N}}$. Montrez enfin que pour tout arbre $\emptyset'$-calculable infini, il existe une suite $(x_n)_{n \in \mathbb{N}}$ de points dans $[0, 1]$ dont les points de convergence sont exactement les chemins infinis de l'arbre. ◇

# 7. WKL₀ et l'argument de compacité

Le système WKL₀ est sans doute le système le plus significatif des mathématiques à rebours, qui les premières en ont identifié l'importance au sein des mathématiques ordinaires. Des formalismes équivalents aux systèmes Z₂ et ACA₀ existaient préalablement, tandis que RCA₀ capture la notion déjà bien établie des mathématiques calculables. WKL₀ constitue l'un des systèmes du phénomène du Club des cinq, et correspond intuitivement aux arguments de compacité.

**Notation**

On note WKL l'énoncé << Tout arbre binaire infini admet un chemin infini. >> On note WKL₀ le système composé de RCA₀ augmenté de l'énoncé WKL.

WKL₀ est l'acronyme de << Weak König's Lemma >>, et correspond à une puissance bien connue en calculabilité, à savoir celle des degrés PA. Nous allons voir que ce système est équivalent à des théorèmes importants d'analyse et de logique, notamment le théorème de compacité de Borel-Lebesgue et le théorème de complétude de Gödel.

## 7.1. Modèles de WKL₀

Tout comme pour RCA₀ et ACA₀, le système WKL₀ admet une caractérisation de ses $\omega$-modèles, qui découle directement de celle de RCA₀, en termes d'idéaux Turing (voir la proposition 5.9).

**Définition 7.1.** Un idéal de Scott est un idéal Turing $\mathcal{I} \subseteq 2^{\mathbb{N}}$ tel que pour tout $X \in \mathcal{I}$ et tout arbre binaire infini $X$-calculable $T \subseteq 2^{<\mathbb{N}}$, il existe un chemin infini de $T$ appartenant à $\mathcal{I}$. ◇
Autrement dit, un idéal Turing $\mathcal{I}$ est un idéal de Scott si pour tout $X \in \mathcal{I}$, il existe un ensemble $Y \in \mathcal{I}$ de degré PA relativement à $X$. Dana Scott a été le premier à étudier ces idéaux [194], qui caractérisent sans surprise les $\omega$-modèles de $\text{WKL}_0$.

**Proposition 7.2.** Une $\omega$-structure $\mathcal{M}$ est un modèle de $\text{WKL}_0$ si, et seulement si, son second ordre est un idéal de Scott. ★

**PREUVE.** Immédiat par la proposition 5.9 et la définition de $\text{WKL}_0$. ■

Sachant qu'il n'existe pas de degré PA calculable, l'idéal Turing des ensembles calculables n'est pas un idéal de Scott. L'$\omega$-structure $\mathcal{M}_{\text{CALC}}$ est donc un modèle de $\text{RCA}_0$ qui n'est pas modèle de $\text{WKL}_0$, ce qui montre que $\text{RCA}_0$ n'implique pas $\text{WKL}_0$.

La plupart des théorèmes de base $\Pi_1^0$ se relativisent et permettent de construire des idéaux de Scott avec des propriétés calculatoires faibles. Ces idéaux correspondent à des $\omega$-modèles de $\text{WKL}_0$, de sorte que nos résultats de calculabilité se traduisent par des résultats de séparation en mathématiques à rebours.

**Proposition 7.3.** Soit $A_0, A_1, \dots$ une suite dénombrable d'ensembles non calculables. Il existe un idéal de Scott $\mathcal{I}$ ne contenant aucun des $A_i$. ★

**PREUVE.** Nous allons définir une suite d'ensembles $Z_0 \leq_T Z_1 \leq_T \dots$ de telle sorte que pour tout $n \in \mathbb{N}$,

(1) $Z_{n+1}$ est de degré PA relativement à $Z_n$;

(2) $A_0, A_1, \dots$ ne sont pas $Z_n$-calculables.

On a $Z_0 = \emptyset$. Supposons que l'on a défini $Z_n$. Par le théorème de base d'évitement de cône (voir le théorème 8-4.7) itéré, il existe un ensemble $Z_{n+1}$ de degré PA relativement à $Z_n$, tel que $A_0, A_1, \dots$ ne sont pas $Z_{n+1}$-calculables. En particulier, $Z_{n+1} \geq_T Z_n$ (voir si besoin l'exercice 8-7.6). Soit $\mathcal{I} = \{X \in 2^\mathbb{N} : \exists n \ X \leq_T Z_n\}$. Par l'exercice 5.11, $\mathcal{I}$ est un idéal Turing. Montrons que $\mathcal{I}$ est un idéal de Scott. Soit $X \in \mathcal{I}$, et soit $T \subseteq 2^{\mathbb{N}}$ un arbre infini $X$-calculable. En particulier, il existe un $n \in \mathbb{N}$ tel que $X \leq_T Z_n$, donc $Z_{n+1}$ est de degré PA relativement à $X$. Il s'ensuit que $Z_{n+1}$ calcule un chemin infini de $T$, donc $\mathcal{I}$ contient un chemin infini de $T$. La classe $\mathcal{I}$ est donc un idéal de Scott. Par construction, $\mathcal{I}$ ne contient aucun des $A_i$.■

En particulier, il n'existe pas d'$\omega$-modèle minimal de $\text{WKL}_0$ pour l'inclusion, contrairement à $\text{RCA}_0$ et $\text{ACA}_0$. En effet, par la proposition 7.3, l'intersection de tous les idéaux de Scott est l'idéal Turing des ensembles calculables, qui n'est pas un idéal de Scott.

Nous pouvons déduire aussi de la proposition 7.3 que $\text{WKL}_0$ n'implique pas $\text{ACA}_0$ dans $\text{RCA}_0$. En effet, tout $\omega$-modèle de $\text{ACA}_0$ contient $\emptyset'$, mais par la proposition 7.3, il existe un $\omega$-modèle de $\text{WKL}_0$ ne contenant pas $\emptyset'$.
**Exercice 7.4.** Montrer qu'il existe un idéal de Scott $\mathcal{I}$ ne contenant que des ensembles de degré calculatoirement dominé. ◇

**Exercice 7.5.** Montrer qu'il existe un idéal de Scott $\mathcal{I}$ ne contenant que des ensembles de degré low. ◇

## 7.2. Mathématiques dans WKL₀

Comme nous l'avons mentionné, le système WKL₀ correspond intuitivement aux arguments de compacité. Le théorème de compacité par excellence est le théorème de Borel-Lebesgue, qui énonce que pour toute collection $(\mathcal{U}_n)_{n \in \mathbb{N}}$ d'ouverts de $\mathbb{R}$ telle que $[0, 1] \subseteq \bigcup_n \mathcal{U}_n$, il existe $k$ tel que $[0, 1] \subseteq \bigcup_{n \le k} \mathcal{U}_n$. Nous allons montrer que cet énoncé est équivalent à WKL₀ dans RCA₀.

Étant donné $[0, 1] \subseteq \bigcup_n \mathcal{U}_n$, on peut supposer sans perte de généralité que chaque ouvert $\mathcal{U}_n$ consiste en un intervalle rationnel $]a_n, b_n[$, en isolant les intervalles de chaque ouvert de notre réunion. Passons à la preuve du théorème.

### PREUVE DE BOREL-LEBESGUE DANS WKL₀.
Pour toute chaîne $\sigma \in 2^{<\mathbb{N}}$, on considère l'intervalle $I_\sigma = [0, \sigma 0^\infty, 0, \sigma 1^\infty] \subseteq [0, 1]$. Notons que les intervalles $I_\sigma$ pour $|\sigma| = n$ forment un découpage de $[0, 1]$ en $2^n$ parties presque disjointes (par exemple, $[0, 0.01010^\infty, 0, 0.01011^\infty]$ et $[0, 0.01100^\infty, 0, 0.01101^\infty]$ ont exactement le point $0.01011^\infty = 0.01100^\infty$ en commun.)

On construit l'arbre $T \subseteq 2^{<\mathbb{N}}$ tel que $\sigma \in T$ ssi $I_\sigma$ n'est inclus dans aucun ouvert $\mathcal{U}_n$. Notons que $\sigma \in T$ est un prédicat $\Pi_1^0$. En effet, $\sigma \notin T$ si, et seulement si, $[0, \sigma 0^\infty, 0, \sigma 1^\infty] \subseteq]a_n, b_n[$ pour un certain $n$.

Donc, $T$ est $\Pi_1^0$ relativement à la représentation des ouverts $\mathcal{U}_n$, et l'on peut construire un arbre $T$-calculable $T'$ contenant $T$ tel que $[T] = [T']$ (voir la proposition 8-1.10). Montrons que $[T]$ ne contient aucun chemin infini. Considérons $X \in 2^{\mathbb{N}}$, et considérons aussi le réel $r_x = 0.X$. Formellement, $r_x = \sum_{i \in \mathbb{N}^*} 2^{-i} \times X(i)$. Par l'hypothèse du théorème, on a $r_x \in]a_n, b_n[$ pour un certain $n$. Soit $\sigma \prec X$ suffisamment grand tel que $r_x \in I_\sigma \subseteq]a_n, b_n[$. Alors, $\sigma \notin T$, et donc $X \notin [T]$. Ainsi, $T$ n'a pas de chemin infini et $T'$ non plus. Par le lemme faible de König, on en déduit que $T'$ est fini, et donc $T$ aussi. Il existe dès lors $n$ tel que tout intervalle $I_\sigma$ pour $\sigma$ de taille $n$ est inclus dans un certain $\mathcal{U}_m$. Comme le nombre de chaînes de taille $n$ est fini, on a donc un certain $k$ tel que $[0, 1] \subseteq \bigcup_{n \le k} \mathcal{U}_n$.

Avant de conclure, souvenons-nous que WKL₀ n'a toujours que l'induction pour les formules $\Sigma_1^0$. Il n'est pas toujours évident de bien cerner où l'induction est utilisée et à quel niveau. Le point auquel il faut ici faire attention est le suivant : pour la dernière étape, on utilise le fait que « pour toute chaîne $\sigma$ de taille $n$, il existe $m$ pour lequel $I_\sigma \subseteq \mathcal{U}_m$ » implique « il existe $k$ tel que pour toute chaîne $\sigma$ de taille $n$, il existe $m \le k$ tel que $I_\sigma \subseteq \mathcal{U}_m$. »
Il s'agit d'une utilisation du schéma de collection $\Sigma_1^0$ que nous définirons formellement dans la section 23-3.1, et qui se démontre à partir de l'induction $\Sigma_1^0$. Un examen attentif révélera que ce schéma est également nécessaire pour montrer $[T] = [T']$ ci-dessus. ■

Montrons à présent que $WKL_0$ est nécessaire pour prouver le théorème de Borel-Lebesgue.

PREUVE DE $WKL_0$ DANS BOREL-LEBESGUE. Soit $T \subseteq 2^{<N}$ un arbre bi-naire infini. Reprenons la notation $I_\sigma = [0.\sigma 0^\infty, 0.\sigma 1^\infty]$ de la preuve précé-dente. Supposons que $T$ n'ait pas de chemin infini. Alors, pour tout $X \in 2^N$, il existe $\sigma \notin T$ tel que $X \in I_\sigma$. Il s'ensuit que $(I_\sigma)_{\sigma \notin T}$ forme une couverture de $2^N$ par des ouverts. Par le théorème de Borel-Lebesgue, il existe un en-semble fini $F \subseteq 2^{<N} \setminus T$ tel que $2^N \subseteq \bigcup_{\sigma \in F} I_\sigma$. Soit $n$ la longueur maximale des chaînes dans $F$. L'arbre $T$ étant infini, il existe $\tau \in T$ de longueur $n$. Comme $\bigcup_{\sigma \in F} I_\sigma$ est une couverture de $2^N$, il existe $\sigma \in F$ tel que $I_\tau \subseteq I_\sigma$. En particulier, $\sigma \preceq \tau$, mais $\sigma \notin T$ et $\tau \in T$, ce qui contredit le fait que $T$ soit un arbre.

Là encore, il faut faire attention à ne pas utiliser plus que l'induction $\Sigma_1^0$, ce qui est bien le cas. ■

Le système $WKL_0$ est équivalent à des théorèmes plus généraux de compacité sur les espaces métriques compacts. En particulier, $WKL_0$ est équivalent à l'énoncé « Toute couverture d'un espace métrique compact par des ouverts admet une sous-couverture finie. » Le système $WKL_0$ est également équivalent au théorème 9-2.24 : toute théorie cohérente peut être étendue en une théorie complète et cohérente. L'équivalence entre la capacité à calculer une extension complète et cohérente de l'arithmétique de Peano et la capacité à calculer un chemin dans tout arbre calculable infini illustre cette équivalence. Le lecteur trouvera un développement plus détaillé des mathématiques dans $WKL_0$ dans l'ouvrage de Simpson [203].

## 7.3. $WKL_0$ et l'aléatoire

Il convient de s'arrêter sur un sous-système de $WKL_0$ particulièrement important, au point qu'il mériterait, par sa robustesse, par son interprétation épistémologique, et par le nombre de théorèmes qui lui sont équivalents, d'être considéré comme le sixième membre d'honneur du Club des cinq. Il s'agit de la restriction du lemme faible de König aux arbres de mesure positive. Dans cette section, nous ferons appel à des notions d'aléatoire algorithmique introduites dans la partie II, et plus précisément aux propriétés calculatoires des aléatoires de Martin-Löf. Il n'est cependant pas nécessaire de comprendre cette section pour continuer le chapitre.
**Définition 7.6.** Un arbre $T \subseteq 2^{<N}$ est de mesure positive si

$$ \liminf_n \frac{|\{\sigma \in T : |\sigma| = n\}|}{2^n} > 0. \quad \diamond $$

Nous avons vu qu'il existait une correspondance entre classes $\Pi_1^0$ et arbres binaires. La notion d'arbre de mesure positive décrit les arbres dont les classes $\Pi_1^0$ correspondantes sont de mesure positive.

**Exercice 7.7.** (⋆) Soit $T \subseteq 2^{<N}$ un arbre. Montrer que

$$ \lambda([T]) = \liminf_n \frac{|\{\sigma \in T : |\sigma| = n\}|}{2^n}. \quad \diamond $$

La notion d'arbre de mesure positive s'avère plus pratique à manipuler que la notion de classe $\Pi_1^0$ de mesure positive dans l'arithmétique du second ordre, car elle évite de devoir formaliser la notion de mesure qui est une fonction sur les classes, et donc d'ordre supérieur. Nous utiliserons donc la formulation en termes d'arbres de mesure positive pour définir le système $WWKL_0$.

**Notation**

$WWKL$ est l'énoncé « Tout arbre binaire de mesure positive admet un chemin infini. »

$WWKL_0$ est le système $RCA_0$ augmenté de l'énoncé $WWKL$.

L'acronyme $WWKL$ vient de l'anglais « Weak weak König's lemma », et nous l'appellerons « Lemme très faible de König ». Il découle directement du lemme faible de König, car tout arbre binaire de mesure positive est infini. Les classes $\Pi_1^0$ de mesure positive possèdent des liens très forts avec l'aléatoire de Martin-Löf. En particulier, tout MLR est, à préfixe près, un membre de chaque classe $\Pi_1^0$ de mesure positive, comme le montre le lemme suivant.

**Lemme 7.8 (Kučera [128])**

Soit $T \subseteq 2^{<N}$ un arbre $X$-calculable tel que $\lambda([T]) > 0$. Alors, $[T]$ contient un suffixe de n'importe quel ensemble $MLR(X)$. Autrement dit, si l'ensemble $Z$ est $MLR(X)$, il existe alors $Y \in [T]$ et $\sigma$ tels que $Z = \sigma Y$. ⋆

**PREUVE.** Considérons la classe $\Sigma_1^0(X) = 2^{<N} \setminus [T]$. En particulier, $\lambda(\mathcal{U}) < 1$. Soit $W$ un ensemble $X$-c. e. sans préfixe tel que $\mathcal{U} = \bigcup_{\sigma \in W} [\sigma]$. On définit alors $\mathcal{U}^1 = \mathcal{U}$ et $W^1 = W$, puis par induction sur $n$ on définit la classe $\mathcal{U}^{n+1}$ comme étant celle décrite par l'ensemble $W^{n+1} = \{\sigma \tau : \sigma \in W \text{ et } \tau \in W^n\}$. On a dès lors $\lambda([W^{n+1}]) = \sum_{\sigma \in W} 2^{-|\sigma|} \lambda([W^n]) = \lambda([W]) \times \lambda([W^n])$.
On en déduit $\lambda(U^n) = (\lambda(U))^n$. Comme $\lambda(U) < 1$, alors $f : n \to \lambda(U^n)$ tend vers 0 de manière effective, c'est-à-dire bornée par une fonction calculable. En particulier, $\bigcap_n U^n$ est un X-test de Martin-Löf.

Considérons à présent un ensemble $Z$ qui n'a pas de suffixe dans $2^N \setminus U$. Donc, pour tout $\sigma$ tel que $Z = \sigma Y$, on a $Y \in U$. En particulier, $Z \in U = U^1$. Soit $\sigma \prec Z$ tel que $\sigma \in W^1$. Alors, $Z$ amputé du préfixe $\sigma$ appartient aussi à $U$, et donc par définition $Z$ a aussi un préfixe dans $W^2$, et appartient donc à $U^2$. On montre en continuant ainsi que $Z \in \bigcap_n U^n$, et donc que $Z$ n'est pas MLR($X$). $\blacksquare$

Le lemme 7.8 nous permet de donner une belle caractérisation des $\omega$-modèles de $WWKL_0$.

**Proposition 7.9.** Une $\omega$-structure $\mathcal{M}$ est un modèle de $WWKL_0$ si, et seulement si, son second ordre est un idéal Turing $\mathcal{I}$ tel que pour tout $X \in \mathcal{I}$, il existe un MLR($X$) $Z \in \mathcal{I}$.

\*

PREUVE. Soit $\mathcal{M}$ un $\omega$-modèle de $WWKL_0$ et soit $\mathcal{I}$ son second ordre. En particulier, $\mathcal{M} \models RCA_0$, donc par la proposition 5.9, $\mathcal{I}$ est un idéal Turing. Soit $X \in \mathcal{I}$, et soit $T \subseteq 2^{<N}$ un arbre $X$-calculable de mesure positive tel que tous les chemins infinis soient MLR($X$). Par exemple, nous pouvons fixer $c \in \mathbb{N}$ et définir $T = \{\sigma \in 2^{<N} : \forall \tau \preceq \sigma K^X(\tau) \ge |\tau| - c\}$, où $K^X(\sigma)$ est la complexité de Kolmogorov sans préfixe, relativisée à $X$ (voir le théorème 18-2.1). Comme $\mathcal{M} \models WWKL$, il existe $Z \in [T]$ tel que $Z \in \mathcal{I}$. En particulier, $Z$ est MLR($X$).

Réciproquement, soit $\mathcal{I}$ un idéal Turing tel que pour tout $X \in \mathcal{I}$, il existe un MLR($X$) $Y \in \mathcal{I}$. Soit $\mathcal{M}$, l'ω-structure induite par $\mathcal{I}$. Par la proposition 5.9, $\mathcal{M} \models RCA_0$. Soit $T \subseteq 2^{<N}$ un arbre de mesure positive codé par un ensemble $X \in \mathcal{I}$. Par hypothèse, il existe un MLR($X$) $Z \in \mathcal{I}$. En particulier, $\lambda([T]) > 0$, donc il existe $Y \in [T]$ et $\sigma \in 2^{<N}$ tels que $Z = \sigma Y$. Comme $Y \leq_T Z$ et $Z \in \mathcal{I}$, il vient $Y \in \mathcal{I}$, et donc $\mathcal{M} \models WWKL$. $\blacksquare$

Le système $WWKL_0$ peut être considéré comme capturant les mathématiques faisant appel à des arguments probabilistes. Cette vision est cependant à relativiser, car certains arguments probabilistes nécessitent des notions d'aléatoire plus fortes. Comme aucun MLR n'est calculable, l'ω-modèle minimal $M_{\text{CALC}}$ de $RCA_0$ n'est pas un modèle de $WWKL_0$, ce qui implique que $RCA_0$ ne prouve pas $WWKL_0$.

Montrons maintenant que $WWKL_0$ est strictement plus faible de $WKL_0$, en construisant un modèle de $WWKL_0$ qui n'est pas modèle de $WKL_0$ à l'aide des outils de l'aléatoire algorithmique.
**Proposition 7.10.** WWKL₀ n'implique pas WKL₀ dans RCA₀. ★

PREUVE. Soit Z un ensemble 2-aléatoire. Par le théorème 19-1.7 et le co-
rollaire 19-1.8, Z n'est pas de degré PA. Soit

$$
Y_0 \oplus Z_0 = Z, \quad Y_1 \oplus Z_1 = Z_0, \quad Y_2 \oplus Z_2 = Z_1,
$$

et ainsi de suite. Par le théorème de van Lambalgen relativisé (voir le théorème 19-2.5), $Y_0$ est MLR et $Z_0$ est MLR($Y_0$), $Y_1$ est MLR($Y_0$) et $Y_2$ est MLR($Y_0 \oplus Y_1$), et de manière générale, $Y_{n+1}$ est MLR($Y_0 \oplus \cdots \oplus Y_n$) et $Y_n \le_T Z$ pour tout $n \in \mathbb{N}$. Soit $\mathcal{I} = \{X \in 2^\mathbb{N} : \exists n \ X \le_T Y_0 \oplus \cdots \oplus Y_n\}$. Soit $\mathcal{M}$ l'ω-structure induite par $\mathcal{I}$. La classe $\mathcal{I}$ est un idéal Turing par l'exercice 5.11, donc $\mathcal{M} \models RCA_0$ par la proposition 5.9. Soit $X \in \mathcal{I}$, et soit $n \in \mathbb{N}$ tel que $X \le_T Y_0 \oplus \cdots \oplus Y_n$. Comme $Y_{n+1} \in \mathcal{I}$ et $Y_{n+1}$ est MLR($Y_0 \oplus \cdots \oplus Y_n$), alors $Y_{n+1}$ est MLR($X$), donc $\mathcal{M} \models$ WWKL. L'ω-structure $\mathcal{M}$ est donc un modèle de WWKL₀. Cependant, $\mathcal{I}$ ne contient aucun ensemble de degré PA car pour tout $X \in \mathcal{I}$, $X \le_T Z$, et $Z$ n'est pas de degré PA. Ainsi par la proposition 7.2, $\mathcal{M}$ n'est pas un modèle de WKL₀. ■

8. Systèmes plus puissants

Nous avons pour l'instant défini cinq systèmes :

RCA₀, WWKL₀, WKL₀, ACA₀ et Z₂,

listés par ordre strictement croissant de force logique. Le système RCA₀
capture les mathématiques calculables, ce qui couvre une grande partie des
mathématiques ordinaires, mais il existe cependant de nombreux théorèmes
classiques non calculables. Le système WWKL₀ ajoute les arguments proba-
bilistes, tandis que le système WKL₀ ajoute les arguments de compacité à la
boîte à outils du mathématicien. Le système ACA₀ représente quant à lui un
saut dans la force logique des mathématiques. Il capture les mathématiques
prédicatives, ce qui correspond à l'écrasante majorité des théorèmes. De très
rares théorèmes classiques échappent à la puissance de ACA₀, et font appel
au système Z₂.

La grande majorité des théorèmes se situant en dessous de ACA₀, les sous-
systèmes faibles de l'arithmétique du second ordre, ont reçu une attention
particulière. En effet, la démarche des mathématiques à rebours est avant
tout de comprendre des tendances des mathématiques et non pas de recher-
cher l'exhaustivité. Il convient cependant de mentionner quelques systèmes
importants qui se situent au-delà de ACA₀, et que nous étudierons plus en
détail dans le chapitre 31 de la partie IV sur l'hypercalculabilité.
## 8.1. ACA'$_0$ ou la puissance de l'induction

Nous allons commencer par un système légèrement plus forts que ACA$_0$, et qui n'est pas considéré comme faisant partie du phénomène du Club des cinq.

Nous avons vu que ACA$_0$ était équivalent à l'énoncé $\forall X \exists Y Y = X'$ (voir l'exercice 6.2). En itérant l'énoncé de l'existence du saut Turing, il s'ensuit immédiatement que ACA$_0$ est équivalent à l'énoncé $\forall X \exists Y Y = X^{(n)}$ pour tout $n \in \mathbb{N}$. Ici, il convient de faire bien attention à la quantification de $n$, qui est une quantification externe. L'énoncé $\forall n \forall X \exists Y Y = X^{(n)}$ fait appel à un axiome d'induction qui sort du cadre de ACA$_0$.

Beaucoup de théorèmes que nous étudierons dans cette partie s'expriment sous la forme $\forall X (F(X) \rightarrow \exists Y G(X, Y))$, où F et G sont des formules arithmétiques éventuellement avec des variables libres. On peut alors voir un théorème de ce type comme un problème mathématique, formulé en termes d'instances et de solutions. On dira qu'un ensemble $X$ est une instance du problème si $F(X)$ est vrai, et $Y$ est une solution de l'instance $X$ si $G(X, Y)$ est vrai. Par exemple, une instance du lemme faible de König est un arbre binaire infini, et une solution de cette instance est un chemin infini. Nous avons vu que par itérations du saut Turing, il était possible de prouver dans ACA$_0$ l'existence de tous les ensembles de la hiérarchie arithmétique. En revanche, ACA$_0$ garde une forme de faiblesse, dans le sens où il n'est pas capable de prouver l'existence de solutions à un problème, qui soient arbitrairement élevées dans la hiérarchie arithmétique. Plus précisément, le théorème suivant a été prouvé indépendamment par Jockusch et Solovay (voir Wang [230]).

### Théorème 8.1 (Jockusch et Solovay)

Soient $F(X)$ et $G(X, Y)$ des formules arithmétiques n'ayant que des variables libres explicites. Si

$$ \mathbf{ACA}_0 \vdash \forall X (F(X) \rightarrow \exists Y G(X, Y)), $$

alors il existe un $k \in \mathbb{N}$ tel que

$$ \mathbf{ACA}_0 \vdash \forall X (F(X) \rightarrow \exists Y \leq_T X^{(k)} G(X, Y)). $$

### PREUVE COMMUNIQUÉE À WANG PAR JOCKUSCH

Soient $F(X)$ et $G(X, Y)$ des formules arithmétiques n'ayant que des variables libres explicites. Soit $C$ un symbole de constante du second ordre. Soit $G_k(X)$ la formule $(F(X) \rightarrow \exists Y \leq_T X^{(k)} G(X, Y))$. Soit $T$ la théorie dans le langage $\mathcal{L}_{PA}$ augmenté de la constante $C$, composée des axiomes de PA, du schéma d'induction pour les formules arithmétiques avec $C$ comme paramètre, et des axiomes $\neg G_k(C)$ pour tout $k \in \mathbb{N}$. Supposons
que $\forall X G_k(X)$ ne soit prouvable par $\mathsf{ACA}_0$ pour aucun $k \in \mathbb{N}$. En appliquant le théorème 9-2.20 et en utilisant $\neg G_{k+1}(X) \rightarrow \neg G_k(X)$, on en déduit que pour tout $k$ le système $\mathsf{ACA}_0 \cup \{\neg G_k(C)\}_{i \le k}$ a un modèle. Par compacité, on en déduit que $\mathsf{ACA}_0 \cup \{\neg G_k(C)\}_{k \in \mathbb{N}}$ a un modèle. Comme $\mathsf{ACA}_0 \vdash \mathrm{PA}$, la théorie $\mathrm{T}$ a un modèle $\mathcal{M}$. Plus précisément, $\mathcal{M}$ est spécifié par un premier ordre $\mathcal{M}$ et une interprétation $C^M \subseteq \mathcal{M}$ du symbole $\mathcal{C}$. Soit $\mathcal{I} \subseteq \mathcal{P}(\mathcal{M})$ la classe des sous-ensembles de $\mathcal{M}$ définissables dans $\mathcal{M}$ par une formule arithmétique avec comme unique paramètre $C^M$. En particulier, $C^M \in \mathcal{I}$. Considérons la structure $\mathcal{M}'$ dans le langage de $\mathcal{L}_{\mathbb{Z}_2}$ dont le premier ordre est $\mathcal{M}$ et le second ordre est $\mathcal{I}$.

Montrons que $\mathcal{M}' \models \mathsf{ACA}_0$. Comme $\mathcal{M} \models \mathrm{PA}$, alors $\mathcal{M}'$ satisfait les axiomes de l'arithmétique de Robinson. Soit $H(x)$ une formule de l'arithmétique avec paramètres dans $\mathcal{M}'$. Comme tout paramètre de $H$ est définissable de manière arithmétique dans $\mathcal{M}$, alors $H$ peut être transformée en une formule $\widehat{H}$ avec comme unique paramètre $C^M$, telle que

$$ \{x \in \mathcal{M} : M \models \widehat{H}(x)\} = \{x \in \mathcal{M} : \mathcal{M}' \models H(x)\}. $$

Comme $\{x \in \mathcal{M} : M \models \widehat{H}(x)\} \in \mathcal{I}$, alors $\mathcal{M}'$ satisfait le schéma de compréhension arithmétique avec paramètres. Montrons enfin que $\mathcal{M}'$ satisfait l'axiome d'induction (11). Soit $X \in \mathcal{I}$. En particulier, $X$ est définissable par une formule arithmétique avec comme unique paramètre $C^M$; or, $T$ prouve le schéma d'induction pour ces formules, donc l'axiome d'induction (11) est satisfait par $\mathcal{M}'$.

Ainsi, $\mathcal{M}' \models \mathsf{ACA}_0$, mais comme $\mathcal{M} \models \neg G_k(C^M)$ pour tout $k$ et que tout ensemble de $\mathcal{M}'$ est arithmétiquement définissable en $C^M$, alors $\mathcal{M}'$ est modèle de $\neg F(C^M) \lor \forall Y \neg G(C^M, Y)$. Donc, $\forall X(F(X) \rightarrow \exists Y G(X, Y))$ n'est pas un théorème de $\mathsf{ACA}_0$. ■

Il découle directement du théorème 8.1 que l'énoncé $\forall n \forall X \exists Y Y=X^{(n)}$ n'est pas prouvable dans $\mathsf{ACA}_0$. Souvenons-nous que les $\omega$-modèles de $\mathsf{ACA}_0$ sont clos par saut Turing, et sont donc en particulier des modèles de $\forall n \forall X \exists Y Y=X^{(n)}$. Les modèles de $\mathsf{ACA}_0$ dans lesquels cet énoncé est faux auront donc nécessairement un premier ordre non standard, au sein duquel il manque le niveau d'induction nécessaire pour montrer par exemple $(\exists X X = \emptyset^{(n)} \rightarrow \exists X X = \emptyset^{(n+1)} \rightarrow \forall n \exists X X = \emptyset^{(n)}$. Cela nous conduit à définir le système suivant.

### Notation

On note $\mathsf{ACA}'_0$ le système $\mathsf{RCA}_0$ augmenté de l'axiome $\llcorner$ Pour tout ensemble $X$ et tout entier $n \in \mathbb{N}$, il existe une suite $Y_0, Y_1, \dots, Y_n$ telle que $Y_0 = X$ et $Y_{s+1} = Y_s'$. $\gg$
Les $\omega$-modèles de $ACA_0$ et $ACA'_0$ coïncident, sachant que tout idéal de saut satisfait l’énoncé ci-dessus. Toute preuve de séparation entre $ACA_0$ et $ACA'_0$ se fait donc nécessairement dans des modèles non standard. Nous verrons dans le chapitre 25 un exemple de théorème classique prouvable dans $ACA'_0$, mais pas dans $ACA_0$.

## 8.2. $ACA_0^+$ et l’$\omega$-saut Turing

Le système $ACA_0^+$ est un renforcement de $ACA_0$ qui apparaît naturellement dans l’analyse des preuves de théorèmes combinatoires dénombrables, et en particulier le théorème 8.2 de Hindman.

**Notation**

$ACA_0^+$ est le système $RCA_0$ augmenté de l’énoncé « Pour tout ensemble $X$, l’$\omega$-saut Turing $X^{(\omega)} = \bigoplus_{n \in \mathbb{N}} X^{(n)}$ de $X$ existe. »

Le système $ACA_0^+$ est strictement plus fort que $ACA_0$, car l’$\omega$-structure dont le second ordre est composé des ensembles arithmétiques est un modèle de $ACA_0$ (et de $ACA'_0$), mais ne contient pas l’$\omega$-saut Turing de $\emptyset$, donc n’est pas un modèle de $ACA_0^+$. Ce système a été introduit par Blass, Hirst, et Simpson [21] pour mesurer la puissance logique du théorème de Hindman. Il s’agit d’un théorème des mathématiques combinatoires, et plus particulièrement de la théorie de Ramsey, qui sera abordée dans le chapitre 25. Nous n’aurons toutefois pas l’occasion de revenir sur le théorème de Hindmann, dont nous mentionnons tout de même ici l’énoncé pour le lecteur qui souhaite en mesurer la difficulté. Étant donné un ensemble $X \subseteq \mathbb{N}$, on note $FS(X)$ l’ensemble

$$ \{ \sum_{n \in F} n : F \subseteq X \text{ non vide et fini} \}. $$

**Théorème 8.2 (Hindman [86])**

Pour tout $k \in \mathbb{N}$ et toute fonction $f : \mathbb{N} \to \{0, \dots, k\}$, il existe un ensemble infini $H \subseteq \mathbb{N}$ tel que $|f(FS(H))| = 1$.

Blass, Hirst, et Simpson [21] ont prouvé que le théorème de Hindman impliquait $ACA_0$ et qu’il était prouvable dans $ACA_0^+$. Le théorème de Hindman est l’exemple typique, en mathématiques à rebours, de théorème pour lequel l’analyse calculatoire a nécessité de trouver de nouvelles preuves plus élémentaires. Il existe à ce jour plusieurs preuves, dont celle originale de Hindman [86] formalisable dans $ACA_0^+$, une preuve courte due à Baumgartner [11], mais dont l’analyse calculatoire est plus complexe, une preuve de
Galvin-Glazer à l'aide d'ultrafiltres [39] qui sont des objets du troisième ordre, et donc plus difficiles à étudier en mathématiques à rebours, et plus récemment une preuve simple due à Towsner [224], mais dont la complexité logique est la même que la preuve originale de Hindman. La question suivante reste l'une des plus grandes questions ouvertes en mathématiques à rebours.

**Question 8.3.** Quelle est la puissance calculatoire exacte du théorème de Hindman ?

<figure><img src="image_139.png" /></figure>

On ignore à ce jour si le théorème de Hindman est équivalent dans $RCA_0$ à $ACA_0$, à $ACA_0^+$, ou même strictement entre les deux systèmes. On ne connaît pour l'instant aucun théorème classique équivalent au système $ACA_0^+$, ce qui relativise l'importance de ce système.

## 8.3. $ATR_0$ et l'induction transfinie

Les systèmes $ATR_0$ et $Π_1^1$-$CA_0$ sont respectivement les quatrième et cinquième grands systèmes du phénomène du Club des cinq étudiés en mathématiques à rebours. Leur étude ainsi que celle de leurs modèles fait appel à des outils plus puissants que ceux de la calculabilité classique, à savoir l'hypercalculabilité, qui est un domaine d'étude à part entière et que nous présenterons dans la partie IV. Les systèmes $ATR_0$ et $Π_1^1$-$CA_0$ seront étudiés plus en détail dans le chapitre 31. Nous en donnons cependant un rapide aperçu dans cette section pour compléter le panorama des systèmes des mathématiques à rebours.

Le système $ATR_0$ affirme informellement l'existence de l'α-saut Turing, pour un ordinal α dans le modèle considéré. Plus précisément, un ensemble *ben ordonné* ($A, <_A$) n'admettant pas de suite infinie décroissante (cette notion sera formellement présentée et étudiée dans les moindres détails dans le chapitre 27). Soit $\theta(x, X)$ une formule arithmétique, contenant notamment les variables libres $x$ et $X$, et potentiellement d'autres variables libres. Cette formule induit sur les ensembles un opérateur $\Theta: 2^N \to 2^N$ défini par $\Theta(X) = \{n \in \mathbb{N} : \theta(n, X)\}$.

**Définition 8.4.** Le schéma de récursion transfinie énonce, pour toute formule arithmétique $\theta(x, X)$ avec des variables libres, et tout ensemble bien ordonné ($A, <_A$), l'existence d'un ensemble $Y = \bigoplus_{a \in A} Y_a$ défini pour tout $a \in A$ par

$$Y_a = \Theta\left(\bigoplus_{b <_A a} Y_b\right).$$

<figure><img src="image_140.png" /></figure>

Par exemple, si l'on considère la formule $\theta(x, X) = \Phi_x^X(x) \downarrow$ et l'ensemble bien ordonné $(\mathbb{N}, <_\mathbb{N})$, alors l'opérateur $\Theta$ est le saut Turing défini par $\Theta(X) = X'$.
On a

$$Y_0 = \Theta(\emptyset) = \emptyset', \quad Y_1 = \Theta(Y_0) = \emptyset'', \quad Y_2 = \Theta(Y_0 \oplus Y_1) = (\emptyset' \oplus \emptyset'')',$$

et ainsi de suite. L'ensemble $Y$ résultant est de même degré que l'ω-saut Turing de $\emptyset$.

**Notation**

$\mathrm{ATR}_0$ est le système $\mathrm{RCA}_0$ augmenté du schéma de récursion transfinie.

Au vu de l'exemple précédent, nous voyons que $\mathrm{ATR}_0$ implique $\mathrm{ACA}_0^+$, et donc $\mathrm{ACA}_0$. Nous verrons dans le chapitre 31 que $\mathrm{ATR}_0$ est un système strictement plus puissant.

## 8.4. $\Pi_1^1$-$\mathrm{CA}_0$ et l'imprédicativité

Il est possible d'étendre la classification des formules au-delà de la hiérarchie arithmétique, en se basant sur l'alternance des quantificateurs sur les ensembles. On obtient alors la hiérarchie analytique. Nous ne définirons que le niveau le plus bas. Une formule de l'arithmétique du second ordre est $\Pi_1^1$ (resp. $\Sigma_1^1$) si elle est de la forme $\forall XF(X)$ (resp. $\exists XF(X)$) où $F$ est une formule arithmétique.

**Notation**

$\Pi_1^1$-$\mathrm{CA}_0$ est le système $\mathrm{RCA}_0$ augmenté du schéma de compréhension (9) pour les formules $\Pi_1^1$.

Le système $\Pi_1^1$-$\mathrm{CA}_0$ est strictement plus puissant que $\mathrm{ATR}_0$, et de très rares théorèmes lui sont équivalents. Mentionnons le théorème de Cantor-Bendixson, qui énonce que toute classe fermée indénombrable de $\mathbb{R}^n$ est la réunion d'une classe fermée parfaite et d'une classe finie ou dénombrable. Le théorème de Cantor-Bendixson affirme en particulier que l'hypothèse du continu est prouvable pour les classes fermées de $\mathbb{R}^n$. Nous verrons la démonstration d'une certaine forme de ce théorème au sein de l'espace de Baire $\mathbb{N}^\mathbb{N}$ avec le théorème 30-3.2.

Contrairement au système $\mathrm{ATR}_0$, le système $\Pi_1^1$-$\mathrm{CA}_0$ est foncièrement imprédicatif. Rappelons qu'une définition imprédicative est en substance une définition circulaire dans laquelle l'objet qui est défini est lui-même susceptible d'être utilisé dans la définition. Considérons l'exemple suivant.

**Exemple 8.5.** Les ensembles suivants sont définis de manière imprédicative :

$$(1) \quad A = \{ n \in \mathbb{N} : \forall X, n \notin X \};$$
(2) $W = \{e \in \mathbb{N} : W_e$ énumère un arbre $T \subseteq \mathbb{N}^< \text{ tel que } \forall Y \ Y \notin [T]\}$.
Les ensembles $A$ et $W$ sont définis via une quantification sur tous les ensembles, et sont donc définis en fonction d'eux-mêmes.

Il va de soi que l'ensemble $A$ de l'exemple précédent peut se définir autrement — $A = \emptyset$—, mais nous verrons dans la section 29-3 que ce n'est pas le cas pour l'ensemble $W$. Notons que l'imprédicativité de $Z_2$ fait uniquement appel au schéma de compréhension (9) pour une formule $\Pi_1^1$, ce qui fait bien de $\Pi_1^1$-CA$_0$ un système imprédicatif.

## 8.5. Résumé

Dans ce chapitre, nous avons présenté une hiérarchie strictement croissante de sous-systèmes de l'arithmétique du second ordre :

$$ RCA_0 < WKL_0 < ACA_0 < ACA'_0 < ACA_0^+ < ATR_0 < \Pi_1^1-CA_0 < Z_2. $$

Les systèmes $RCA_0$, $WKL_0$, $ACA_0$, $ATR_0$ et $\Pi_1^1$-CA$_0$ forment le Club des cinq. La plupart des théorèmes ordinaires sont soit prouvables dans $RCA_0$, soit équivalents à l'un des quatre autres systèmes modulo $RCA_0$. Parmi ces théorèmes, la très grande majorité d'entre eux est prouvable dans $ACA_0$, voire $WKL_0$.

L'étude des sous-systèmes de l'arithmétique du second ordre ne se cantonne cependant pas à cette hiérarchie minimaliste linéairement ordonnée. Nous allons étudier dans les chapitres suivants plusieurs sous-systèmes de puissance intermédiaire qui apparaissent naturellement dans l'étude des mathématiques. Le chapitre 25 en particulier se focalisera sur l'étude méta-mathématique du théorème de Ramsey, qui a profondément bouleversé le visage des mathématiques à rebours.
<figure><img src="image_141.png" /></figure>
Chapitre 23

Induction et conservation

Dans ce chapitre nous nous concentrons sur les possibilités et les limites du système RCA₀ en ce qui concerne les énoncés du premier ordre. Rappelons que RCA₀ restreint le schéma d'induction aux formules Σ₁₀.

La restriction de l'induction pour capturer les mathématiques calculables peut sembler étonnante à première vue, car il s'agit d'un principe régissant le comportement des entiers et non des ensembles d'entiers. Nous verrons cependant qu'il existe un lien entre le schéma d'induction et le schéma de compréhension bornée, autrement dit, l'existence des ensembles finis dans le modèle. La restriction de l'induction s'inscrit dans le programme des mathématiques à rebours qui vise à trouver les axiomes optimaux pour prouver les théorèmes ordinaires. Il est donc raisonnable de considérer l'induction comme une ressource que l'on cherche à minimiser.

Étant donné que les entiers standard sont un modèle de l'induction pour toutes les formules, il est utile pour bien appréhender les limites de RCA₀ d'appuyer son intuition sur les modèles non standard, qui rappelons-le contiennent des éléments plus grands que tous les entiers standard.

**Notation :** ω is the new N

Dans le cadre de l'étude de modèles potentiellement non standard, il est d'usage de désigner les entiers standard (ceux que nous considérons comme étant les « vrais entiers » et notés $N$ jusqu'alors dans ce livre) par la lettre $\omega$. Notre notation habituelle $N$ fera alors référence au sein de ce chapitre à l'ensemble syntaxique des entiers : par exemple, la phrase « $\forall n \in N F(n)$ » signifie que tout entier du point de vue du modèle considéré vérifie la formule $F$. La notation $N$ est alors simplement un symbole syntaxique qui est interprété par $M$ au sein d'un modèle $\mathcal{M} = (M, S, +, \times, <, 0, 1)$.
# 1. Fonctions RCA₀-prouvablement calculables

Afin de s'assurer de la validité d'une preuve dans RCA₀, il faut notamment vérifier que seul l'axiome d'induction $\Sigma_1^0$ est utilisé. Il s'agit d'une restriction à ne pas prendre à la légère, et qu'il faut garder en tête en particulier avant d'appliquer l'axiome de compréhension pour les formules $\Delta_1^0$, que nous rappelons ici. Pour toute formule $\Sigma_1^0 F(x)$ et toute formule $\Pi_1^0 G(x)$, nous avons :

$$ (\forall x (F(x) \leftrightarrow G(x))) \rightarrow \exists X \forall y (y \in X \leftrightarrow F(y)). \quad (12) $$

En particulier, il sera nécessaire de démontrer $(\forall x (F(x) \leftrightarrow G(x)))$ au sein de RCA₀ avant de pouvoir appliquer l'axiome de compréhension. Il est de fait envisageable que certains ensembles soient calculables, c'est-à-dire $\Delta_1^0$, sans pour autant que nous puissions le démontrer au sein de RCA₀. Il ap-paraît donc important de mener une étude détaillée des énoncés arithmé-tiques qu'il est possible de démontrer dans RCA₀, et notamment de com-prendre quelles fonctions y sont prouvablement calculables.

Rappelons qu'une fonction $f : \omega \to \omega$ est codée sous la forme d'un ensemble d'entiers par son graphe $G_f = \{\langle m, n \rangle : f(m) = n\}$. Une fonction $f : \omega \to \omega$ est calculable si, et seulement si, son graphe est définissable par une for-mule $\Sigma_1$ de l'arithmétique (via l'ingénieux codage de Gödel, présenté dans la preuve du théorème 9-3.4), autrement dit s'il existe une formule $\Sigma_1 F(x, y)$ telle que $G_f = \{\langle m, n \rangle : \omega \models F(m, n)\}$, où $\omega$ dénote de modèle standard de PA.

## Remarque

Les graphes des fonctions calculables correspondent à des formules $\Sigma_1$ (en particulier sans paramètres du second ordre). Pour les fonctions $X$-calculables avec oracle $X$, la correspondance tient toujours, mais pour une formule $\Sigma_1^0$ utilisant le paramètre $X$.

**Définition 1.1.** On dit qu'une formule $F(x, y)$ de l'arithmétique (du premier ou du second ordre) est *fonctionnelle* si $\omega \models \forall x \exists! y F(x, y)$. ◇

Rappelons que la notation $\exists!y$ signifie « il existe un unique $y$ ». Notons que si une formule $\Sigma_1^0 F(x, y)$ est fonctionnelle, la fonction $f : \omega \to \omega$ qu'elle définit est bien de graphe $\Delta_1^0$, car pour toute fonction $f : \omega \to \omega$ (totale), on a $f(x) = y$ ssi $f(x) \neq z$ pour tout $z \neq y$. Formellement, la formule $F(x, y)$ s'exprime de manière $\Pi_1^0$ via la formule $\forall z \neq y \neg F(x, z)$. Attention toutefois, ce n'est par parce que $F(x, y)$ est fonctionnelle que le système RCA₀ peut le démontrer ; il se pourrait que dans certains modèles la relation $F(x, y)$ ne soit pas fonctionnelle à cause d'éléments $x$ non standard. Cela nous conduit à la définition suivante.
**Définition 1.2.** Une formule $F(x, y)$ de l'arithmétique (du premier ou du second ordre) est *T-prouvablement fonctionnelle* pour une théorie $T$ si $T \vdash \forall x \exists! y F(x, y)$, c'est-à-dire :

$$ T \vdash \forall x \exists y F(x, y) \quad \text{et} \quad T \vdash \forall x \forall y_0 \forall y_1 (F(x, y_0) \land F(x, y_1) \rightarrow y_0 = y_1). $$

Une fonction $f : \omega \to \omega$ est *T-prouvablement totale* s'il existe une formule $F(x, y)$ T-prouvablement fonctionnelle telle que $F(n, f(n))$ est vraie pour tout $n \in \omega$. Une fonction $f : \omega \to \omega$ est *T-prouvablement calculable* si elle est T-prouvablement totale via une formule $\Sigma_1$. ◇

**Formules $\Sigma_1$ vs $\Sigma_1^0$**

Notons que si $T \vdash \forall x \exists! y F(x, y)$ où $F$ est une formule $\Sigma_1^0$ avec une variable libre $Z$, cela équivaut à une preuve de $T \vdash \forall Z \forall x \exists! y! F(x, y)$. La fonction correspondante sera ainsi une fonctionnelle prouvablement totale sur tous les oracles $Z$.

La définition ci-dessus se généralise sans problème aux fonctions à plusieurs paramètres. La question principale de ce chapitre est donc la caractérisation des fonctions RCA₀-prouvablement calculables. Dans un premier temps, nous allons notamment montrer le résultat qui suit.

**Théorème 1.3**

Les fonctions primitives récursives sont RCA₀-prouvablement calculables.

Il s'agit d'un théorème qui va permettre de nous abstraire un peu du système d'axiomes RCA₀. Souvenons-nous de la caractérisation des fonctions primitives récursives comme celles que l'on peut calculer par des programmes structurés utilisant des boucles for, mais pas de boucles while (voir le théorème 6-3.22). Nous pouvons garder grâce à cela une certaine légèreté dans le formalisme, tout en restant rigoureux : pour montrer que l'utilisation d'une fonction calculable est valide dans RCA₀, il suffit de montrer qu'elle est primitive récursive.

Le théorème 1.3 va en fait plus loin, et l'on a la superbe caractérisation suivante.

**Théorème 1.4 (Parikh, voir Hajek et Pudlak [81])**

Les fonctions RCA₀-prouvablement calculables sont exactement les fonctions primitives récursives.

La réciproque est hélas bien plus complexe à démontrer et dépasse le cadre de cette ouvrage; nous donnerons toutefois dans la deuxième partie de ce chapitre (voir la section 7) certains éléments de la preuve.
Nous consacrons donc le début de ce chapitre à la preuve du théorème 1.3. Nous allons en fait montrer un résultat un peu plus fort : les fonctions primitives récursives définissables à l'aide d'un oracle Z quelconque sont prouvablement calculables quel que soit l'oracle dans la théorie RCA₀.

**Définition 1.5.** La classe des fonctions Z-primitives récursives est la plus petite classe de fonctions contenant les fonctions de base (successeur, projection, constantes), la fonction caractéristique de Z, et qui est close par le schéma de composition et de récursion primitive. ◇

Dans le cas d'une fonction primitive récursive sans oracle, la partie du premier ordre de RCA₀ —notée Σ₁-PA, c'est-à-dire l'arithmétique de Robinson et le schéma d'induction pour les formules Σ₁ — suffit pour montrer qu'elle est calculable. Il ne s'agit pas de quelque chose de bien surprenant, et nous verrons dans la deuxième partie de ce chapitre que tout énoncé du premier ordre démontrable dans RCA₀ est déjà démontrable dans Σ₁-PA.

## 2. Sous-systèmes faibles de PA

Afin de montrer le théorème 1.3, nous allons procéder à un codage des fonctions primitives récursives (éventuellement avec oracle) par des formules fonctionnelles Σ₁, similaire à celui qui fut présenté dans la preuve du théorème 9-3.4, à ceci près que nous allons cette fois devoir nous assurer que tout ce que nous faisons se formalise bien dans RCA₀. Le caractère fastidieux des développements à venir sera compensé par une compréhension détaillée des principaux axiomes de sous-systèmes faibles de l'arithmétique, menée notamment dans la section 3.

Même si nous étudions ici le premier ordre, nous nous plaçons dans le cadre de l'arithmétique du second ordre. Les différentes formules utilisées sont susceptibles de comporter des variables libres du second ordre. Pour la majorité des preuves qui suivent, cela n'a pas d'incidence.

### 2.1. L'arithmétique de Robinson

L'arithmétique de Robinson (notée Q) est, rappelons-le, un fragment de l'arithmétique de Peano à laquelle on a retiré le schéma d'induction. Ses axiomes sont précisés dans la section 9-2.3. Les axiomes de l'arithmétique de Robinson seuls forment un système très faible, au sein duquel à peu près aucun énoncé du type $∀x F(x)$ n'est démontrable.

Voici, à titre d'exemple, un modèle non standard de Q au sein duquel l'énoncé $∀x ¬(x < x)$ est faux.
**Exemple 2.1.** Soit $\mathcal{M} = (\omega \cup \{\infty\}, +, \times, <, 0, 1)$ la structure où $+, \times, <$ ont leur sens usuel sur $\omega$, et où

$$ \triangleright n + \infty = \infty + n = \infty \text{ pour } n \in \omega \cup \{\infty\}, $$

$$ \triangleright n \times \infty = \infty \times n = \infty \text{ pour } n \in (\omega \setminus 0) \cup \{\infty\}, $$

$$ \triangleright 0 \times \infty = \infty \times 0 = 0. $$

La structure $\mathcal{M}$ est un modèle de $\mathbb{Q}$. On laisse au lecteur le soin de vérifier que les axiomes de $\mathbb{Q}$ sont tous vérifiés dans ce modèle.

Notons que l'arithmétique de Robinson $\mathbb{Q}$ pourra tout de même démontrer des énoncés du type $\neg(\dot{n} < \dot{n})$ où $\dot{n}$ est le terme $(\dots(1+1)+\dots+1)$ — avec 1 répété $n$ fois —, mais sans être capable de faire une généralisation à tous les entiers.

**Exercice 2.2.** (⋆) Montrer que les énoncés

$$ \forall x, y \ x + y = y + x \text{ et } \forall x, y \ x \times y = y \times x $$

ne sont pas démontrables dans $\mathbb{Q}$.

◇

Afin de pouvoir utiliser les faits même les plus basiques sur les entiers, comme la commutativité de l'addition ou de la multiplication, il apparaît alors nécessaire d'utiliser un minimum d'induction.

## 2.2. Le schéma d'induction ouvert

Voyons pour commencer le schéma d'induction le plus basique possible, qui permet de démontrer les faits élémentaires concernant les entiers.

**Notation**

On dénote par $l_{\text{ouvert}}$ le schéma d'axiomes d'induction

$$ (F(0) \land \forall x (F(x) \rightarrow F(x+1))) \rightarrow \forall x F(x) $$

restreint aux formules sans quantificateur.

**Proposition 2.3.** La commutativité, l'associativité et l'injectivité de l'addition sont prouvables dans $\mathbb{Q} + l_{\text{ouvert}}$. Formellement,

$$ Q + l_{\text{ouvert}} \vdash \forall x, y \ x + y = y + x, $$

$$ Q + l_{\text{ouvert}} \vdash \forall x, y, z \ (x + y) + z = x + (y + z), $$

$$ Q + l_{\text{ouvert}} \vdash \forall x, y, z \ x + y = x + z \rightarrow y = z. $$

⋆

**PREUVE**

Commençons par la commutativité. Montrons d'abord $0 + x = x$ pour tout $x \in \mathbb{F}_1$. On a $0 + 0 = 0$ par (4) de $\mathbb{Q}$.

Supposons $0 + x = x$. Alors, $0 + (x + 1) = (0 + x) + 1$, par (5) de $\mathbb{Q}$. Par
l'hypothèse d'induction $(0+x)+1 = x+1$. Par $\mathbf{l}_{\text{ouvert}}$, on obtient $0+x = x$ pour tout $x$. Montrons à présent $(x+1)+y = (x+y)+1$ pour tous $x, y$ ($\mathbb{F}_2$). On a bien $(x+1)+0 = x+1 = (x+0)+1$, par (4) de $\mathbf{l}_{\text{ouvert}}$. Supposons $(x+1)+y = (x+y)+1$. Alors,

$$(x+1)+(y+1)=((x+1)+y)+1=((x+y)+1)+1=(x+(y+1))+1,$$

par (5) de $\mathbf{l}_{\text{ouvert}}$ et par l'hypothèse d'induction.

Par $\mathbf{l}_{\text{ouvert}}$, on obtient $(x+1)+y = (x+y)+1$ pour tous $x, y$. Montrons finalement la commutativité de l'addition. On a $x+0 = 0+x$ pour tout $x$, par (4) de $\mathbb{Q}$ et ($\mathbb{F}_1$). Supposons $x+y = y+x$. Alors, $x+(y+1) = (x+y)+1$, par (5) de $\mathbb{Q}$. Par hypothèse d'induction, $(x+y)+1 = (y+x)+1$. Par ($\mathbb{F}_2$), $(y+x)+1 = (y+1)+x$. Par $\mathbf{l}_{\text{ouvert}}$, on obtient $x+y = y+x$ pour tous $x, y$.

Passons à l'associativité. On a bien $(x+y)+0 = x+y = x+(y+0)$, par (4) de $\mathbb{Q}$. Supposons $(x+y)+z = x+(y+z)$. Alors,

$$(x+y)+(z+1)=((x+y)+z)+1=(x+(y+z))+1 \\ =x+((y+z)+1)=x+(y+(z+1)),$$

par (5) de $\mathbb{Q}$ et par hypothèse d'induction. Par $\mathbf{l}_{\text{ouvert}}$, on obtient l'associativité pour tous $x, y, z$.

Montrons pour finir l'injectivité. Comme on a $0+x = x$ pour tout $x$, alors $0+y = 0+z \rightarrow y = z$. Supposons $x+y = x+z \rightarrow y = z$. Puis supposons $(x+1)+y = (x+1)+z$. Alors, $(x+y)+1 = (x+z)+1$, par associativité et commutativité de l'addition. Par (2) de $\mathbb{Q}$ on a par conséquent $(x+y) = (x+z)$. Donc, $y = z$ par hypothèse d'induction, ce qui implique $y+1 = z+1$. Par $\mathbf{l}_{\text{ouvert}}$, on obtient l'injectivité pour tous $x, y, z$. ■

**Exercice 2.4.** (⋆) Montrer que les trois énoncés suivants sont prouvables dans $\mathbb{Q} + \mathbf{l}_{\text{ouvert}}$.

(1) La commutativité de la multiplication : $x \times y = y \times x$.

(2) La distributivité de la multiplication sur l'addition :

$$x \times (y + z) = x \times y + x \times z.$$

(3) L'associativité de la multiplication : $(x \times y) \times z = x \times (y \times z)$. ◇

L'injectivité de la multiplication sera plus facile à montrer en utilisant $<$.

**Notation**

On écrit $x \leq y$ comme raccourci pour l'énoncé $x = y \lor x < y$.
**Lemme 2.5.** Les énoncés suivants sont prouvables dans $\mathbb{Q} + I_{\text{ouvert}}$.

(1) Totalité de l'ordre : $x = y \lor x < y \lor y < x$. Chacun de ces cas est, de plus, mutuellement exclusif.

(2) Transitivité de la comparaison : $(x < y \land y \le z) \rightarrow x < z$.

(3) Addition d'inégalité : $(x_1 < y_1 \land x_2 \le y_2) \rightarrow x_1 + x_2 < y_1 + y_2$.

(4) Croissance de la multiplication : $x < x \times y$ pour $x \ne 0$ et $y \ne 0, 1$.

(5) L'injectivité de la multiplication : $(x \times y = x \times z \land x \ne 0) \rightarrow y = z$. ★

**PREUVE.** (1) Montrons $x = y \lor x < y \lor y < x$. Rappelons que par (8) de $\mathbb{Q}$ on a $x < y$ ssi $x + z = y$ pour $z \ne 0$. Pour $x = 0$ et $y$ quelconque, soit $y = 0$ auquel cas $x = y$, soit $y \ne 0$ auquel cas $x + y = y$ par (4) de $\mathbb{Q}$ et la commutativité de l'addition, et donc $x < y$. Supposons $x = y \lor x < y \lor y < x$ et montrons

$$ (x+1) = y \lor (x+1) < y \lor y < (x+1). $$

Si $x = y$, alors $y+1 = x+1$, et donc $y < x+1$. Si $x < y$, alors $x+z = y$ pour $z \ne 0$. Si $z = 1$, alors $x+1 = y$. Si $z \ne 1$, alors $z = z' + 1$ par (3) de $\mathbb{Q}$, pour $z' \ne 0$, car $z \ne 1$. En particulier, $x+(z'+1) = y$, et donc $(x+1)+z' = y$, par commutativité et associativité de l'addition. Donc, $x+1 < y$, par (8) de $\mathbb{Q}$. Finalement, si $y < x$, alors $y+z = x$ pour $z \ne 0$. Par suite, $(y+z)+1 = y+(z+1) = x+1$ par associativité de l'addition. Dès lors, $y < x+1$, par (8) de $\mathbb{Q}$. Par $I_{\text{ouvert}}$, on a donc $x = y \lor x < y \lor y < x$ pour tous $x, y$.

Montrons à présent que chaque cas est mutuellement exclusif. Si $x = y$, on ne peut avoir $x+z = y$ ou $y+z = x$ pour $z \ne 0$. En effet, par injectivité de l'addition, cela donnerait $z = 0$. Si $x < y$, alors $x+z = y$ pour $z \ne 0$. Supposons $y \le x$. Alors, $y+z' = x$ pour $z'$, ce qui donne $y+z'+z = y = y+0$, et donc $z'+z = 0$ par injectivité de l'addition, ce qui est absurde.

(2) Si $x < y$ et $y \le z$, alors $x+a = y$ pour $a \ne 0$ et $y+b = z$ pour $b$. Donc, $x+(a+b) = (x+a)+b = z$, par associativité de l'addition. Ainsi, $x < z$.

(3) Si $x_1 < y_1$ et $x_2 \le y_2$, alors $x_1 + z_1 = y_1$ pour $z_1 \ne 0$ et $x_2 + z_2 = y_2$. Donc, $(x_1 + x_2) + (z_1 + z_2) = (x_1 + z_1) + (x_2 + z_2) = y_1 + y_2$, par associativité et commutativité de l'addition. Ainsi, $x_1 + x_2 < y_1 + y_2$.

(4) Montrons $x < x \times y$ pour tout $x \ne 0$ et tout $y \ne 0, 1$. Pour $y = 2$, on a bien $x < x + x$, par (8) de $\mathbb{Q}$. Supposons à présent $x < x \times y$. Alors, $x < x \times y < x \times y + x = x \times (y+1)$. Par $I_{\text{ouvert}}$, on a bien $x < x \times y$ pour tout $x \ne 0$ et tout $y \ne 0, 1$.

(5) Montrons la contraposée de $(x \times y = x \times z \land x \ne 0) \rightarrow y = z$. Supposons $y \ne z$. Par (1) de ce lemme, $y < z$ ou $z < y$. Supposons $y < z$,
l'autre cas étant symétrique. Montrons alors par induction que pour tout $x \neq 0$, $x \times y < x \times z$. Pour $x = 1$, on a bien $x \times y = y < z = x \times z$. Soit $x \neq 0$ tel que $y < z$ implique $x \times y < x \times z$ pour tous $y, z$. Alors, $(x+1) \times y = x \times y + y$. Or, $x \times y < x \times z$ par l'hypothèse d'induction et $y < z$. Donc, par (3) de ce lemme,

$$(x+1) \times y = x \times y + y < x \times z + z = (x+1) \times z.$$

Par $l_{\text{ouvert}}$, on a bien $y < z \rightarrow x \times y < x \times z$ pour tout $x \neq 0$ et tous $y, z$. Par (1) de ce lemme, on a $x \times y < x \times z$ implique $x \times y \neq x \times z$. ■

**Exercice 2.6.** Montrer la multiplication d'inégalité dans $Q + l_{\text{ouvert}}$ :

$$(x < y \land z \neq 0) \rightarrow x \times z < y \times z. \quad \diamond$$

## 2.3. Le schéma d'induction $\Delta_0^0$

En dehors de faits basiques sur les entiers, le système $l_{\text{ouvert}}$ reste relativement faible. La définition de certaines fonctions simples nécessitera l'utilisation de quantificateurs bornés. Nous introduisons pour cela un système légèrement plus puissant.

**Notation**

On dénote par $l\Delta_0^0$ le schéma d'axiomes d'induction

$$(F(0) \land \forall x (F(x) \rightarrow F(x+1))) \rightarrow \forall x F(x)$$

restreint aux formules $\Delta_0^0$.

**Notation**

On écrit $x|y$ pour signifier que $x$ divise $y$, ce qui se formalise par l'énoncé $\Delta_0$ suivant : $\exists m \leq y, x \times m = y$.

**Exercice 2.7.** (⋆) Montrer la division euclidienne dans $Q + l\Delta_0^0$: pour tous $a, b$ avec $b \neq 0$, il existe un unique couple $q, r$ avec $0 \leq r < b$ tel que $a = qb + r$. ◦

**Lemme 2.8.** Les énoncés suivants sont prouvables dans $Q + l\Delta_0^0$ :

$$(1) \quad z|x \land z|y \rightarrow z|(x+y);$$

$$(2) \quad 2|x \lor 2|(x+1).$$

**PREUVE.** (1) Si $z \times m_1 = x$ et $z \times m_2 = y$, alors $z \times (m_1 + m_2) = x + y$.

(2) On a $2 \times 0 = 0$, donc $2|0$. Supposons $2|x \lor 2|(x+1)$. Si $2|(x+1)$, alors $2|(x+1) \lor 2|(x+2)$. Si $2|x$, comme aussi $2|2$, alors $2|(x+2)$. Par $l\Delta_0^0$, on en conclut $2|x \lor 2|(x+1)$ pour tout $x$. ■
**Lemme 2.9**

La fonction $\div : \omega^2 \to \omega$ définie par $a \div b$ égal à $z$ tel que $b+z = a$ si $b < a$, et par $a \div b = 0$ sinon, est prouvablement totale dans $\mathbb{Q} + |\Delta_0|$ via une formule $\Delta_0$. $\star$

**PREUVE**

La formule $\Delta_0$ qui définit $a \div b$ est $F(a, b, r) \equiv (b < a \land b + r = a) \lor r = 0$. Montrons l'existence. Pour tous $a, b$, si $b < a$, alors par (8) de $\mathbb{Q}$ il existe $r \neq 0$ tel que $b+r = a$. Si $b \ge a$, alors la formule est vérifiée pour $r = 0$. Montrons l'unicité. Supposons $F(a, b, r_1)$ et $F(a, b, r_2)$ vérifiées. Si $(b < a)$, alors $r_1 = r_2 = 0$. Si $b < a$, alors $b+r_1 = a$ et $b+r_2 = a$, donc $b+r_1 = b+r_2$, et donc $r_1 = r_2$, par injectivité de l'addition. $\blacksquare$

**Lemme 2.10.** Les énoncés suivants sont prouvables dans $\mathbb{Q} + |\Delta_0|$ :

$$ (1) \quad x \times (a \div b) = x \times a \div x \times b; $$

$$ (2) \quad \text{si } z|x \text{ et } z|y, \text{ alors } z|(x \div y). \quad \star $$

**PREUVE.** (1) Supposons $a \le b$. Alors, $x \times a \le x \times b$, par l'exercice 2.6. En particulier, $x \times (a \div b) = 0 = x \times a \div x \times b$. Supposons à présent $b < a$. Alors, $x \times b \le x \times a$, par l'exercice 2.6. Soit $r_0$ tel que $r_0 + b = a$. Soit $r_1$ tel que $r_1 + x \times b = x \times a$. Alors, $x \times r_0 + x \times b = x \times a$ ce qui nous donne $x \times r_0 = r_1$, ce qui donne bien $x \times (a \div b) = x \times a \div x \times b$.

$$ (2) \quad \text{Soient } m_1, m_2 \text{ tels que } z \times m_1 = x \text{ et } z \times m_2 = y. \text{ Par (1),} $$

$$ z \times m_1 \div z \times m_2 = x \div y. $$

$$ \text{Donc, } z \times (m_1 \div m_2) = x - y. \text{ Ainsi, } z|(x \div y). \quad \blacksquare $$

**Lemme 2.11.** La bijection de Cantor $\langle \cdot \rangle : \omega^2 \to \omega$ et ses projections sont prouvablement totales dans $\mathbb{Q} + |\Delta_0|$ via une formule $\Delta_0$. $\star$

**PREUVE.** La fonction de couplage est définie par la formule

$$ F(x, y, r) \equiv r \times 2 = (x + y)(x + y + 1) + 2y. $$

Montrons l'existence. Par le lemme 2.8, soit $2|(x+y)$, soit $2|(x+y+1)$. Donc, toujours par le lemme 2.8, $2|(x+y)(x+y+1)+2y$. Donc, $\exists r F(x, y, r)$. L'unicité est claire par injectivité de la multiplication.

Nous avons montré dans l'exercice 2-3.7 que la fonction de couplage ainsi définie était bijective et croissante sur chacun de ses paramètres. On laisse au lecteur le soin de vérifier que cette preuve se formalise dans $|\Delta_0|$. Les projections sont définies par les deux formules suivantes :

$$ P_1(z, r) \equiv \exists x \le z \langle x, r \rangle = z, \quad P_2(z, r) \equiv \exists y \le z \langle r, y \rangle = z. $$

L'existence et l'unicité découlent du caractère bijectif de la fonction de couplage. $\blacksquare$
## 3. Hiérarchies d'induction

Afin de continuer plus loin notre démonstration du fait que les fonctions primitives récursives sont prouvablement calculables dans $RCA_0$, nous avons besoin d'examiner quelques conséquences de l'induction, utilisées couramment en mathématique sans que l'on y réfléchisse.

1. Le principe de collection bornée : tout ensemble fini d'entiers possède une borne supérieure.

2. Le principe de minimum : tout ensemble non vide d'entiers admet un plus petit élément.

En présence d'une induction restreinte, chacun des deux principes ci-dessus l'est lui aussi. Nous allons comprendre de quelle manière la restriction de l'induction impacte ces principes, et étudier leurs différents liens.

**Notation**

Soit $n > 0$. On dénote par $|\Sigma_n^0$ (resp. $|\Pi_n^0$) le schéma d'axiomes d'induction ($F(0) \wedge \forall x (F(x) \rightarrow F(x+1))$) $\rightarrow \forall x F(x)$ restreint aux formules $\Sigma_n^0$ (resp. $\Pi_n^0$).

### 3.1. Le schéma de collection bornée

Le principe de collection bornée — tout ensemble fini d'entiers admet une borne supérieure — est évident quand on définit par $\langle$ ensemble fini $\rangle$ les ensembles d'éléments qui justement sont bornés : il s'agit alors d'une tautologie. Le principe devient moins évident quand on définit les ensembles finis comme étant ceux que l'on peut mettre en bijection avec $\{0, 1, \dots, n\}$ pour un certain $n$. On appelle *axiome de collection bornée* pour une formule $F(x, y)$ l'énoncé :

$$ \forall n ((\forall x < n \exists y F(x, y)) \rightarrow \exists b \forall x < n \exists y < b F(x, y)). \quad (13) $$

**Notation**

Soit $n > 0$. On désigne par $B\Sigma_n^0$ (resp. $B\Pi_n^0$) le schéma d'axiomes de collection bornée restreint aux formules $\Sigma_n^0$ (resp. $\Pi_n^0$).

**Dans les modèles non standard.** Soit $M$ un modèle non standard, et soit un entier non standard $a \in M$. Nous pouvons définir une fonction $f$ de $\{b : b < a\}$ vers $M$ qui ne soit pas bornée dans $M$ (on peut même définir une bijection, $M$ étant dénombrable). Bien entendu, si $M$ est un modèle du schéma de collection bornée, une telle fonction ne peut être définie par une formule de l'intérieur de $M$. À l'inverse, si $M$ n'est pas modèle du
schéma de collection bornée pour les formules $\Sigma_n^0$, cela signifie qu'il existe un élément $a$ et une formule $\Sigma_n^0 F(x, y)$ tels que pour tout $x < a$ il existe au moins un élément $y$ pour lequel $F(x, y)$ est vrai, et tel que ces éléments $y$ sont non bornés dans $M$.

**Clôture des formules $\Sigma_n^0$ et $\Pi_n^0$ par quantifications bornées.** De nom-
breuses preuves font appel au fait que les différents niveaux de la hiérarchie
arithmétique sont clos par quantification bornée.

Ainsi, pour une formule $\Sigma_1^0$ de la forme $\exists y F(x, y)$ avec $F(x, y) \Delta_0^0$, la formule $\exists a \forall y < a \exists y F(x, y)$ est elle aussi considérée comme étant $\Sigma_1^0$. Cela a été démontré via la proposition 9-3.3 et vient du fait que l'on peut la récrire sous la forme $\exists a \exists b \forall y < a \exists y < b F(x, y)$. L'équivalence entre les deux formules nécessite cependant l'axiome de collection bornée, et n'est donc pas garantie dans les modèles ne le vérifiant pas pour la formule $F$. Nous montrons ici que cet axiome est suffisant pour garantir la proposition 9-3.3.

**Proposition 3.1 (Parsons [171]).** Soient $F_1(\bar{a}, x)$, $F_2(\bar{a}, x)$ et $F(\bar{a}, x)$ des formules $\Sigma_n^0$ (resp. $\Pi_n^0$) pour $n > 0$. Alors, chacune des trois formules suivantes est prouvablement équivalente dans $Q + I\Delta_0^0 + B\Sigma_n^0$, ainsi que dans $Q + I\Delta_0^0 + B\Pi_n^0$, à une formule $\Sigma_n^0$ (resp. $\Pi_n^0$) :

(i) $F_1(\bar{a}, x) \wedge F_2(\bar{a}, x), F_1(\bar{a}, x) \vee F_2(\bar{a}, x)$;

(ii) $\exists x < b F(\bar{a}, x), \forall x < b F(\bar{a}, x)$;

(iii) $\exists x F(\bar{a}, x)$ (resp. $\forall x F(\bar{a}, x)$).

*

**PREUVE.** Soient

$F(\bar{a}, x) \equiv \exists y G(\bar{a}, x, y)$, $F_1(\bar{a}, x) \equiv \exists y G_1(\bar{a}, x, y)$ et $F_2(\bar{a}, x) \equiv \exists y G_2(\bar{a}, x, y)$.

Considérons les énoncés suivants :

$$F_1(\bar{a}, x) \wedge F_2(\bar{a}, x) \leftrightarrow \exists y \exists y_1, y_2 < y (G_1(\bar{a}, x, y_1) \wedge G_2(\bar{a}, x, y_2)); \quad (a)$$

$$F_1(\bar{a}, x) \vee F_2(\bar{a}, x) \leftrightarrow \exists y (G_1(\bar{a}, x, y) \vee G_2(\bar{a}, x, y)); \quad (b)$$

$$\exists x < b F(\bar{a}, x) \leftrightarrow \exists y \exists x < b G(\bar{a}, x, y); \quad (c)$$

$$\forall x < b F(\bar{a}, x) \leftrightarrow \exists z \forall x < b \exists y < z G(\bar{a}, x, y); \quad (d)$$

$$\exists x F(\bar{a}, x) \leftrightarrow \exists z \exists x < z \exists y < z G(\bar{a}, x, y). \quad (e)$$

À présent, si $F, F_1, F_2$ sont $\Sigma_1^0$ avec $G, G_1, G_2 \Delta_0^0$, alors les quatre équiva-
lences (a) (b) (c) (e) sont aisément démontrables dans $I\Delta_0^0$. L'équivalence (d)
découle quant à elle directement de l'axiome de collection bornée pour $G$ qui
est $\Delta_0^0$. Donc, les formules de (i),(ii),(iii) sont prouvablement équivalentes
à des formules $\Sigma_1^0$ dans $B\Sigma_1^0$ et dans $B\Pi_1^0$. Par passage à la négation, les
formules de (i), (ii), (iii) sont prouvablement équivalentes à des formules $\Pi_1^0$
dans $B\Sigma_1^0$ et dans $B\Pi_1^0$, pour le cas où $F, F_1, F_2$ sont $\Pi_1^0$.

Supposons la proposition vraie pour les cas $\Sigma_n^0$ et $\Pi_n^0$. Alors, si $F, F_1, F_2$ sont des formules $\Sigma_{n+1}^0$ avec $G, G_1, G_2 \Pi_n^0$, de la même manière $B\Sigma_{n+1}^0$ ou $B\Pi_{n+1}^0$
montrent les équivalences (a) (b) (c) (d) (e). Comme $B\Sigma_{n+1}^0$ ou $B\Pi_{n+1}^0$ démontrent $B\Sigma_n^0$, et par hypothèse d'induction sur $G, G_1, G_2$, les formules de (i), (ii), (iii) sont prouvablement équivalentes à des formules $\Sigma_{n+1}^0$ dans $B\Sigma_{n+1}^0$ ou dans $B\Pi_{n+1}^0$. Par passage à la négation, les trois formules de (i),(ii),(iii) sont prouvablement équivalentes à des formules $\Pi_{n+1}^0$ dans $B\Sigma_{n+1}^0$ ou dans $B\Pi_{n+1}^0$, dans le cas où $F, F_1, F_2$ sont $\Pi_{n+1}^0$. ■

**L'induction implique le schéma de collection.** Le schéma de collection bornée ne fait pas partie des axiomes usuels de l'arithmétique. Nous voyons ici comment il découle de l'induction. Nous commençons d'abord par montrer que le schéma de collection pour les formules $\Pi_n^0$ permet de le montrer pour les formules $\Sigma_{n+1}^0$.

**Proposition 3.2 (Paris et Kirby [170]).** Soit $n > 0$. Alors,

$$Q + I\Delta_0^0 \vdash B\Pi_n^0 \leftrightarrow B\Sigma_{n+1}^0. \quad \star$$

**PREUVE.** L'implication $B\Sigma_{n+1}^0 \rightarrow B\Pi_n^0$ est immédiate. Supposons $B\Pi_n^0$. Soit $\exists zF(x, y, z)$ une formule $\Sigma_{n+1}^0$ avec $F \ \Pi_n^0$, et soit $a \in \mathbb{N}$ tel que

$$\forall x < a \exists y (\exists zF(x, y, z)).$$

On a alors $\forall x < a \exists v \exists y, z < v F(x, y, z)$. En utilisant $B\Pi_n^0$, par la proposition 3.1 soit $G(x, v)$ une formule $\Pi_n^0$ équivalente à $\exists y, z < v F(x, y, z)$. Alors, par $B\Pi_n^0$ on a $\exists b \ \forall x < a \ \exists v < b G(x, v)$, qui est alors équivalent à $\exists b \ \forall x < a \ \exists v < b \exists y, z < v F(x, y, z)$, ce qui implique

$$\exists b \ \forall x < a \exists y < b (\exists zF(x, y, z)). \quad \blacksquare$$

Voyons à présent comment montrer le schéma de collection à l'aide du schéma d'induction.

**Théorème 3.3 (Paris et Kirby [170])**

Soit $n > 0$. Alors, $Q \vdash I\Sigma_n^0 \rightarrow B\Sigma_n^0$.

**PREUVE.** Par induction sur $n$. Comme $Q + I\Delta_0^0 \vdash B\Sigma_{n+1}^0 \leftrightarrow B\Pi_n^0$, montrons $Q \vdash I\Sigma_{n+1}^0 \rightarrow B\Pi_n^0$. Soit $a \in \mathbb{N}$ et soit $F(x, y)$ une formule. Considérons les formules

$$G \equiv \forall x < a \exists y F(x, y) \text{ et } H(a') \equiv \exists b \forall x < a' \exists y < b (a' \le a \rightarrow F(x, y)).$$

Supposons $G$. Dans le cas où $F(x, y)$ est $\Delta_0^0$, alors $H(a')$ est $\Sigma_1^0$. Or, $H(0)$ est trivalement vrai, et l'on déduit par $G$ que $H(a') \rightarrow H(a' + 1)$ (il y a ici un argument que nous laissons au lecteur). Par $I\Sigma_1^0$, on a donc $\forall a' H(a')$, et donc $H(a)$, ce qui implique $\exists b \forall x < a \exists y < b F(x, y)$.
Supposons à présent $Q \vdash \mathrm{I}\Sigma_n^0 \to \mathrm{B}\Sigma_n^0$ avec $F(x, y)$ une formule $\Pi_n^0$. Alors, $H$ est équivalente à une formule $\Sigma_{n+1}^0$ par $\mathrm{B}\Sigma_n^0$. On procède alors comme dans le paragraphe précédent. Ainsi, pour tout $n \in \omega$, on a $Q \vdash \mathrm{I}\Sigma_n^0 \to \mathrm{B}\Sigma_n^0$. $\blacksquare$

## 3.2. Le schéma de minimum

Le schéma de minimum nous dit informellement que tout ensemble d'entiers non vide a un plus petit élément. Formellement, on appelle *axiome de minimum* pour une formule $F(x)$ l'énoncé :

$$ \exists x F(x) \rightarrow \exists x (F(x) \land \forall y < x \neg F(y)). \quad (14) $$

**Notation**

Soit $n > 0$. On dénote par $\mathrm{L}\Sigma_n^0$ (resp. $\mathrm{L}\Pi_n^0$) le schéma d'axiomes de minimum restreint aux formules $\Sigma_n^0$ (resp. $\Pi_n^0$).

**Dans les modèles non standard.** Dans un modèle non standard $M$, une *coupure* est un segment initial strict de $M$, non vide et clos par successeur. Par exemple, la partie standard $\omega$ d'un modèle non standard est toujours une coupure. Si un élément $a$ est dans le complémentaire d'une coupure, c'est aussi nécessairement le cas pour $a - 1$, car une coupure est close par successeur. On en déduit que si une coupure est définissable par une formule $F$, cela contredit directement le schéma de minimum pour la formule $\neg F$. Il s'agit en fait d'une condition nécessaire et suffisante. En effet, si $A = \{x : F(x)\}$ est un ensemble non vide qui n'a pas de plus petit élément, alors l'ensemble des éléments strictement plus petits que tout élément de $A$ est nécessairement une coupure. On en déduit le principe suivant.

**Principe de débordement (overspill)**

L'ensemble des entiers standard n'est jamais définissable dans un modèle qui respecte le schéma de minimum. En particulier, si une formule est vérifiée par tous les entiers standard, elle le sera nécessairement aussi pour un entier non standard.

**L'induction équivaut au schéma de minimum.** Nous voyons à présent que le schéma de minimum est, à peu de chose près, une simple reformulation de l'induction : si l'ensemble $\{x : F(x)\}$ est non vide et n'a pas de plus petit élément, c'est que l'induction rate pour la formule qui définit la coupure que l'on peut créer à partir de $F(x)$.
**Proposition 3.4.** Soit $n > 0$. Alors, $Q \vdash |\Sigma_n^0 \leftrightarrow \Pi_n^0$ et $Q \vdash |\Pi_n^0 \leftrightarrow L\Sigma_n^0$.★

PREUVE. On montre l'équivalence $|\Sigma_n^0 \leftrightarrow \Pi_n^0$, l'autre se montrant de manière identique.

Supposons $\neg|\Sigma_n^0$. Soit $F(x)$ une formule $\Sigma_n^0$ telle que $F(0), F(x) \to F(x+1)$, mais telle que l'ensemble $A = \{x : \neg F(x)\}$ est non vide. Par contra- posée, $\neg F(x) \to \neg F(x-1)$. Donc, $A$ n'a pas de plus petit élément. On a ainsi $\neg L\Pi_n^0$.

Supposons à présent $\neg L\Pi_n^0$, et supposons $|\Sigma_n^0$ par l'absurde. Soit $F(x)$ une formule $\Pi_n^0$ telle que l'ensemble $A = \{x : F(x)\}$ est non vide et n'a pas de plus petit élément. Soit $G(x) \equiv \forall y \le x \neg F(y)$. Par $|\Sigma_n^0$ qui im- plique $B\Sigma_n^0$, $G(x)$ est prouvablement équivalente à une formule $\Sigma_n^0$. Notons que $\neg F(0)$, car sinon $A$ aurait un plus petit élément. Donc, $G(0)$. Suppo- sons $G(x)$. Si l'on avait $F(x+1)$, alors $A$ aurait un plus petit élément. Par suite, $\neg F(x+1)$, ainsi que $G(x+1)$. On a ainsi $G(0) \wedge (G(x) \to G(x+1))$, mais $G(x)$ n'est vérifié pour aucun élément de $A$, qui est non vide. On a donc $\neg|\Sigma_n^0$. On a là une contradiction. ■

Le théorème suivant est particulièrement intéressant : en utilisant les pro- priétés des entiers, on montre que l'induction pour les formules $\Sigma_n^0$ est équivalente à l'induction pour les formules $\Pi_n^0$.

**Théorème 3.5 (Paris et Kirby [170])**

Soit $n > 0$. Alors, $Q \vdash |\Sigma_n^0 \leftrightarrow \Pi_n^0$.

PREUVE. Montrons $Q \vdash |\Sigma_n^0 \to \Pi_n^0$. Supposons que $|\Pi_n^0$ échoue, mais pas $|\Delta_0^0$ (afin de pouvoir utiliser les faits basiques sur les entiers). Soit $F(x)$ une formule $\Pi_n^0$ telle que $F(0)$ et $\forall x(F(x) \to F(x+1))$, mais $\neg F(a)$ pour un entier $a > 0$. Soit $G(y)$ la formule $\exists x (a = x + y \wedge \neg F(x))$. Remarquons que la formule $G(y)$ est équivalente à une formule $\Sigma_n^0$, en déca- lant $\ll a = x+y\gg$ vers sa partie $\Delta_0^0$. De plus, $G(0)$ est vrai et $G(a)$ est faux. Soit $y$ tel que $G(y)$ est vrai. En particulier, il existe un $x$ tel que $a = x + y$ et $\neg F(x)$. Nécessairement, $y < a$, donc $x > 0$ ; or, $a = (x-1) + (y+1)$ et par hypothèse, $\neg F(x) \to \neg F(x-1)$, donc $G(y+1)$ est vrai. Comme $G(0)$ et $\forall y (G(y) \to G(y+1))$ et $\neg G(a)$, alors $|\Sigma_n^0$ échoue.

Montrons $Q \vdash \Pi_n^0 \to |\Sigma_n^0$. Supposons que $|\Sigma_n^0$ échoue mais pas $|\Delta_0^0$. Soit $F(x)$ une formule $\Sigma_n^0$ telle que $F(0)$ et $\forall x(F(x) \to F(x+1))$, mais $\neg F(a)$ pour un entier $a > 0$. Soit $H(y)$ la formule $\forall x (a = x + y \to \neg F(x))$. Comme précédemment, $H(y)$ est équivalente à une formule $\Pi_n^0$. De plus, $H(0)$ est vrai et $H(a)$ est faux. On montre également $H(y) \to H(y+1)$. Ainsi, $H(0)$ et $\forall y (H(y) \to H(y+1))$ et $\neg H(a)$, donc $\Pi_n^0$ échoue. ■
**Exercice 3.6. (*) (Hájek et Pudlák [81]).** On appelle schéma d'induction ordonnée pour toute formule $F(x)$ l'énoncé

$$ \forall x((\forall y < x F(y)) \rightarrow F(x)) \rightarrow \forall x F(x). $$

Montrer que pour tout $n \in \omega$, Q prouve l'équivalence entre $\mathbb{I}\Sigma_n^0$ (resp. $\mathbb{I}\Pi_n^0$) et le schéma d'induction ordonnée pour les formules $\Sigma_n^0$ (resp. $\Pi_n^0$). ◇

### 3.3. Collection et induction $\Delta_n^0$

Nous avons vu que $\mathbb{B}\Sigma_n^0$ se déduisait de $\mathbb{I}\Sigma_n^0$. Nous voyons à présent que sous réserve d'avoir un minimum d'induction ($\mathbb{I}\Delta_0^0$), le schéma de collection pour toutes les formules implique le schéma d'induction pour toutes les formules. Plus précisément, on dispose du résultat qui suit.

**Théorème 3.7 (Paris et Kirby [170])**

$$ \text{Soit } n > 0. \text{ Alors, } \mathbb{Q} + \mathbb{I}\Delta_0^0 \vdash \mathbb{B}\Sigma_{n+1}^0 \rightarrow \mathbb{I}\Sigma_n^0. $$

**PREUVE.** Par induction sur $n$.

Supposons $\mathbb{B}\Sigma_{n+1}^0$. Soit $F(x) \equiv \exists y G(x, y)$ pour $G$ une formule $\Pi_{n-1}^0$ (ou $\Delta_0^0$ si $n=1$). Supposons $F(0)$ et $\forall x(F(x) \rightarrow F(x+1))$. Soit $a \in \mathbb{N}$. Montrons $F(a)$. Nous avons

$$ \forall x \le a (\exists y G(x, y) \rightarrow \exists u G(x+1, u)). $$

Autrement dit,

$$ \forall x \le a \exists u (\exists y G(x, y) \rightarrow G(x+1, u)). $$

Par $\mathbb{B}\Pi_n^0$ (équivalent à $\mathbb{B}\Sigma_{n+1}^0$), il existe $b \in \mathbb{N}$ tel que

$$ \forall x \le a \exists u \le b (\exists y G(x, y) \rightarrow G(x+1, u)), $$

ce qui implique

$$ \forall x \le a \exists u \le b (\exists y \le b G(x, y) \rightarrow G(x+1, u)), $$

et donc

$$ \forall x \le a (\exists y \le b G(x, y) \rightarrow \exists u \le b G(x+1, u)). $$

Soit $H(x) \equiv x \le a \rightarrow (\exists u \le b G(x, u))$. Si $n=1$, la formule $G(x, u)$ est $\Delta_0^0$ et donc aussi la formule $H(x)$. Par $\mathbb{I}\Delta_0^0$, on a donc $H(x)$ pour tout $x$. Si $n > 1$, la formule $G(x, u)$ est $\Pi_{n-1}^0$. Par $\mathbb{B}\Sigma_{n+1}^0$, la formule $H(x)$ est donc équivalente à une formule $\Pi_{n-1}^0$. Par hypothèse d'induction, on a $\mathbb{I}\Sigma_{n-1}^0$ (qui implique $\mathbb{I}\Pi_{n-1}^0$ par le théorème 3.5), et l'on a donc $H(x)$ pour tout $x$. Dans tous les cas, on a $H(x)$ pour tout $x$. En particulier, $H(a)$ est vrai, donc $\exists u \le b G(a, u)$, et donc $F(a)$. ■

Il est possible d'affiner la seconde implication, et montrer que $\mathbb{B}\Sigma_n^0$ implique l'induction pour les formules prouvablement $\Delta_n^0$.
**Notation**

Soit $n > 0$. On note $|\Delta_n^0$ le schéma d'axiomes

$$ \forall x(F(x) \leftrightarrow G(x)) \rightarrow ((F(0) \land F(n) \rightarrow F(n+1)) \rightarrow \forall n F(n)) $$

restreint aux formules $F, G$ avec $F \Sigma_n^0$ et $G \Pi_n^0$.

**Théorème 3.8 (Hájek et Pudlák [81])**

$$ \text{Soit } n > 0. \text{ Alors, } Q + |\Delta_0^0 \vdash B\Sigma_n^0 \rightarrow |\Delta_n^0. $$

**PREUVE.** Supposons $B\Sigma_n^0$. Soient $\exists y F(x, y)$ et $\forall x G(x, y)$ des formules respectivement $\Sigma_n^0$ et $\Pi_n^0$ telles que $\forall x$ ($\exists y F(x, y) \leftrightarrow \forall y G(x, y)$). Supposons $\exists y F(0, y)$ et $\forall x$ ($\exists y F(x, y) \rightarrow \exists y F(x + 1, y)$).

Soit $a \in \mathbb{N}$. Montrons $\exists y F(a, y)$. On a

$$ \forall x \exists y (F(x, y) \lor \neg G(x, y)). $$

Donc, par $B\Sigma_n^0$, il existe $b \in \mathbb{N}$ tel que

$$ \forall x \le a \exists y \le b (F(x, y) \lor \neg G(x, y)). $$

Soit $H(x) \equiv (x \le a \rightarrow (\exists y \le b F(x, y)))$. Par hypothèse sur $F$ et $G$, on a $H(0)$ et $H(x) \rightarrow H(x + 1)$. Par $B\Sigma_n^0$, la formule $H(x)$ est équivalente à une formule $\Pi_{n-1}^0$. Comme $B\Sigma_n^0 \rightarrow |\Sigma_{n-1}^0$ et $|\Sigma_{n-1}^0 \leftrightarrow |\Pi_{n-1}^0$, alors on a $H(x)$ pour tout $x$. En particulier, $\exists y F(a, y)$. $\blacksquare$

Ainsi, $B\Sigma_n^0$ se situe entre $|\Sigma_n^0$ et $|\Delta_n^0$. La question de savoir si $|\Delta_n^0$ implique en retour $B\Sigma_n^0$ est restée ouverte pendant plus d'une décennie, avant d'être résolue par Slaman en 2002, en utilisant toutefois la théorie $Q + |\Sigma_1^0$ comme théorie de base.

**Théorème 3.9 (Slaman [204])**

$$ \text{Soit } n > 0. \text{ Alors, } Q + |\Sigma_1^0 \vdash B\Sigma_n^0 \leftrightarrow |\Delta_n^0. $$

La preuve de l'implication $|\Delta_n^0 \rightarrow B\Sigma_n^0$ fait appel à des techniques avancées de codage dans les modèles non standard de l'arithmétique. Il n'existe pas à ce jour de preuve syntaxique de cette implication.

## 3.4. Schéma récapitulatif

Nous avons donc pour l'instant dans $Q + |\Delta_0^0$ (et donc dans $RCA_0$) la hiérarchie d'induction suivante, visible sur la figure 3.10.

Il est possible de montrer que les implications réciproques de la figure ne tiennent pas. Cela se fait via la construction de modèles non standard, au
<figure><img src="image_142.png" /><figcaption>FIGURE 3.10 – Hiérarchie d’induction. Les flèches indiquent une implication dans $Q + I\Sigma_n^0$.</figcaption></figure>

sein desquels par exemple $B\Sigma_n^0$ est valide, mais pas $I\Sigma_n^0$. Le lecteur qui souhaite en apprendre davantage pourra consulter [109] ou [81].

## 4. Fonctions primitives récursives et RCA₀

Nous avons à présent les éléments nécessaires pour démontrer que les fonctions primitives récursives sont prouvablement calculables dans RCA₀. La preuve passe par un codage des suites finies par des entiers, via une technique similaire à celle utilisée pour la fonction $\beta$ de Gödel (voir le lemme 9 -3.6), mais ne reposant pas sur le théorème des restes chinois. L’unicité de la décomposition des nombres en facteurs premiers sera un élément clef de notre codage, plus particulièrement le lemme de Gauss. On rappelle que deux entiers naturels $a, b$ sont premiers entre eux si 1 est leur seul diviseur commun. Il s’agit d’une formule $\Delta_0$.

**Lemme 4.1 (Lemme de Gauss).** Le système $Q + I\Delta_0^0$ montre que pour tous nombres $p, a, b$ tels que $p$ et $b$ sont premiers entre eux, si $p|ab$, alors $p|a★$

**PREUVE.** Fixons $p, b$ premiers entre eux. Supposons par l’absurde que le lemme de Gauss est faux, i.e. que l’ensemble $\{a \neq 0 : p|ab \text{ et } \neg p|a\}$ est non vide. Par schéma de minimum pour les formules $\Delta_0$, soit $a$ le plus petit élément de cet ensemble. Montrons $a < p$. Supposons par l’absurde $a \ge p$. Alors, par la division euclidienne (voir l’exercice 2.7), il existe $q, r$ avec $r < p$ tels que $a = pq + r$. Comme $\neg p|a$, alors $r \neq 0$. Comme $p|(pq + r)b$ alors $p|pqb + rb$. Or, $p|pqb$, donc $p|rb$. Cependant, comme $r < p$, on a $\neg p|r$, ce qui contredit la minimalité de $a$. Donc, $a < p$. À présent, soit $p = aq + r$ avec $0 \le r < a$. Montrons $r \neq 0$. Supposons $p = aq$. Comme $\neg p|a$,
alors $q > 1$. Comme $p|ab$, alors $aq|ab$, et donc $q|b$. Donc, $q$ est un diviseur commun différent de 1 de $b$ et $p$, ce qui contredit nos hypothèses. Ainsi, $r \neq 0$. On a alors $bp = baq + br$, donc $br = bp \div baq$. Comme $p|bp$ et $p|baq$, alors $p|br$. Or, $0 < r < a < p$, donc $\neg p|r$, ce qui contredit la minimalité de $a$. ■

Notre codage des listes repose sur la capacité à générer des suites de nombres tous deux à deux premiers, de la manière suivante.

**Lemme 4.2.** Soit $x$ fixé, et soit $a$ un entier multiple de tous les entiers $i$ pour $1 \le i \le x$. Le système $Q + |\Delta_0^0|$ montre que pour $i, j \le x$ avec $i \neq j$ les nombres $a(i+1)+1$ et $a(j+1)+1$ sont premiers entre eux. ★

**PREUVE.** Supposons par l'absurde qu'un nombre premier $p$ divise les deux entiers $a(i+1)+1$ et $a(j+1)+1$ avec $i < j$. Alors aussi, $p$ divise

$$a(j+1) + 1 - a(i+1) + 1 = a(j \div i).$$

Comme $p$ est premier, d'après le lemme de Gauss, $p$ divise $a$ ou $p$ divise $j \div i$. Par hypothèse sur $a$, dans tous les cas, $p$ divise $a(i+1)$. Comme $p$ divise également $a(i+1)+1$, alors $p$ divise $a(i+1)+1 \div a(i+1) = 1$, ce qui est une contradiction. Donc, les nombres $a(i+1)+1$ et $a(j+1)+1$ sont premiers entre eux. ■

L'idée de codage de nos listes est la suivante. Étant donné $x_0, x_1, \dots, x_{n-1}$, nous commençons par choisir $a$ multiple de tous les entiers $z$ compris (au sens large) entre 1 et $\max\{\langle i, x_i \rangle : i < n\}$. Notre liste est alors codée par le couple $(a, b)$ tel que $b = \Pi_{i<n}(a(\langle i, x_i \rangle + 1) + 1)$. Étant donné $(a, b)$, le i-ième élément de notre liste est donné par l'unique $z \le a$ tel que $\langle i, z \rangle \le a$ et tel que $(a(\langle i, x_i \rangle + 1) + 1)|b$.

**Notation**

Pour un entier $a$, on note $p_i^a$ l'entier $a(i+1)+1$.

**Définition 4.3.** Un couple $(a, b)$ code pour une suite de taille $n$ si

$$\forall i < n \exists! x \le a \langle i, x \rangle \le a \wedge p_{\langle i, x \rangle}^a |b.$$

<figure><img src="image_143.png" /></figure>

**Notation**

Pour un couple $(a, b)$ qui code pour une suite de taille $n$, et pour $i < n$, on note $(a, b)_i$ l'unique entier $x \le a$ tel que $\langle i, x \rangle \le a \wedge p_{\langle i, x \rangle}^a |b$.

Notre première utilisation de l'induction $\Sigma_1^0$ sera pour montrer l'existence d'un entier $a$ multiple de suffisamment d'éléments pour coder nos suites.
**Lemme 4.4.** Le système RCA₀ montre que, pour tout $x \in \mathbb{N}$, il existe un plus petit entier $y \in \mathbb{N}$ qui est multiple de tous les entiers $i$ pour $1 \le i \le x$.★

**PREUVE.** Montrons l'existence. C'est clair pour $x = 0$. Supposons l'existence pour $x$. Soit $y$ un multiple de tous les entiers plus petits que $x$. On montre dans $\mathbb{Q} + \mathbb{I}\Delta_0^0$ que les diviseurs de $y$ sont aussi des diviseurs de $y \times (x+1)$, et que $x+1$ est diviseur de $y \times (x+1)$. Par $\mathbb{I}\Sigma_1^0$, l'existence est assurée pour tout $x$. En particulier, pour $x$ fixé, l'ensemble

$$ \{y : \forall 1 \le i \le x \ i | y\} $$

est non vide. On applique enfin le schéma de minimum pour les formules $\Delta_0$ pour obtenir le plus petit élément. ■

Nous pouvons à présent passer au codage des suites finies.

**Lemme 4.5**

Supposons que $(a, b)$ code pour une suite de taille $n$. Alors, RCA₀ montre que pour tout $r$ il existe un couple $(a', b')$ qui code pour une suite de taille $n+1$, tel que $(a', b')_n = r$ et tel que $\forall i < n \ (a', b')_i = (a, b)_i$. ★

**PREUVE.** Montrons d'abord l'énoncé suivant : si $(a, b)$ code pour une suite de taille $n$, alors pour tout $a'$ tel que les diviseurs de $a$ sont tous des diviseurs de $a'$, il existe $b'$ tel que $(a', b')_i = (a, b)_i$ pour tout $i < n$.

Supposons que ce soit le cas pour $n$. Soit $(a, b)$ codant pour une suite de taille $n+1$ et $a'$ tel que les diviseurs de $a$ sont tous des diviseurs de $a'$. Alors, $(a, b)$ code aussi pour une suite de taille $n$. Donc, par hypothèse d'induction, il existe $b'$ tel que $(a, b)$ et $(a', b')$ codent pour la même suite de taille $n$. Soit $b'$ le plus petit entier de la sorte (schéma de minimisation $\Delta_0$). Alors, $(a', b')$ ne code pas pour une suite de taille $n+1$ car si $m \times p_{\langle n, x \rangle}^{a'} = b'$, alors $(a', m)$ code pour la même suite de taille $n$ que $(a, b)$ — par application du lemme de Gauss et le fait que $p_{\langle n, x \rangle}^{a'}$ et $p_{\langle i, y \rangle}^{a'}$ soient premiers entre eux pour tout $i < n$ —, ce qui contredit la minimalité de $b'$. À présent, soit $r = (a, b)_n$ et $b'' = b'p_{\langle n, r \rangle}^{a'}$. Toujours en utilisant le lemme de Gauss, on montre que $(a, b)$ et $(a', b'')$ codent pour la même suite de taille $n+1$.

Montrons à présent le lemme. Soit $(a, b)$ codant pour une suite de taille $n$, et soit $r \in \mathbb{N}$. D'après la proposition 4.4, soit $a'$ tel que tout $i \le \max(a, \langle n, r \rangle)$ divise $a'$. D'après le paragraphe précédent, il existe $b'$ tel que $(a', b')$ code pour la même suite de taille $n$ que $(a, b)$. Soit $b'' = b'p_{\langle n, r \rangle}^{a'}$. Il est clair que $(a', b'')_n = r$. Toujours en utilisant le lemme de Gauss, on montre que $(a', b'')_i = (a', b')_i = (a, b)_i$ pour $i < n$. ■

Passons finalement à la preuve que les fonctions primitives récursives sont prouvablement calculables.
## Théorème 4.6

Les fonctions primitives récursives sont prouvablement calculables dans le système RCA₀.

### PREUVE

On laisse au lecteur le soin de montrer que le théorème est vérifié pour les fonctions de base. Le schéma de composition ne présente pas de difficulté particulière : soit $f(\bar{x}) = g(h_1(\bar{x}), \dots, h_k(\bar{x}))$ pour des fonctions $g, h_1, \dots, h_k$ prouvablement calculables via des formules $G, H_1, \dots, H_k$. Alors, $f$ est prouvablement calculable par la formule

$$F(\bar{x}, r) \equiv \exists y_1, \dots, y_k H_1(\bar{x}, y_1) \wedge \dots \wedge H_k(\bar{x}, y_k) \wedge G(y_1, \dots, y_k, r).$$

Nous passons à présent au schéma de récursion primitive. Soit

$$\begin{align*} f(\bar{x}, 0) &= g(\bar{x}) \\ f(\bar{x}, n+1) &= h(\bar{x}, n, f(\bar{x}, n)), \end{align*}$$

pour des fonctions $g, h$ prouvablement calculables par des formules $G, H$. Nous allons créer une formule $F(\bar{x}, n, r)$ telle que :

$$\text{RCA}_0 \vdash \forall \bar{x}, n \exists! r F(\bar{x}, n, r);$$

$$\text{RCA}_0 \vdash \forall \bar{x}, \exists r F(\bar{x}, 0, r) \wedge G(\bar{x}, r);$$

$$\text{RCA}_0 \vdash \forall \bar{x}, n \exists r_1, r_2 F(\bar{x}, n, r_1) \wedge F(\bar{x}, n+1, r_2) \wedge H(\bar{x}, n, r_1, r_2).$$

La formule en question est donnée par

$$F(\bar{x}, n, r) \equiv \begin{cases} \exists a, b (a, b) \text{ code pour une suite de taille } n+1 \text{ et} \\ r = (a, b)_n \text{ et } G(\bar{x}, (a, b)_0) \text{ et } \forall i < n H(\bar{x}, i, (a, b)_i, (a, b)_{i+1}). \end{cases}$$

Notons que par $\text{B}\Sigma_1^0$, qui est prouvable dans $|\Sigma_1^0|$, la formule ci-dessus est équivalente à une formule $\Sigma_1^0$.

Montrons l'existence par induction sur $n$. Il est clair que l'on a $\exists r F(\bar{x}, 0, r)$. Supposons $\exists r F(\bar{x}, n, r)$ via le couple $(a, b)$ codant pour une suite ayant pour taille $n+1$. Soit $r$ l'unique entier tel que $H(\bar{x}, n, (a, b)_n, r)$.

D'après le lemme 4.5, il existe $(a', b')$ qui code pour une suite ayant pour taille $n+2$, tel que $(a', b')_{n+1} = r$ et tel que $(a', b')_i = (a, b)_i$ pour $i \le n$. Il est alors clair que l'on a $G(\bar{x}, (a', b')_0) \wedge \forall i < n H(\bar{x}, i, (a', b')_i, (a', b')_{i+1})$. De plus, $H(\bar{x}, n, (a', b')_n, (a', b')_{n+1})$. Donc, $F(\bar{x}, n+1, (a', b')_{n+1})$. Par $|\Sigma_1^0|$, l'existence est assurée pour tout $n$.

Montrons à présent l'unicité. Là encore, elle est claire pour $n=0$. Supposons l'unicité pour $n$, et supposons que $F(\bar{x}, n+1, r_1)$ est vérifiée via $(a_1, b_1)$ et que $F(\bar{x}, n+1, r_2)$ est vérifiée via $(a_2, b_2)$. Soient $v_1 = (a_1, b_1)_n$ et $v_2 = (a_2, b_2)_n$. Alors, $F(\bar{x}, n, v_1)$ et $F(\bar{x}, n, v_2)$. Par hypothèse d'induction, on a $v_1 = v_2$. Donc, $H(\bar{x}, n, v_1, (a, b)_{n+1})$ et $H(\bar{x}, n, v_1, (a', b')_{n+1})$. Donc, $(a, b)_{n+1} = (a', b')_{n+1}$, et donc $r_1 = r_2$. ■
# 5. Le schéma de compréhension bornée

Nous voyons à présent un autre schéma d'axiomes sur lequel il convient de s'arrêter, et que l'on pourrait résumer ainsi : « les ensembles finis existent ». Nous allons voir que lorsque l'induction est restreinte, la formulation précise de cet énoncé, ainsi que sa validité, deviennent non triviales.

## 5.1. Codage des ensembles finis

À présent que nous pouvons utiliser les fonctions primitives récursives dans $RCA_0$, il est d'usage de faire appel à la fonction $x \mapsto 2^x$ pour co-der les ensembles finis, en codant l'ensemble $x_0 < x_1 < \dots < x_n$ par l'entier $n = 2^{x_0} + 2^{x_1} + \dots + 2^{x_n}$. Via ce codage, on récupère aisément à partir d'un entier $n$ l'ensemble qu'il code via le lemme suivant.

**Lemme 5.1 (Hájek et Pudlák [81])**

Le système $RCA_0$ prouve que pour tous $n, x \in \mathbb{N}$, il existe un unique tri-plet $(u, v, w)$ avec $u \le y, v < 1$ et $w < 2^x$ tel que :

$$y = 2^{x+1}u + 2^x v + w. \quad \star$$

Le lemme 5.1 se prouve à l'aide de deux applications de la division euclidienne.

**Définition 5.2.** On appelle $x$-ième bit de $y$ l'unique entier $v \in \{0, 1\}$ de la décomposition précédente. On notera $x \in y$ si $v = 1$, et $x \notin y$ sinon. Un entier $y$ est le code canonique de l'ensemble $A$ si pour tout $x \in \mathbb{N}$, $x \in A$ssi le $x \in y$. Un ensemble est codé s'il possède un code canonique. $\diamond$

Notons que la relation « $x \in y$ » est $\Delta_0^0$, car elle s'écrit

$$\exists u \le y \exists w < 2^x (y = 2^{x+1}i + 2^x + w).$$

Le code canonique d'un ensemble, s'il existe, est unique par le lemme 5.1. Il est aisé de montrer dans $RCA_0$ qu'un ensemble $X$ est fini si, et seulement si, il possède un code canonique (voir l'exercice 5.4 à venir). Attention toutefois, par « fini », il faut comprendre fini dans le modèle.

Il est possible d'extraire dans $RCA_0$ toutes les informations standard des codes canoniques, comme leur taille, leur maximum ou leur minimum. On laisse au lecteur le soin de montrer que les fonctions correspondantes sont bien primitives récursives.

## 5.2. Notions d'infini et RCA₀

Qu'est-ce qu'un ensemble infini ? La définition la plus intuitive, et que nous adopterons par défaut, est celle de l'absence de majorant.
**Définition 5.3.** Un ensemble $A$ est *infini* si pour tout $x$ il existe $y > x$ tel que $y \in A$. Un ensemble est *fini* s'il n'est pas infini. ◇

**Dans les modèles non standard.** Attention! La notion de fini et d'infini est toujours relative au modèle. Si $M$ est un modèle non standard, et si $a \in M$ est un entier non standard, l'ensemble $\{x \in M : x < a\}$ est infini de l'extérieur du modèle, mais fini dans le modèle. Attention également, de l'extérieur du modèle, on peut construire des ensembles bornés dans le modèle (et donc finis), mais qui n'y appartiennent pas! C'est le cas par exemple du segment initial constitué des entiers standard.

**Exercice 5.4.** Montrer dans $\mathbf{RCA}_0$ qu'un ensemble est fini si, et seulement si, il est canoniquement codé :

(i) $\mathbf{RCA}_0 \vdash \forall y \exists X (y \text{ est le code canonique de } X)$;

(ii) $\mathbf{RCA}_0 \vdash \forall X \forall b (\forall x (x \in X \rightarrow x < b) \rightarrow X \text{ est canoniquement codé}).$ ◇

**Définitions équivalentes.** On pourrait considérer qu'un ensemble $A \subseteq \mathbb{N}$ est infini s'il est en bijection avec $\mathbb{N}$. On pourrait également considérer qu'un ensemble est infini s'il contient des « blocs » de taille arbitraire, et $\mathbf{RCA}_0$ est suffisamment puissant pour montrer l'équivalence de ces définitions.

**Proposition 5.5.** Le système $\mathbf{RCA}_0$ prouve les équivalences suivantes, pour tout $A$ :

(1) l'ensemble $A$ est infini;

(2) il existe une fonction bijective croissante $f : \mathbb{N} \rightarrow A$;

(3) pour tout $z$, le segment initial de $A$ de cardinalité exactement $z$ possède un code canonique. ★

**PREUVE.** (1) $\rightarrow$ (2). Soit $g(x)$ le plus petit $y > x$ tel que $y \in X$. La fonction est $\Sigma_1^0$, et totale car $A$ est infini, donc est $\Delta_1^0$. La fonction $g$ existe par compréhension $\Delta_1^0$. Soit $a$ le plus petit élément de $A$ (qui existe par la proposition 3.4). Alors, la fonction $f : \mathbb{N} \rightarrow A$ définie par $f(0) = a$ et $f(n+1) = g(f(n))$ existe par récursion primitive, et satisfait (2).

(2) $\rightarrow$ (3). Soit $f : \mathbb{N} \rightarrow A$ une fonction bijective croissante, et soit $z \in \mathbb{N}$. Par compréhension $\Delta_1^0$, l'ensemble $A_z = \{f(x) : x < z\}$ existe, et par l'exercice 5.4, l'ensemble $A_z$ possède un code canonique.

(3) $\rightarrow$ (1). Soit $x \in \mathbb{N}$. Par (3), le code canonique $q$ du segment initial de $A$ de cardinalité $x+1$ existe. L'élément maximal de $q$ est un élément de $A$ plus grand que $x$. Ainsi, $A$ est infini. ■
### 5.3. Schéma de compréhension bornée

Nous avons vu que dans $\mathbf{RCA}_0$ un ensemble est fini si, et seulement si, il a un code canonique. Attention toutefois, il s'agit des ensembles dont on peut montrer l'existence dans le modèle, via le schéma de compréhension ! En revanche, étant donné une formule $F(x)$ arbitraire et une borne $b$, l'ensemble $\{x < b : F(x)\}$ n'existe pas nécessairement si $F$ est trop complexe. L'ensemble existera bien sûr quand $F$ est prouvablement $\Delta_1^0$. Il est en fait possible de montrer, grâce à l'induction $\Sigma_1^0$, que ce sera également le cas si $F$ est $\Sigma_1^0$. Il s'agit en fait d'une condition équivalente : $Q + I\Delta_0^0$ montre que $I\Sigma_1^0$ est équivalent au fait que l'ensemble $\{x < b : F(x)\}$ est canoniquement codé pour toute formule $F \ \Sigma_1^0$. Cette équivalence se propage à tous les niveaux de la hiérarchie.

Souvenons-nous de la notation $y \in n$ de la définition 5.2. On appelle *axiome de compréhension bornée* pour une formule $F(x)$ l'énoncé

$$ \forall t \exists n \forall y (y \in n \leftrightarrow (y < t \land F(y))). \qquad (15) $$

Comme pour le cas du schéma d'induction, la hiérarchie de compréhension bornée s'étend aux prédicats $\Delta_n^0$. Pour des formules $F(x), G(x)$ avec $F(x) \ \Sigma_n^0$ et $G(x) \ \Pi_n^0$, l'axiome de compréhension bornée est l'énoncé

$$ \forall x (F(x) \leftrightarrow G(x)) \rightarrow (\forall t \exists n \forall y (y \in n \leftrightarrow (y < t \land F(y))). \qquad (16) $$

**Notation**

Soit $n > 0$. On note $BC\Sigma_n^0$ (resp. $BC\Pi_n^0$) le schéma de compréhension bornée (15) restreint aux formules $\Sigma_n^0$ (resp. $\Pi_n^0$) et l'on note $BC\Delta_n^0$ le schéma de compréhension bornée (16) restreint aux formules $\Delta_n^0$.

Dans $\mathbf{RCA}_0$, si un ensemble existe, son complémentaire existe également. Ainsi, pour tout $n > 0$, $\mathbf{RCA}_0 \vdash BC\Sigma_n^0 \leftrightarrow BC\Pi_n^0$.

### Théorème 5.6 (Hájek et Pudlák [81])

Soit $n > 0$. Alors, $\mathbf{RCA}_0 \vdash BC\Sigma_n^0 \leftrightarrow I\Sigma_n^0$.

**PREUVE.** Supposons $BC\Sigma_n^0$. Soit $F(x)$ une formule $\Sigma_n^0$ telle que $F(0)$ est vraie et telle que $F(n) \rightarrow F(n+1)$ pour tout $n \in \mathbb{N}$. Soit $a \in \mathbb{N}$. Montrons que $F(a)$ est vraie. Par $BC\Sigma_n^0$, l'ensemble $X = \{x \le a : F(x)\}$ est codé par un entier $z$. Soit $G(n) \equiv (n \le a \land n \in z) \lor n > a$. On a bien $G(0)$ et $G(n) \rightarrow G(n+1)$. Par $I\Delta_0^0$, on a $G(x)$ pour tout $x$ et donc $F(a)$.

Supposons $I\Sigma_n^0$. Soit $F(x)$ une formule $\Sigma_n^0$ et soit $z$ fixé. Soit $G(q)$ la formule $\Pi_n^0 \forall x < z (F(x) \rightarrow x \in q)$. L'entier $2^z - 1$ code pour l'ensemble $\{x \in \mathbb{N} : x < z\}$. En particulier, $G(2^z - 1)$ est vraie. Donc, par $I\Pi_n^0$,
qui est équivalent à $\mathrm{I}\Sigma_n^0$, il y a un plus petit élément $q$ qui vérifie $G$. Sup-
posons $x \in q \wedge \neg F(x)$. Alors, $q - 2^x < q$ vérifie aussi $G$, ce qui contredit la
minimalité de $q$. Donc, $\forall x < z (F(x) \leftrightarrow x \in q)$. ■

**Exercice 5.7.** (★★) Montrer que pour tout $n \in \omega$,

$$
\mathrm{RCA}_0 \vdash \mathrm{I}\Delta_n^0 \leftrightarrow \mathrm{BC}\Delta_n^0.
$$

◇

La figure 5.8 résume les relations entre les différents schémas rencontrés
jusqu’à maintenant.

<figure><img src="image_144.png" /><figcaption>FIGURE 5.8 – Hiérarchies d’induction, de collection et de compréhension bornée. Les flèches indiquent une implication dans RCA₀.</figcaption></figure>

**6. Théorèmes de conservation**

Lorsque l'on étend une théorie *S* en une théorie *T*, il est naturel de se demander dans quelle mesure la nouvelle théorie *T* est plus forte que *S* : quels énoncés indémontrables dans *S* deviennent des théorèmes de *T* ? Nous avons étudié jusqu'ici des énoncés individuels, comme le théorème de Bolzano-Weierstrass, qui est prouvable dans *ACA*₀ mais pas dans *WKL*₀. Dans ce chapitre, nous allons adopter une approche plus systématique, et étudier la prouvabilité relative pour des collections de formules. On s'intéressera aux trois grands types de questions suivantes.

(1) Dans quelle mesure l'arithmétique du second ordre prouve-t-elle de nouveaux énoncés de l'arithmétique du premier ordre ? Pour y apporter une réponse plus complète, nous allons nous employer à déterminer la partie du premier ordre de sous-systèmes de l'arithmétique du second ordre comme RCA₀, WKL₀ ou ACA₀. Autrement dit, nous allons trouver,
pour chacun de ces systèmes T, une théorie du premier ordre S telle que les énoncés du premier ordre prouvables dans T sont exactement ceux prouvables dans S.

(2) Quelle est la puissance relative des systèmes de l'arithmétique du second ordre ? Plus précisément, nous allons montrer que pour certaines classes $\Gamma$ de formules et pour des sous-systèmes $S \subseteq T$ de l'arithmétique du second ordre, si $T$ prouve un énoncé dans $\Gamma$, alors cet énoncé est déjà prouvable dans $S$. Par exemple, nous verrons que tout énoncé arithmétique prouvable dans $WKL_0$ est déjà prouvable dans $RCA_0$.

(3) Dans quelle mesure les mathématiques infinitaires prouvent-elles des énoncés qui ne sont pas prouvables par les mathématiques finitaires ? Cette question, au cœur de la crise des fondements des mathématiques, est à l'origine des mathématiques à rebours. Nous verrons comment ces dernières apportent une réponse partielle au programme de Hilbert.

Nous allons apporter à ces trois questions des réponses de même nature, en prouvant des théorèmes de conservation.

**Définition 6.1.** Soient $T$ et $S$ des théories dénombrables dans les langages $\mathcal{L}_T \supseteq \mathcal{L}_S$ et soit $\Gamma$ un ensemble de formules closes de $\mathcal{L}_S$. La théorie $T$ est une extension conservative de $S$ pour les formules de $\Gamma$ si pour toute formule $F \in \Gamma$, $T \vdash F$ ssi $S \vdash F$. Si $\Gamma$ est l'ensemble des formules de $\mathcal{L}_S$, alors on dit que $T$ est une extension conservative de $S$. ♦

La question (1) demandera de prouver des théorèmes de conservation dans le cas où $S$ est une théorie dans $\mathcal{L}_{PA}$ et $T$ dans $\mathcal{L}_{Z_2}$, tandis que la question (2) fera appel à des théorèmes de conservation où $S$ et $T$ sont toutes les deux des théories dans $\mathcal{L}_{Z_2}$.

Les théories que nous allons étudier sont toutes sujettes au théorème de complétude, qui dit qu'un énoncé $A$ est prouvable dans une théorie $T$ ssi tout modèle de $T$ est un modèle de $A$. Dans ce cas, pour prouver qu'une théorie $T$ est une extension conservative de $S$ pour une collection de formules closes $\Gamma$, il suffit de montrer que pour tout modèle $\mathcal{M}$ de $S$, il existe un modèle $\mathcal{N}$ de $T$, tel que pour toute formule $F \in \Gamma$, si $\mathcal{N} \models F$ alors $\mathcal{M} \models F$. La structure $\mathcal{N}$ est généralement obtenue à partir de $\mathcal{M}$ en lui ajoutant des éléments pour satisfaire $T$, en faisant attention à ne pas prouver de nouvelles formules de $\Gamma$.

Dans ce chapitre, nous allons nous restreindre à des théories dans des langages dénombrables, comme $\mathcal{L}_{PA}$ ou $\mathcal{L}_{Z_2}$. La proposition suivante va nous permettre de restreindre la technique décrite ci-dessus aux structures dénombrables.
**Théorème 6.2 (Löwenheim-Skolem dénombrable)**

Soit $T$ une théorie cohérente dans un langage $\mathcal{L}$ dénombrable. Alors, il existe un modèle dénombrable de $T$.

**PREUVE.** La preuve du théorème 9-2.22 de complétude de Gödel produit un modèle dénombrable dans le cas où le langage $\mathcal{L}$ est dénombrable. ■

La proposition précédente est un cas particulier du théorème plus général dit de Löwenheim-Skolem, et nous y ferons parfois référence de cette manière. La proposition suivante donne une approche très générale pour prouver des résultats de conservation.

**Proposition 6.3.** Soient $S$ et $T \supseteq S$ des théories dans les langages dénombrables $\mathcal{L}_T \supseteq \mathcal{L}_S$, et soit $\Gamma$ un ensemble de formules closes de $\mathcal{L}_S$. Supposons que pour tout modèle dénombrable $\mathcal{M}$ de $S$, il existe un modèle $\mathcal{N}$ de $T$ tel que

(★) pour toute formule $F \in \Gamma$, si $\mathcal{M} \not\models F$, alors $\mathcal{N} \not\models F$.

Alors, $T$ est une extension conservative de $S$ pour les formules de $\Gamma$. ★

**PREUVE.** Soit $F \in \Gamma$ une formule telle que $S \not\models F$. Alors, $S \cup \{\neg F\}$ est une théorie cohérente, donc par le théorème 6.2 de Löwenheim-Skolem, il existe un modèle dénombrable $\mathcal{M}$ de $S \cup \{\neg F\}$. Par hypothèse, il existe un modèle $\mathcal{N}$ de $T$ satisfaisant (★). En particulier, $\mathcal{N} \not\models F$, or $\mathcal{N} \models T$, donc $T \not\models F$ (voir le théorème 9-2.20). ■

## 6.1. Parties du premier ordre

Nous allons concentrer notre attention sur la partie du premier ordre des sous-systèmes de l'arithmétique du second ordre. Commençons par définir formellement ce que l'on entend par *partie du premier ordre* pour une théorie et pour une structure.

**Définition 6.4.** La *partie du premier ordre* d'une théorie $T$ de $\mathcal{L}_{Z_2}$ est l'ensemble des énoncés de $\mathcal{L}_{\text{PA}}$ prouvables dans $T$. La *partie du premier ordre* d'une $\mathcal{L}_{Z_2}$-structure $(M, S^\mathcal{M}, +^\mathcal{M}, \times^\mathcal{M}, <^\mathcal{M}, 0^\mathcal{M}, 1^\mathcal{M})$ est la $\mathcal{L}_{\text{PA}}$-structure

$$ \mathcal{M} \upharpoonright_{\mathcal{L}_{\text{PA}}} = (M, +^\mathcal{M}, \times^\mathcal{M}, <^\mathcal{M}, 0^\mathcal{M}, 1^\mathcal{M}). \diamond $$

Notons que si $\mathcal{M} \models T$ pour une théorie $T$ de l'arithmétique du second ordre, alors $\mathcal{M} \upharpoonright_{\mathcal{L}_{\text{PA}}} \models S$, où $S$ est la partie du premier ordre de $T$. Ca- ractériser la partie du premier ordre d'un système $T$ de l'arithmétique du second ordre consiste en deux étapes : tout d'abord, il faut identifier un ensemble $S$ d'axiomes dans $\mathcal{L}_{\text{PA}}$ tels que $T \vdash S$, puis prouver que $T$ est une extension conservative de $S$. Pour ce faire, nous allons utiliser une version plus spécifique de la proposition 6.3 où $\mathcal{N} \upharpoonright_{\mathcal{L}_{\text{PA}}} = \mathcal{M}$.
**Définition 6.5.** Une $\mathcal{L}_{Z_2}$-structure $\mathcal{N}$ est une $\omega$-extension d'une $\mathcal{L}_{\text{PA}}$-structure $\mathcal{M}$ si $\mathcal{N} \upharpoonright_{\mathcal{L}_{\text{PA}}} \mathcal{M}$. On note alors $\mathcal{M} \subseteq_{\omega} \mathcal{N}$ et l'on dit aussi que $\mathcal{M}$ est une $\omega$-sous-structure de $\mathcal{N}$.
$\diamond$

Attention ! La notion d'ω-extension n'a rien à voir avec celle d'ω-structure de la définition 22-3.4. En particulier, $\mathcal{N}$ peut être une ω-extension de $\mathcal{M}$ sans être une ω-structure.

**Proposition 6.6.** Soient $S$ une $\mathcal{L}_{\text{PA}}$-théorie et $T$ une $\mathcal{L}_{Z_2}$-théorie. Si tout modèle dénombrable de $S$ est une $\omega$-sous-structure d'un modèle de $T$, alors $T$ est une extension conservative de $S$.
$\star$

PREUVE. Soit $\mathcal{M}$ un modèle dénombrable de $S$, et soit $\mathcal{N}$ une $\omega$-extension de $\mathcal{M}$ telle que $\mathcal{N} \models T$. Soit $F$ une formule close de $\mathcal{L}_{\text{PA}}$ telle que $\mathcal{M} \not\models F$. Alors, comme la satisfaction d'une formule du premier ordre sur $\mathcal{N}$ ne fait intervenir que sa partie du premier ordre, on a $\mathcal{N} \not\models F$. Ainsi, par la proposition 6.3, $T$ est une extension conservative de $S$ pour les formules closes de $\mathcal{L}_{\text{PA}}$.
$\blacksquare$

## Premier ordre vs formule arithmétique

Attention à distinguer les formules dans $\mathcal{L}_{\text{PA}}$, et les formules arithmétiques dans $\mathcal{L}_{Z_2}$. En effet, dans le second cas, les variables libres peuvent être des ensembles d'entiers. On distingue donc le principe $|\Sigma_n^0|$ qui est une théorie du second ordre, où les formules peuvent avoir des variables libres d'ensembles, de $|\Sigma_n|$ qui est une théorie du premier ordre.

Notre premier résultat de conservation montre que la partie du premier ordre de $\text{ACA}_0$ est l'arithmétique de Peano. Autrement dit, les seules formules de $\mathcal{L}_{\text{PA}}$ prouvable à l'aide de $\text{ACA}_0$ sont les théorèmes de PA. Nous aurons besoin de la définition suivante.

**Définition 6.7.** Soit $\mathcal{M} = (M, S^\mathcal{M})$ une $\mathcal{L}_{Z_2}$-structure et $\Gamma$ une collection de formules de $\mathcal{L}_{Z_2}$ à paramètres dans $\mathcal{M}$, sans variable libre d'ensemble, et n'ayant que $x$ pour variable libre d'entier. Un ensemble $X \subseteq \mathcal{M}$ est $\Gamma$-définissable dans $\mathcal{M}$ si $X = \{n \in M : \mathcal{M} \models F(n)\}$ pour une formule $F \in \Gamma$. Un ensemble $X$ est $\Delta_n^0$-définissable dans $\mathcal{M}$ s'il est à la fois $\Sigma_n^0$-définissable et $\Pi_n^0$-définissable.
$\diamond$

La définition précédente s'applique également aux structures du premier ordre en considérant leur $\omega$-extension triviale dont la partie du second ordre est vide.

## Théorème 6.8 (Friedman [65])

Le système $\text{ACA}_0$ est une extension conservative de PA.
### PREUVE

Par la proposition 6.6, il suffit de prouver que pour tout modèle dénombrable $\mathcal{M} \models PA$, il existe une $\omega$-extension $\mathcal{N}$ de $\mathcal{M}$ telle que $\mathcal{N} \models \text{ACA}_0$. Soit $\mathcal{M} = (M, +^\mathcal{M}, \times^\mathcal{M}, <^\mathcal{M}, 0^\mathcal{M}, 1^\mathcal{M})$ un modèle dénombrable de PA. Soit $S^\mathcal{N}$ la classe des ensembles $X \subseteq M$ définissables par une formule de $\mathcal{L}_{\text{PA}}$ avec paramètres dans $\mathcal{M}$. Notons que les paramètres ne sont que du premier ordre. Soit $\mathcal{N}$ l'${\omega}$-extension de $\mathcal{M}$ dont la partie du second ordre est $S^\mathcal{N}$. Montrons que $\mathcal{N} \models \text{ACA}_0$. Par l'exercice 22-2.2, il suffit de montrer que $\mathcal{N}$ satisfait l'arithmétique de Robinson (Q) augmentée de l'axiome d'induction sur les ensembles (11) et du schéma de compréhension pour les formules arithmétiques avec paramètres.

Comme $\mathcal{N}$ est une $\omega$-extension de $\mathcal{M}$ et que $\mathcal{M} \models PA$, alors $\mathcal{N} \models PA$, donc $\mathcal{N} \models Q$. Soit $X \in S^\mathcal{N}$, et soit $F$ la formule de $\mathcal{L}_{\text{PA}}$ définissant $X$ dans $\mathcal{M}$. Comme $\mathcal{N} \models PA$, alors le schéma d'induction est satisfait pour $F$, donc l'axiome d'induction est satisfait pour $X$.

Montrons que $\mathcal{N}$ satisfait le schéma de compréhension pour les formules arithmétiques avec paramètres dans $\mathcal{N}$. Soit $G(x)$ une formule arithmétique de $\mathcal{L}_{Z_2}$ avec paramètres dans $\mathcal{N}$. Soient $X_0, \dots, X_{k-1}$ les paramètres du second ordre de $G$, et soient $F_0, \dots, F_{k-1}$ les formules de $\mathcal{L}_{\text{PA}}$ les définissant. Soit $H(x)$ la formule de $\mathcal{L}_{Z_2}$ où l'on a remplacé toutes les occurrences de $y \in X_s$ par $F_s(y)$, de telle sorte que $H$ n'ait plus que des paramètres du premier ordre. En particulier, $H$ est une formule de $\mathcal{L}_{\text{PA}}$ avec paramètres dans $\mathcal{M}$, donc $Y = \{n \in M : \mathcal{M} \models H(n)\} \in S^\mathcal{N}$, or $Y = \{n \in M : \mathcal{N} \models G(n)\}$, donc $\mathcal{N} \models \exists X \forall n (n \in X \leftrightarrow G(n))$. ■

Le second résultat de conservation concerne la partie du premier ordre de $\text{RCA}_0$. On note $\Sigma_1$-PA la théorie du premier ordre composée de l'arithmétique de Robinson Q augmentée du schéma d'induction $\Sigma_1$ pour les formules de $\mathcal{L}_{\text{PA}}$ avec paramètres du premier ordre ($|\Sigma_1$)). Nous aurons besoin du lemme suivant, laissé en exercice.

**Exercice 6.9.** Soit $\mathcal{M} = (M, S^\mathcal{M})$ une structure telle que $\mathcal{M} \models \text{B}\Sigma_1^0$, et soit $X \subseteq M$ un ensemble $\Delta_1^0$-définissable avec paramètres dans $\mathcal{M}$. Pour toute formule $\Sigma_1^0 F$ à paramètres dans $\mathcal{M} \cup \{X\}$, il existe une formule $\Sigma_1^0 G$ à paramètres dans $\mathcal{M}$, ayant les mêmes variables libres que $F$, et telle que $\mathcal{M} \cup \{X\} \models \forall x(F(x) \leftrightarrow G(x))$. ◇

Nous sommes maintenant prêts à prouver notre résultat de conservation.

### Théorème 6.10 (Friedman [65])

Le système $\text{RCA}_0$ est une extension conservative de $\Sigma_1$-PA.
## PREUVE

Par la proposition 6.6, il suffit de prouver que pour tout modèle dénombrable $\mathcal{M} \models \Sigma_1$-PA, il existe une $\omega$-extension $\mathcal{N}$ de $\mathcal{M}$ telle que $\mathcal{N} \models \text{RCA}_0$. Soit $\mathcal{M} = (M, +^\mathcal{M}, \times^\mathcal{M}, <^\mathcal{M}, 0^\mathcal{M}, 1^\mathcal{M})$ un modèle dénombrable de $\Sigma_1$-PA. Soit $S^\mathcal{N}$ la classe des ensembles $X \subseteq M$ définissables par une formule $\Delta_1$ de $\mathcal{L}_{\text{PA}}$ avec paramètres dans $\mathcal{M}$. Notons que les paramètres ne sont que du premier ordre. Soit $\mathcal{N}$ l'${\omega}$-extension de $\mathcal{M}$ dont la partie du second ordre est $S^\mathcal{N}$.

En itérant l'exercice 6.9, ci-dessus, pour retirer à chaque itération un paramètre du second ordre, on peut montrer que si $F(x)$ est une formule $\Sigma_1^0$ à paramètres dans $\mathcal{N}$ et sans variable libre d'ensemble, il existe une formule $\Sigma_1 G(x)$ à paramètres dans $\mathcal{M}$, avec les mêmes variables libres, et telle que $\mathcal{N} \models \forall x (F(x) \leftrightarrow G(x))$. En effet, si $F(x)$ a comme paramètres du second ordre $X_1, \dots, X_k$, on peut construire successivement des formules $\Sigma_1^0 F_1(x), \dots, F_{k-1}(x)$ telles que $F_i(x)$ a comme paramètres du second ordre $X_1, \dots, X_{k-i-1}$, et telles que $\mathcal{N} \models \forall x (F(x) \leftrightarrow F_i(x))$. La dernière formule $F_{k-1}(x)$ est la formule $G(x)$ désirée.

Montrons que $\mathcal{N} \models \text{RCA}_0$. Comme $\mathcal{N}$ est une $\omega$-extension de la structure $\mathcal{M}$ et $\mathcal{M} \models \Sigma_1$-PA, alors $\mathcal{N} \models \Sigma_1$-PA, donc $\mathcal{N} \models \text{Q}$. Montrons que $\mathcal{N} \models |\Sigma_1^0|$. Soit $F(x)$ une formule $\Sigma_1^0$ close avec paramètres dans $\mathcal{N}$. Soit $G(x)$ une formule $\Sigma_1$ avec paramètres dans $\mathcal{M}$ telle que $\mathcal{N} \models \forall x (F(x) \leftrightarrow G(x))$. Comme $\mathcal{M} \models |\Sigma_1|$, alors le schéma d'induction s'applique dans $\mathcal{M}$ pour $G$, donc s'applique dans $\mathcal{N}$ pour $G$, donc dans $\mathcal{N}$ pour $F$. Ainsi, $\mathcal{N} \models |\Sigma_1^0|$. Montrons que $\mathcal{N}$ satisfait le schéma de compréhension pour les formules $\Delta_1^0$ closes avec paramètres dans $\mathcal{N}$ et comme unique variable libre $x$. Soit $F_\exists(x)$ une formule $\Sigma_1^0$ à paramètres dans $\mathcal{N}$ et soit $F_\forall$ une formule $\Pi_1^0$ à paramètres dans $\mathcal{N}$, telles que $\mathcal{N} \models \forall x (F_\exists(x) \leftrightarrow F_\forall(x))$. Soient $G_\exists$ et $G_\forall$ les formules $\Sigma_1$ et $\Pi_1$ à paramètres dans $\mathcal{M}$ correspondantes en utilisant l'exercice précédent. Alors, $\mathcal{M} \models \forall x (G_\exists(x) \leftrightarrow G_\forall(x))$, donc l'ensemble $X = \{n \in M : G_\exists(x)\}$ est définissable par une formule $\Delta_1$ avec paramètres dans $\mathcal{M}$, donc $X \in S^\mathcal{N}$. Ainsi, $\mathcal{N} \models \exists X \forall z (z \in X \leftrightarrow F_\exists(z))$, donc $\mathcal{N}$ satisfait le schéma de compréhension pour les formules $\Delta_1^0$ closes avec paramètres dans $\mathcal{N}$. Ainsi, $\mathcal{N} \models \text{RCA}_0$. ■

## 6.2. Conservation $\Pi_1^1$

Nous avons étudié jusqu'ici la partie de premier ordre des théories $\mathcal{ACA}_0$ et $\text{RCA}_0$, en montrant qu'elles étaient des extensions conservatives, respectivement de PA et $\Sigma_1$-PA. Notons qu'il s'agit d'extensions de théories du premier ordre en théories du second ordre.

Nous allons dans cette section changer de stratégie. Supposons que l'on dispose de théories $S \subseteq T$ toutes deux dans le langage de l'arithmétique
du second ordre. Supposons aussi que la partie du premier ordre de $S$ soit connue. Afin de connaître la partie du premier ordre de $T$, il suffit de montrer que cette dernière est une extension conservative de $S$ pour les formules arithmétiques. Elle aura ainsi la même partie du premier ordre que $S$. La technique que nous exposerons fera en fait le travail directement pour toutes les formules $\Pi_1^1$, c'est-à-dire les formules de la forme $\forall XF(X)$ où $F$ est une formule arithmétique et $X$ une variable du second ordre (nous étudierons les formules et classes $\Pi_1^1$ en détail dans le chapitre 29).

Nous allons prouver en particulier que $WKL_0$ est une extension conservative de $RCA_0$ pour les formules $\Pi_1^1$, et donc que la partie du premier ordre de $WKL_0$ est $\Sigma_1$-PA. Commençons par étendre la notion d'ω-extension aux structures du second ordre.

**Définition 6.11.** Soient $\mathcal{M} = (M, S^\mathcal{M})$ et $\mathcal{N} = (N, S^\mathcal{N})$ deux structures de $\mathcal{L}_{Z_2}$. On dit que $\mathcal{N}$ est une $\omega$-extension de $\mathcal{M}$ si $\mathcal{M} \upharpoonright_{\mathcal{L}_{PA}} = \mathcal{N} \upharpoonright_{\mathcal{L}_{PA}}$ et $S^\mathcal{M} \subseteq S^\mathcal{N}$. On dira alors aussi que $\mathcal{M}$ est une $\omega$-sous-structure de $\mathcal{N}$. ♦

Nous voyons à présent comment utiliser la notion d'ω-extension pour prouver que deux théories montrent les mêmes formules $\Pi_1^1$, et donc les mêmes formules arithmétiques.

**Proposition 6.12.** Soient $S$ et $T \supseteq S$ des $\mathcal{L}_{Z_2}$-théories telles que tout modèle dénombrable $\mathcal{M}$ de $S$ est une $\omega$-sous-structure d'un modèle dénombrable $\mathcal{N}$ de $T$. Alors, $T$ est une extension conservative de $S$ pour les formules closes $\Pi_1^1$. ★

**PREUVE.** Soit $\mathcal{M}$ un modèle dénombrable de $S$, et soit $\mathcal{N}$ une $\omega$-extension de $\mathcal{M}$ telle que $\mathcal{N} \models T$. Soient $S^\mathcal{M}$ et $S^\mathcal{N}$ les parties du second ordre de respectivement $\mathcal{M}$ et $\mathcal{N}$. Soit $F$ une formule close $\Pi_1^1$ de la forme $\forall XG(X)$, où $G(X)$ est une formule arithmétique telle que $\mathcal{M} \not\models F$.

Alors, $\mathcal{M} \models \exists X \neg G(X)$, donc il existe un $X \in S^\mathcal{M}$ tel que $\mathcal{M} \models G(X)$. Comme $S^\mathcal{M} \subseteq S^\mathcal{N}$, alors $X \in S^\mathcal{N}$, et comme $\mathcal{M} \upharpoonright_{\mathcal{L}_{PA}} = \mathcal{N} \upharpoonright_{\mathcal{L}_{PA}}$, alors $\mathcal{N} \models G(X)$, donc $\mathcal{N} \models \exists X \neg G(X)$, et $\mathcal{N} \models \neg F$. Ainsi, par la proposition 6.3, $T$ est une extension conservative de $S$ pour les formules closes $\Pi_1^1$. ■

Comme exprimé dans la section 22-8.1, un certain nombre d'énoncés s'expriment sous la forme $\forall X (F(X) \rightarrow \exists Y H(X, Y))$, où $F$ et $H$ sont des formules arithmétiques éventuellement avec des variables libres. Par exemple, pour le lemme faible de König, $F(X)$ est le prédicat « X code pour un arbre binaire infini » et $H(X, Y)$ signifie « Y est un chemin de l'arbre codé par $X$ ». Nous allons développer des techniques générales pour créer des modèles d'énoncés de la forme ci-dessus, tout en garantissant la conservation de formules $\Pi_1^1$.
**Définition 6.13.** Soit $\mathcal{M} = (M, S^\mathcal{M})$ une structure de l'arithmétique du second ordre, et soit $G \subseteq M$. On note $\mathcal{M} \cup \{G\}$ l'ω-extension de $\mathcal{M}$ dont la partie du second ordre est $S^\mathcal{M} \cup \{G\}$, et $\mathcal{M}[G]$ l'ω extension de $\mathcal{M}$ dont la partie du second ordre est la collection des ensembles qui sont définissables par un prédicat $\Delta_1^0$ à paramètres dans $\mathcal{M} \cup \{G\}$. $\diamond$

Reprenons l'exemple d'énoncé de la forme $\forall X (F(X) \rightarrow \exists Y H(X, Y))$. Intuitivement, en partant d'une structure $\mathcal{M} \models \text{RCA}_0$ et d'un ensemble $X \in \mathcal{M}$ tel que $F(X)$, nous voulons créer une ω-extension $\mathcal{M}_1$ contenant un ensemble $G \subseteq M$ tel que $\mathcal{M}_1 \models H(X, G)$, de telle sorte que l'énoncé $F(X) \rightarrow \exists Y H(X, Y)$ soit vrai dans $\mathcal{M}_1$. En itérant le processus, nous allons obtenir une suite d'ω-extensions $\mathcal{M} \subseteq \mathcal{M}_1 \subseteq \mathcal{M}_2 \subseteq \dots$ telle que $\bigcup_n \mathcal{M}_n$ est un modèle de $\text{RCA}_0$ et de $\forall X (F(X) \rightarrow \exists Y H(X, Y))$.

Pour satisfaire une étape, nous allons donc construire un ensemble $G \subseteq M$ tel que $\mathcal{M} \cup \{G\} \models H(X, G)$ et l'ajouter à $\mathcal{M}$. La structure $\mathcal{M} \cup \{G\}$ obtenue ne satisfait pas le schéma de compréhension $\Delta_1^0$ en général. Nous devons donc clore la structure $\mathcal{M} \cup \{G\}$ par ce schéma, ce qui donne $\mathcal{M}[G]$. Tout le « travail » va consister à s'assurer que le modèle $\mathcal{M}[G]$ ainsi obtenu ne va pas saboter $\text{RCA}_0$, et en particulier l'induction $\Sigma_1^0$. Il est donc nécessaire de s'assurer que $\mathcal{M}[G] \models \text{IA}\Sigma_1^0$. La proposition suivante montre qu'il suffit de prouver que $\mathcal{M} \cup \{G\} \models \text{IA}\Sigma_1^0$ pour obtenir $\mathcal{M}[G] \models \text{IA}\Sigma_1^0$, et donc $\mathcal{M}[G] \models \text{RCA}_0$.

**Proposition 6.14.** Soit $T \equiv \forall X (F(X) \rightarrow \exists Y H(X, Y))$, où $F$ et $H$ sont des formules arithmétiques. Supposons que pour tout modèle dénombrable $\mathcal{M}$ de $\text{RCA}_0$, et tout ensemble $X \in \mathcal{M}$ tel que $\mathcal{M} \models F(X)$, il existe un ensemble $G \subseteq M$ tel que $\mathcal{M} \cup \{G\} \models \text{IA}\Sigma_1^0$ et $\mathcal{M} \cup \{G\} \models H(X, G)$. Alors, $\text{RCA}_0 + T$ est une extension conservative de $\text{RCA}_0$ pour les formules $\Pi_1^1$. $\star$

**PRÉUVE.** Soit $\mathcal{M}$ un modèle dénombrable de $\text{RCA}_0$. Nous allons définir une suite $\mathcal{M} = \mathcal{M}_0 \subseteq \mathcal{M}_1 \subseteq \mathcal{M}_2 \subseteq \dots$ d'ω-extensions dénombrables de telle sorte que, pour tout $n \in \mathbb{N}$,

(1) $\mathcal{M}_n \models \text{RCA}_0$;

(2) pour tout $X \in \mathcal{M}_n$ tel que $\mathcal{M}_n \models F(X)$, il existe $m \in \mathbb{N}$ et $Y \in \mathcal{M}_m$ tel que $\mathcal{M}_m \models H(X, Y)$.

Montrons que si c'est le cas, alors $\text{RCA}_0 + T$ est une extension conservative de $\text{RCA}_0$ pour les formules $\Pi_1^1$. Soit $\mathcal{N} = \bigcup_n \mathcal{M}_n$. Par (1), $\mathcal{N} \models \text{RCA}_0$, et par (2), comme $F$ et $H$ sont des formules arithmétiques et que $\mathcal{N}$ est une ω-extension de $\mathcal{M}_n$ pour tout $n \in \mathbb{N}$, $\mathcal{N} \models \forall X (F(X) \rightarrow \exists Y H(X, Y))$. Par la proposition 6.12, $\text{RCA}_0 + T$ est une extension conservative de $\text{RCA}_0$ pour les formules $\Pi_1^1$.
Supposons que l'on a construit $\mathcal{M}_n$, et soit $X \in \mathcal{M}_n$ un ensemble tel que $\mathcal{M}_n \models F(X)$. Soit $G \subseteq M$ tel que

$$ \mathcal{M}_n \cup \{G\} \models |\Sigma_1^0| \text{ et } \mathcal{M}_n \cup \{G\} \models H(X, G). $$

Montrons que $\mathcal{M}_{n+1} = \mathcal{M}_n[G]$ satisfait (1) et (2) ci-dessus. Par construction, $\mathcal{M}_n[G] \models H(X, G)$ et $\mathcal{M}_n[G]$ satisfait le schéma de compréhension $\Delta_1^0$. Montrons que $\mathcal{M}_n[G] \models |\Sigma_1^0|$. Soit $P(x)$ une formule $\Sigma_1^0$ à paramètres dans $\mathcal{M}_n[G]$ sans autre variable libre que $x$. En itérant l'exercice 6.9 comme dans la preuve du théorème 6.10, il existe une formule $\Sigma_1^0 Q(x)$ à paramètres dans $\mathcal{M}_n \cup \{G\}$ telle que $\mathcal{M}_n[G] \models \forall x (P(x) \leftrightarrow Q(x))$. Comme

$$ \mathcal{M}_n \cup \{G\} \models |\Sigma_1^0|, $$

alors le schéma d'induction est satisfait pour $Q$, donc également pour $P$. Ainsi, $\mathcal{M}_n[G] \models |\Sigma_1^0|$. Donc, $\mathcal{M}_n[G] \models \text{RCA}_0$. Cela termine la construction. Notons qu'il faut faire attention au choix de $X$ pour que (2) soit satisfait. Plus précisément, si l'on fixe une énumération $\mathcal{M}_n = \{X_0^n, X_1^n, \dots\}$ de tous les ensembles de $\mathcal{M}_n$, à l'étape $n$, on choisit $X_m^n$ pour le plus petit $\langle n, m \rangle$ qui n'a pas encore été satisfait. ■

Nous avons à présent les éléments nécessaires pour montrer le théorème annoncé : $\text{WKL}_0$ est une extension conservative de $\text{RCA}_0$ pour les formules $\Pi_1^1$. On peut en particulier en déduire que la partie du premier ordre de $\text{WKL}_0$ est la même que celle de $\text{RCA}_0 : \Sigma_1^-$ PA.

**Théorème 6.15 (Harrington (voir Simpson [203]))**

Le système $\text{WKL}_0$ est une extension conservative de $\text{RCA}_0$ pour les formules $\Pi_1^1$.

Avant de prouver le théorème 6.15, nous avons besoin d'un lemme technique (donné en exercice) sur les formules $\Sigma_1^0$. Par le théorème 9-3.4, un ensemble $A \subseteq \mathbb{N}$ est $X$-c. e. s'il est définissable par une formule $\Sigma_1^0(X)$ de $\mathcal{L}_{Z_2}$. En particulier, pour toute formule $\Sigma_1^0 F(X, x)$, il existe une fonctionnelle Turing $\Phi_e$ tel que $\{n : F(X, n)\} = \{n : \Phi_e^X(n) \downarrow\}$. Il s'ensuit par la propriété de l'usage que $\{n : F(X, n)\} = \{n : \exists k \Phi_e^{X|k}(n)[k] \downarrow\}$. Autrement dit, si l'on définit la formule $\Delta_0^0 H(\sigma, x) \equiv \Phi_e^\sigma(x)[|\sigma|]$, on a

$$ \{n : F(X, n)\} = \{n : \exists k H(G \upharpoonright_k n)\}. $$

L'exercice suivant montre que cette équivalence peut se formaliser dans $\mathbb{B}\Sigma_1^0$.

**Exercice 6.16. (*) (Simpson [203]).** Soit $\mathcal{M} = (M, S^\mathcal{M})$ une $\mathcal{L}_{Z_2}$-structure telle que $\mathcal{M} \models \mathbb{B}\Sigma_1^0$. Soit $F(X)$ une formule $\Sigma_1^0$ à paramètres dans $\mathcal{M}$, et sans autre variable libre d'ensemble que $X$. Alors, il existe une formule $\Delta_0^0 H(\sigma)$ avec les mêmes paramètres que $F$, sans variable