Théorèmes de Gödel

Un exemple d’incomplétude en arithmétique : le théorème de Paris-Harrington

Frédéric Deglise et Marc Boutin

Sujet proposé par M. Giuseppe Longo

Le but de cet exposé est de donner une idée de la portée mathématique des théorèmes d’incomplétude, initiés par les deux théorèmes de Gödel. On présentera en particulier un énoncé qui n’est pas purement métathéorique, le théorème de Paris-Harrington qui affirme qu’une proposition de combinatoire, vraie mathématiquement, n’est pourtant pas démontrable avec les seuls axiomes de Peano.

1 Théorèmes de Gödel

Les deux théorèmes de Gödel affirment un résultat théorique fort sur l’ensemble des théories logiques cohérentes que nous pouvons formuler. Le premier théorème prouve que pour toute théorie consistante suffisament puissante, il existe une phrase logique qui n’est ni vraie ni fausse dans cette théorie, et même qui n’est pas démontrable à partir des axiomes de la théorie. Le second précise que l’on peut formuler la cohérence de notre théorie à partir de son langage mais que cette formule n’est pas démontrable.

La preuve de ce théorème est basée sur l’idée, nouvelle à l’époque de Gödel, que l’on peut traduire des énoncés métathéoriques en formules d’une théorie donnée satisfaisant certaines conditions.

Plus précisément, on peut coder les formules d’un langage dénombrable par des entiers — c’est à dire associer à chaque formule un unique entier (ainsi qu’un algorithme pour passer de l’un à l’autre) — et on peut ensuite transposer les procédés récursifs disponibles sur les entiers (ie dans la métathéorie) en formule vraie dans la théorie, ce qui constitue le lemme de représentation.

1.1 Hypothèses du théorème de Gödel

Ainsi, soit 𝔏 un langage constitué par un nombre dénombrable de symboles :

x_{1}, x_{2}, ... variables f_{1}, f_{2}, ... fonctions d’arité n_{f_{1}}, n_{f_{2}}, ...

R_{1}, R_{2}, ... relations d’arité n_{R_{1}}, n_{R_{2}}, ... ¬, →, ∧, ∃, ∀ symboles usuels

Soit T une théorie écrite sur 𝔏, que l’on suppose consistante, c’est-à-dire qu’on ne peut y trouver de contradiction.

L’hypothèse suffisante pour le lemme de représentation — outre le fait que l’on puisse énumérer les symboles du langage — est que T soit une extension de l’arithmétique, formulée par les axiomes de Peano, ce que l’on peut formaliser comme suit :

1. Il existe des relations fonctionnelles (définissable par une formule écrite dans 𝔏) et vraie dans T qui définissent les fonctions successeur, addition et multiplication de l’arithmétique, ainsi qu’un terme clos correspondant a 0

2. Il existe une méthode de plongement des entiers dans les termes de T , que l’on formalisera par une relation de T , notee I

3. T vérifie les axiomes de Peano restreint aux termes qui correspondent effectivement aux entiers naturels. On les ecrit :

