Théorie oméga-cohérente

D'un point de vue sémantique, dans la définition ci-dessus le n fait référence à un entier standard, qui renvoie à un entier « ordinaire » (un entier du méta-langage dans lequel on raisonne sur la théorie), mais une théorie arithmétique (du premier ordre) a nécessairement des modèles non standards, c'est-à-dire des modèles ayant d'autres éléments que les entiers standards. Le x fait référence à un élément quelconque de ce modèle (donc pas forcément un entier standard).

Cette définition a été introduite par Kurt Gödel, comme hypothèse pour son premier théorème d'incomplétude. Plus précisément, Gödel montre que pour une théorie arithmétique vérifiant certaines hypothèses naturelles, il existe un énoncé G qui n'est pas démontrable si la théorie est cohérente (cohérence simple), et dont la négation n'est pas démontrable si la théorie est ω-cohérente.

D'autres hypothèses fortes de cohérence ont été introduites après Gödel, qui supposent que les énoncés démontrables dans la théorie qui appartiennent à une certaine classe sont vrais dans le modèle standard N, en particulier pour des classes d'énoncés définis à l'aide de la hiérarchie arithmétique. On montre que ce sont bien des hypothèses de cohérence car elles ont pour conséquence que certains énoncés ne sont pas démontrables, ceux qui appartiennent à la classe en question et qui sont faux. Par exemple, dans le cas du premier théorème d'incomplétude, pour démontrer que la négation de l'énoncé G n'est pas démontrable, il suffit de supposer que les formules Σ₁⁰ démontrables dans la théorie sont vraies dans le modèle standard. Cette hypothèse, appelée parfois 1-cohérence, est conséquence de l'ω-cohérence.

Une hypothèse naturelle sur les théories arithmétiques, qui intervient pour le théorème de Gödel (voir Théorèmes d'incomplétude de Gödel#Formules Σ1) est que les énoncés Σ₁⁰ vrais soient démontrables. Dans une telle théorie la cohérence simple équivaut à ce que les énoncés Π₁⁰ (les négations d'énoncés Σ₁⁰) démontrables sont vrais.

Le premier théorème d'incomplétude (comme d'ailleurs le second) a pour conséquence l'existence de théories arithmétiques cohérentes qui ne sont pas ω-cohérentes.

En effet, pour une théorie arithmétique T donnée, par exemple l'arithmétique de Peano, ou l'arithmétique de Robinson l'énoncé G introduit par Gödel, qui dépend de T, est une formule Π₁⁰, c'est-à-dire un énoncé arithmétique du type ∀x H(x), tel que pour chaque entier n l'énoncé H(n) ou sa négation soit vérifiable par le calcul, c'est-à-dire que la vérité dans le modèle standard de H(n) est décidable au sens algorithmique. Beaucoup d'énoncés classiques de l'arithmétique ont une forme analogue, comme la conjecture de Goldbach ou le théorème de Fermat-Wiles, de même que l'énoncé du problème de l'arrêt. L'énoncé G énonce pour sa part que pour tout x, x n'est pas le code d'une preuve de G. On peut vérifier par le calcul qu'un certain entier est ou non le code d'une preuve d'une formule donnée (cela revient intuitivement à « vérifier » une preuve, non à la découvrir).

La forme même de l'énoncé de Gödel a pour conséquence que chaque formule H(n) est vraie dans le modèle standard N et démontrable dans la théorie T.

Le premier théorème d'incomplétude affirme qu'une théorie T cohérente n'a pas pour conséquence l'énoncé G = ∀x H(x), c'est-à-dire que la théorie T + ¬ G est cohérente. Cette théorie est ω-incohérente, puisque pour chaque entier n, H(n) est démontrable, alors que ¬ ∀x H(x), qui est un axiome, est a fortiori démontrable.

L'énoncé de cohérence de la théorie T a la même forme (aucun entier ne code une preuve de 0 = 1) et on peut conduire le même raisonnement à partir du second théorème d'incomplétude.

• Craig Smorynski, Logical Number Theory I -- An Introduction, Springer Verlag, 1991 - (ISBN 3-540-52236-0) - (ISBN 0-387-52236-0).
• Craig Smorynski, The Incompletness Theorems, in Handbook of Mathematical Logic édité par J. Barwise, North Holland, 1977 - (ISBN 0-7204-2285-X)
• Jean-Yves Girard, Proof Theory and Logical Complexity, volume 1. Bibliopolis, 1987.