# Théorie oméga-cohérente

En logique mathématique une théorie arithmétique est appelée théorie ω-cohérente (oméga-cohérente) quand, pour toute propriété P des nombres entiers que l'on peut exprimer dans le langage de la théorie,
    si pour chaque entier n, P(n) est démontrable dans la théorie,
    alors ¬∀x P(x) n'est pas démontrable dans la théorie (¬ pour la négation, ∀ pour la quantification universelle, « pour tout »).
Quand on prend pour P un énoncé clos (qui ne dépend pas de x) on retrouve la définition de la cohérence, appelée parfois dans ce contexte cohérence simple, qui est donc conséquence de l'ω-cohérence.

## Hypothèses de cohérence et modèle standard

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 Σ$_1$$^0$ 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 Σ$_1$$^0$ vrais soient démontrables. Dans une telle théorie la cohérence simple équivaut à ce que les énoncés Π$_1$$^0$ (les négations d'énoncés Σ$_1$$^0$) démontrables sont vrais.

## Existence de théories cohérentes mais ω-incohérentes

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 Π$_1$$^0$, 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.