∀x (I(x) → Sx ≠ \overline{0}) ∀x, y (I(x) ∧ I(y) ∧ Sx = Sy → x = y) ∀x (I(x) ∧ x ≠ \overline{0} → ∃y(I(y) ∧ x = Sy)) ∀x (I(x) → (x + \overline{0} = x)) ∀x, y (I(x) ∧ I(y) → x + Sy = S(x + y)) ∀x (I(x) → x.\overline{0} = \overline{0}) ∀x, y (I(x) ∧ I(y) → x.Sy = x.y + x) ∀x_{1}, ..., x_{n}(𝔓(\overline{0}, x_{1}, ..., x_{n}) ∧∀x(I(x) ∧ 𝔓(x, x_{1}, ..., x_{n}) → 𝔓(Sx, x_{1}, ...x_{n})) → ∀x(I(x) → 𝔓(x, x_{1}, ..., x_{n}))

On appellera alors (AP)_{T} ces axiomes de Péano.

remarque : pour prouver entièrement le premier théorème de Gödel, il nous faudra ajouter une hypothèse d’ω-consistance sur T .

1.2 Codage des termes et des formules de T

On peut alors coder les symboles de 𝔏 puis, par induction, les formules de 𝔏, l’important étant que les fonctions définies soient récursives primitives, c’est à dire définies par récurrence ou composition à partir des fonctions successeur ou projections pour les fonctions de plusieurs variables.

Soit (p_{i})_{i∈ℕ} suite des nombres premiers; on utilise les fonctions suivantes, récursives primitives :

α_{n}: ℕ^{n} ⟶ ℕ val_{n} : ℕ ⟶ ℕ (i_{1}, ..., i_{n}) ⟶ ∏ p_{k}^{i_{k}} i ⟶ Valuation de i en p_{n}

Il suffit alors d’associer à chaque symbole de 𝔏 un code élémentaire, comportant par exemple son type et son arité, puis de définir inductivement le codage des termes et des formules. On posera par exemple :

1. si R_{i} est le i^{ime} symbole de relation de 𝔏, d’arité n_{R_{i}}, ⌜R_{i}⌝ = α_{2}(3, n, n_{R_{i}}). (3 représente ici le code pour une relation)

2. si t = R_{i}(t_{1}, ..., t_{m}) est un terme de 𝔏, ⌜t⌝ = α_{m+2}(0, ⌜R_{i}⌝, ⌜t_{1}⌝, ..., ⌜t_{m}⌝).

On vérifie alors que la fonction caractéristique des codes dans les entiers est récursive primitive. Si l’on a garantit l’injectivité du codage, on voit qu’il est désormais possible d’identifier le code d’une formule parmis les entiers et de reconstituer cette formule.

1.3 Procédé diagonal : démontrabilité et substitution

Pour prouver le premier théorème, on utilise un procédé diagonal qui nous permet de construire parmi les codes un entier représentant une formule non démontrable. L’étape suivante consiste donc à définir une relation récursive primitive vraie uniquement sur les codes de formules démontrables.

Définition 1.3.1 Une formule F est démontrable dans T si et seulement si il existe une suite finie de formules aboutissant à F qui soient des axiomes logiques, des axiomes de T ou déduites de deux formules précédentes par la règle du modus ponens (si on a A, A → B, on a B).

Puisque l’on peut représenter une suite finie et sa longeur grâce aux fonctions α_{n} et val_{n}, qui sont récursives, il ne nous reste plus qu’à supposer que l’ensemble des axiomes de T , sous la forme de codes, est récursif primitif. On obtient ainsi dem_{T}, relation recursive primitive sur les codes telle que : dem_{T} (x, ⌜F ⌝) vraie équivaut à x est le code d’une suite finie de formules qui démontre F. On définit alors dem_{T} (x) ≡ ∃y(dem_{T} (y, x)).

Techniquement, la réalisation du procédé diagonal nécessite la définition d’une autre fonction sur les codes qui correspond a la substitution classique dans les formules, et qui permet de substituer à une variable libre une autre formule. Elle se présente sous la forme subs(v,i,j) où v est le code d’une variable, i et j le code de deux formules, j etant substitué a chaque occurence libre de v dans i. La substitution étant définie par induction sur les formules, cette fonction est encore récursive primitive. Pour les besoins du lemme de diagonalisation, on définie la fonction sub, plus simple, à partir de subs de deux variables comme suit : sub(⌜F ⌝,y)=subs(⌜x_{i}⌝,⌜F ⌝,y) si i est le plus petit indice tel que x_{i} est variable libre dans F, ⌜F ⌝ si F n’a pas de variable libre.

1.4 Représentation des fonctions

Définition 1.4.1 Soit R une relation n-aire sur ℕ. R est représentable sur T si et seulement si on a F [x_{1}, ..., x_{n}] formule de 𝔏 tel que : si m_{1}, ..., m_{n} sont des entiers, R(m_{1}, ..., m_{n}) est vraie ⇔ T ⊢ F [\overline{m_{1}}/x_{1}, ..., \overline{m_{n}}/x_{n}] (où \overline{k} est le terme de 𝔏 correspondant dans T à l’entier k).

On obtient alors le lemme de représentation attendu :

Lemme 1.4.1 Toute relation récursive primitive est représentable sur (AP)_{T}.

Preuve On démontre que toute fonction récursive primitive est représentable sur (AP)_{T}. (ie la relation f(m_{1}, ..., m_{n}) = 0 est représentable). Pour celà, la difficulté essentielle réside dans la possibilité de représenter toute suite finie de longeur inconnue a priori par un nombre fixé d’entiers.

Lemme 1.4.2 (fonction β de Gödel) Il existe une fonction β tel que pour tout entier n, pour toute suite finie (x_{1}, ..., x_{n}), il existe a,b entiers tels que β(a, b, i) = x_{i} pour tout i de 1 à n.

Preuve On rappelle le théorème Chinois dans ℕ: soit a_{1}, ..., a_{n} des entiers premiers entre eux deux à deux, si b_{1}, ..., b_{n} sont des entiers, alors il existe b entier tel que pour tout indice i, b ≡ b_{i}mod(a_{i}). Soit donc donnée une suite b_{1}, ..., b_{n}, on choisit a = max(n, b_{1}, .., b_{n})! : alors les (ai + 1)_{i=1,..,n} sont premiers entre eux (et plus grand que tous les b_{1}, ..., b_{n}) : on obtient alors b, d’après le théorème chinois, tel que pour tout i, b ≡ b_{i}mod(ai+1). La fonction β(a, b, i) est donc le reste de b dans sa division euclidienne par ai+1. □

On vérifie que cette fonction β est elle-même représentable, en désignant encore par β la formule qui la représente. Alors, soit par exemple f définie par récurrence comme suit :

\{ \begin{matrix}f(0) = f_{0} \\ f(n + 1) = g(n, f(n)) \end{matrix}

sachant que f_{0} est un entier et g(m_{1}, m_{2})−m_{3}) est représentable par G[x_{1}, x_{2}, x_{3}]. Alors f est représentée par

F [x_{1}] ≡ ∃a, b( β(a, b, \overline{0}, \overline{f_{0}})
∧ ( ∀i < x_{1} G[i, β(a, b, i), β(a, b, i + 1)] )
∧ β(a, b, x_{1}, \overline{0})

On obtient ainsi Dem_{T} formule qui représente dem_{T} et Sub qui représente sub. On peut définir le fait d’être un théorème de T en posant T he_{T} (y) ≡ ∃x(Dem_{T} (x, y)).

1.5 Enoncé et démonstration centrale

Nous résumons les propriétés essentielles aux théorèmes de Gödel des fonctions définies plus haut dans les propriétés de dérivation : D1 T ⊢ F implique (AP)_{T} ⊢ T he_{T} (⌜F ⌝)

D1’ (AP)_{T} ⊢ T he_{T} (⌜F ⌝) implique T ⊢ F D2 (AP)_{T} ⊢ T he_{T} (⌜F ⌝) → T he_{T} (T he_{T} (⌜F ⌝)) D3 (AP)_{T} ⊢ T he_{T} (⌜F ⌝) ∧ T he_{T} (⌜F → G⌝) → T he_{T} (⌜G⌝)

remarque : D1’ nécessite l’hypothèse supplémentaire sur T d’ω-consistance; en effet, le fait d’existence d’un certain x tel que Dem_{T} (x, ⌜F ⌝) ne dit pas forcément que F est un théorème de T , car x peut sortir du cadre des entiers standards.

Théorème 1.5.1 (de Gödel)

1. Il existe une formule F telle que T ⊬ F et T ⊬ ¬F

2. Soit Con_{T} ≡ ¬T he_{T} (⌜\overline{0} = \overline{1}⌝), qui affirme la consistance de T . Alors T ⊢ F ↔ Con_{T}, donc T ⊬ Con_{T}

Preuve

1. Lemme 1.5.1 (de diagonalisation) Soit G[x] une formule Il existe une formule F telle que

(AP)_{T} ⊢ F ↔ G[⌜F ⌝]

Preuve On pose θ[y] ≡ G[Sub(y, y)/_{x}], m = ⌜θ(y)⌝, F = θ[m/_{y}]. Alors (AP)_{T} ⊢ F ↔ G[⌜F ⌝] En effet, dans (AP)_{T} , F ↔ θ[m/_{y}] ↔ G[Sub(m, m)/_{x}] ↔ G[⌜θ[m/_{y}]⌝/_{x}] ↔ G[⌜F ⌝] □

On peut alors expliciter F, obtenue en diagonalisant G[x] ≡ ¬T he_{T} (x). alors (AP)_{T} ⊢ F ↔ ¬T he_{T} (⌜F ⌝) d’après le lemme.

(i) T ⊬ F sinon d’après D1, (AP)_{T} ⊢ T he_{T} (⌜F ⌝), (AP)_{T} ⊢ ¬F absurde

(ii) T ⊬ ¬F sinon d’après D1’, (AP)_{T} ⊢ ¬T he_{T} (⌜F ⌝)], (AP)_{T} ⊢ F absurde □

2. on pose : ⊥≡ \overline{0} = \overline{1}

(i) → T ⊢⊥→ F, d’après D1, (AP)_{T} ⊢ T he_{T} (⌜⊥→ F ⌝). D’après D3, (AP)_{T} ⊢ T he_{T} (⌜⊥⌝) → T he_{T} (⌜F ⌝), par contraposition, (AP)_{T} ⊢ F → Con_{T}

(ii) ← D’après D2, (AP)_{T} ⊢ T he_{T} (⌜F ⌝) → T he_{T} (⌜T he_{T} (⌜F ⌝)⌝), Or (AP)_{T} ⊢ F ↔ ¬T he_{T} (⌜F ⌝) donc d’après D1 et D3, (AP)_{T} ⊢ T he_{T} (⌜F ⌝) → T he_{T} (⌜¬T he_{T} (⌜F ⌝)⌝) d’où, (AP)_{T} ⊢ T he_{T} (⌜F ⌝) → T he_{T} (⌜¬F ⌝) Appliquant de nouveau D3, on en déduit (AP)_{T} ⊢ T he_{T} (⌜F ⌝) → T he_{T} (⌜F ∧ ¬F ⌝)

(AP)_{T} ⊢ T he_{T} (⌜F ⌝) → T he_{T} (⌜⊥⌝)
Par contraposée, (AP)_{T} ⊢ ¬T he_{T} (⌜⊥⌝) → ¬T he_{T} (⌜F ⌝)
ie (AP)_{T} ⊢ Con_{T} → F □

2 Le théorème de Paris Harrington

2.1 Présentation du théorème de Paris-Harrington

Le théorème de Paris-Harrington affirme l’indémontrabilité d’un théorème combinatoire de l’arithmétique, qui est une extension du théorème de Ramsey. Ce résultat constitue un des premiers théorèmes s’exprimant dans un langage simple, indémontrable dans (AP).

2.1.1 Définitions et notations

Soit M un ensemble et n un entier. On note [M]^{n} = {F ⊆ M/Card(F) = n}. Si r est un cardinal, une fonction P : [M]^{n} → r est appelée partition de [M]^{n}

en r morceaux.

H ⊆ M est dit homogène pour P si la restriction de P à [H]^{n} est constante. Un ensemble fini H⊂ℕ est dit relativement large si Card(H) ≥ min(H). Si M est un ensemble, k et r des cardinaux, et n un entier, on note

M → (k)_{r}^{n}

si quelle que soit P partition de [M]^{n} en r morceaux, il existe H⊂M homogène pour P de cardinalité k. Si r et k sont finis et M⊂ω on note

M →^{∗} (k)_{r}^{n}

si quelle que soit P partition de [M]^{n} en r morceaux, il existe H⊂M relativement large, homogène pour P de cardinalité supérieure ou égale à k.

2.1.2 Le théorème de Ramsey et ses extensions

Théorème 2.1.1 Théorème de Ramsey Quels que soient n, k, r entiers, il existe m entier tel que pour tout m’ > m on a m′ → (k)_{r}^{n}

Pour la preuve de ce théorème, voir [4] . Par exemple, pour n=2 r=2 et k=3 ce théorème affirme que tout graphe de plus de 6 sommets admet un sous graphe de taille 3 vide ou complet. Voici un première extension du théorème de Ramsey, pour un cardinal infini :

Théorème 2.1.2 Théorème de Ramsey infini Soient n, r ∈ ω; alors ω→(ω)_{r}^{n}.

Pour la preuve de ce théorème, voir [1].

Enoncé 1 ∀n∀x∃y > x({x, x + 1, .., y} →^{∗} (n)_{n}^{n})

Preuve Cet énoncé est vrai mathématiquement. La preuve générale (hors de (AP)) de cet énoncé utilise un résultat complémentaire:

Lemme 2.1.1 Lemme de Kőnig Soit A un arbre possédant un nombre dénombrable de niveaux, et à chaque niveau un nombre fini de sommets, alors on peut tracer dans A un chemin infini, c’està-dire une suite de sommets de A dont les indices correspondent à leur niveau dans A.

Pour la preuve de ce lemme, voir [1].

La démonstration se fait par l’absurde : supposons ∃n∃x(∀y > x∃P_{y} : [{x, .., y}]^{n} → n contrexemple au théorème.) Alors on construit un arbre avec les P_{y} et l’ordre P_{y_{1}} est en dessous P_{y_{0}} ssi y_{1} < y_{0} et P_{y1} est la restriction de P_{y_{0}} à [{x, .., y_{1}}]^{n} . Le lemme de Kőnig assure alors l’existence d’un P : [ω]^{n} → n tel que la restriction de P à tous les ensembles [{x, ..y}]^{n} soit un contrexemple à l’énoncé ci dessus. Mais alors si H ⊆ ω est l’ensemble infini donné par le théorème de Ramsey infini homogène pour P, il suffit de prendre y assez grand pour aboutir à une contradiction, puisque H ∩ x, ..y est alors homogène pour P. □

Remarque: On peut en fait démontrer, en examinant la preuve ce dessus de plus près : pour tout n, pour tout x (AP) ⊢ ∃y{x, ..., y} →^{∗} (n)_{n}^{n} .

2.1.3 Théorème de Paris-Harrington

Le théorème de Paris Harrington affirme que l’énoncé 1, bien que “vrai” , est en fait indémontrable dans l’arithmétique :

Théorème 2.1.3 Paris Harrington (1977)

Soit F_{P H} ≡ ∀n∀x∃y > x({x, .., y} →^{∗} (n)_{n}^{n}).

Alors F_{P H} n’est pas démontrable dans (AP).

2.2 Démonstration du théorème de Paris-Harrington

La preuve du théorème se fait en trois étapes :

1. On construit une nouvelle théorie T ;

2. On démontre

(AP) ⊢ F_{P H} → Con_{T}

par construction de modèle ;

3. On démontre

(AP) ⊢ Con(T) → Con_{(AP)}

ce qui achève la démonstration, en utilisant le second théorème de Gödel.

2.2.1 Définition de la théorie T

On identifiera les sous-ensembles de ω avec des suites finies croissantes. Le langage de T est celui de AP auquel s’ajoute un nombre infini de symboles de constante c_{0}, c_{1}, ... Pour toue formule θ(Y) du langage de AP on définit une formule limitée comme suit: si θ est sous forme prénexe ∃x_{1}...∀x_{r}ϕ(X, Y) alors θ^{∗}(Y; z_{1}, ..., z_{r}) est ∃x_{1} < z_{1}...∀x_{r} < z_{r}ϕ(X, Y). Les axiomes de T sont les suivants :

1. Les axiomes usuels de définition recursive pour +, x, ¡, et les axiomes d’induction, mais uniquement pour les formules limitées.

2. Quel que soit i, l’axiome (c_{i})^{2} < c_{i+1}.

3. Pour tout sous ensemble I = i_{1}, ..., i_{r} de ω on définit c(I) = c_{i_{1}}, ..., c_{i_{r}}. Pour tout i¡K,K’ et pour toute formule limitée ψ(Y; Z), si Z,K et K’ ont même taille, on a l’axiome suivant :

∀Y < c_{i} [ψ(Y; c(K)) ↔ ψ(Y, c(K′))].

2.2.2 (AP) ⊢ F_{P H} → Con_{T}

Pour démontrer ce résultat, on utilise l’énoncé suivant :

Enoncé 2 Pour tous e, k et r, il existe M tel que quelle que soit la famille ⟨P_{ξ} : [M]^{e} → r, ξ < 2^{max(M)}⟩ , il existe X de cardinal au moins k tel que:

1. si a,b ∈ X et a < b , alors a^{2} < b

2. si a ∈ X et ξ < 2^{a} , alors X est homogène pour P_{ξ} .

On a ainsi :

Proposition 1 L’énoncé 2 implique la consistance de T.

Preuve Cette preuve utilise un résultat sur les partitions :

Lemme 2.2.1 Soient n partitions P_{i} : [M]^{e_{i}} → r_{i}; 0 ≤ i < n . Soit e = max(e_{i}) ; r = ∏ max(r_{i}, 7) . Il existe une partition P : [M]^{e} → r telle que ∀H ⊆ M de cardinal e au moins, H est homogène pour tous les P_{i} si et seulement si H est homogène pour P.

Preuve Voir [3]. □ D’après le théorème de compacité, il suffit de trouver un modèle des sous ensembles finis de la théorie T. Soit alors S un tel sous ensemble. On note {c_{0}, ..., c_{k−1}} les constantes qui apparaissent dans les axiomes de S. On va montrer que si, pour un certain M dépendant de S, x_{0}, ..., xk − 1 sont les k premiers éléments de l’ensemble X donné par l’énoncé 2, S a un modèle de la forme ⟨ω; +, x, <; x_{0}, ..., x_{k−1}⟩ .

Les axiomes de type 1 et 2 de S sont aisément vérifiés (pour 2 on utilise le point 1 de l’énoncé 2 ). On démontre les axiomes de type 3 grace au point 2 de l’énoncé. □ Remarque: La démonstration peut être faite dans (AP). Le résultat suivant achève la démonstration:

Proposition 2 L’énoncé ∀e, r, k : M →^{∗} (k)_{r}^{e} implique celui de la proposition 1.

Preuve La preuve est une preuve technique faisant intervenir de la combinatoire et les ensembles relativement larges. Voir [3]. □

2.2.3 (AP) ⊢ Con(T) → Con_{(AP)}

Soit 𝔘 ⊧ T et soit I le segment initial de 𝔘 des a < c_{i} pour un certain i dans ω. D’après les axiomes de type 2 de T, I est clos pour x et +.

Lemme 2.2.2 ℑ = ⟨I, +, x, <⟩ est un modèle de (AP).

En effet, on a le résultat suivant:

Lemme 2.2.3 Etant donnés i < K , A < c_{i} et θ(Y), où K, A, et Y sont de la taille appropriée,

ℑ ⊧ θ(A) si et seulement si (U) ⊧ θ^{∗}(A; c(K)).

Preuve Par induction sur θ: Si θ(Y) est de la forme ∃xψ(x, Y) alors θ^{∗}(Y; Z) est ∃x < z_{1}ψ^{∗}(x, Y, z_{2}, ..., z_{r}). Donc ℑ ⊧ θ(A) ssi pour un certain b dans I et un certain J (où min(J) est assez grand) (U) ⊧ ψ^{∗}(b, A; c(J)) , ce qui arrive ssi pour un certain K’ (U) ⊧ θ^{∗}(A; c(K′)) ce qui donne le résultat ( par les axiomes de type 3 de la définition de T ). □

Références

[1] Kunen Combinatorics, in Handbook of mathematical logic, 1977 Edité par Jon Barwise [2] Smorynski The incompleteness theorems, in Handbook of mathematical

logic, 1977 Edité par Jon Barwise

[3] Paris Harrington An incompleteness in PA, in Handbook of mathematical logic, 1977 Edité par Jon Barwise

[4] Erdös, Hajnal, Rado Partition relations for cardinal numbers, 1965 Acta Math. Acad. Sci. Hungar.

[5] Cori-Lascar Logique mathématique II, 1993 Masson