Astuce de Rosser

En logique mathématique, l’astuce de Rosser (Rosser’s trick(en)) permet de démontrer un énoncé renforcé du premier théorème d'incomplétude de Gödel, vu comme résultat d'indécidabilité, en l'étendant à des théories cohérentes qui ne sont pas forcément l’ω-cohérentes, et appelé parfois théorème de Gödel-Rosser. John Barkley Rosser l'introduit dans un article de 1936, alors que la démonstration originale des théorèmes d'incomplétude de Gödel a été publiée en 1931.

La démonstration du premier théorème d'incomplétude introduit pour une théorie T un énoncé G_T qui, via un codage et dit de manière informelle, signifie « cet énoncé n'est pas démontrable ». Gödel démontre que si la théorie est cohérente, l'énoncé G_T est vrai c'est--à-dire qu'il n'est pas démontrable. Mais sous ces hypothèses il est possible que la négation de G_T, soit démontrable dans T. Pour éliminer ces cas, Gödel introduit une hypothèse ad hoc supplémentaire, la ω-cohérence : si la théorie T est de plus ω-cohérente, alors G_T est indécidable dans T (elle n'est pas démontrable dans T et sa négation non plus).

L'astuce de Rosser permet de produire un énoncé indécidable pour n'importe quelle théorie cohérente, pas forcément ω-cohérente. Elle consiste à utiliser un énoncé renforcé qui, toujours via codage, signifie « si cet énoncé est démontrable, alors il existe une démonstration plus courte de sa négation » (ce qui dans une théorie cohérente a pour conséquence que cet énoncé n'est pas démontrable).

Contexte

L’astuce de Rosser reprend essentiellement les hypothèses du premier théorème d'incomplétude de Gödel. La théorie T est supposée récursivement axiomatisable (c'est le cas par exemple si elle a un nombre fini d'axiomes, ou de l'arithmétique de Peano), consistante (ou cohérente) et contenant « suffisamment » d'arithmétique élémentaire, par exemple l'arithmétique de Robinson.

La démonstration de Gödel définit pour une telle théorie une formule Dem_T(x, y) dont la signification est que y est le code sous forme d’un nombre entier naturel (un nombre de Gödel) pour une formule et x est le code d’une démonstration de la formule codée par y à partir des axiomes de T (dans le reste de cet article, aucune distinction ne sera faite entre le nombre y et la formule codée par y ; le nombre codant une formule φ sera noté #φ).

En outre, la formule Pvbl_T (y) est définie comme ⱻ x Dem_T(x,y). Elle définit parmi les entiers l'ensemble des codes de formules démontrables dans T. Le codage des formules permet d'introduire une fonction neg(y), définie sur tous les entiers naturels, avec la propriété que si y est le code d'une formule φ, alors neg(y) est le code de la formule ¬φ, négation de la formule φ.

L’énoncé de Gödel de la théorie T est une formule G_T telle que T prouve que G_T ⇔ ¬ Pvbl_T(#G_T). La démonstration de Gödel montre que si T est consistante, alors G_T n'est pas prouvable dans T. Mais pour montrer que la négation de G_T n'est pas non plus prouvable dans T, Gödel ajoute une hypothèse plus forte, à savoir que la théorie est ω-consistante et non simplement consistante. La théorie T= PA + ¬ G_PA a pour conséquence ¬ G_T. Rosser (1936) a construit un énoncé auto-référentiel renforcé qui peut être utilisé pour remplacer l’énoncé de Gödel dans la démonstration de Gödel, levant ainsi le recours à l’ω-consistance.

L’assertion de Rosser

Dans une théorie arithmétique fixée T, associons respectivement Proof_T (x, y) et neg(x) au prédicat de la preuve et à la fonction de négation. Un prédicat de preuve modifié Proof^R_T(x,y) est défini comme suit :

$\mathrm {Proof} _{T}^{R}(x,y)\equiv \mathrm {Proof} _{T}(x,y)\land \lnot \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (y))],$

ou a contrario

$\lnot \mathrm {Proof} _{T}^{R}(x,y)\equiv \mathrm {Proof} _{T}(x,y)\to \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (y))].$

Ce prédicat de preuve modifié est utilisé pour définir un prédicat de prouvabilité modifié Pvbl^R_T(y) :

$\mathrm {Pvbl} _{T}^{R}(y)\equiv \exists x\mathrm {Proof} _{T}^{R}(x,y).$

Informellement parlant, Pvbl^R_T(y) proclame le fait que y est prouvable via une certaine preuve codée x telle qu'il n'existe aucune preuve codée plus petite de la négation de y. Sous l’hypothèse de consistance de T, pour chaque formule φ la formule Pvbl^R_T(#φ) tiendra si et seulement si Pvbl_T(#φ) se tient. Cependant, ces prédicats ont des propriétés différentes du point de vue de leur prouvabilité dans T. Utilisant le lemme de la diagonale, appelons ρ une formule telle que T démontre

$\mathrm {\rho } \leftrightarrow \lnot \mathrm {Pvbl} _{T}^{R}$(#ρ).

La formule ρ est l’assertion de Rosser de la théorie T.

Le théorème de Rosser

Soit T une théorie « efficace », consistante, contenant suffisamment d'arithmétique ainsi que l’assertion ρ de Rosser. Alors il vient (Mendelson 1977, p. 160):

1. T ne prouve pas ρ
2. T ne prouve pas ¬ ρ.

La démonstration de (1) est semblable à celle de la démonstration du premier théorème d'incomplétude de Gödel.

La preuve de (2) engage plus avant. Supposons que T démontre ¬ ρ et soit e un nombre entier naturel codant pour une preuve de ¬ ρ dans T. Etant donné que T est consistante, il n'y a aucun code pour une démonstration de ρ dans T, de sorte que Proof^R_T(e, neg (#ρ)) tiendra (parce qu'il n'y a aucun z < e qui codera pour une démonstration de ρ).

L’hypothèse que T inclut suffisamment d’arithmétique assure que T permettra de démontrer

$\mathrm {\forall } x(e\leq x\to \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (\#\rho ))]),$

et (utilisant l’hypothèse de consistance et le fait que e est un nombre naturel)

$\mathrm {\lnot } \exists x<e[\mathrm {Proof} _{T}(x,\#\rho )].$

Partant de cette dernière formule, les hypothèses sur T permettent de démontrer

$\mathrm {Proof} _{T}(x,\#\rho )\to e\leq x.$

Donc T prouve

$\mathrm {\forall } x[\mathrm {Proof} _{T}(x,\#\rho )]\to \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (\#\rho ))].$

Mais cette dernière formule est de façon prouvable équivalente à ρ dans T, par définition de ρ, ce qui signifie que T démontre ρ. C'est une contradiction, puisque T a été présumée démontrer ¬ ρ et assumée consistante. Ainsi T ne peut pas démontrer ¬ ρ tout en étant consistante.

Références

• (en) Cet article est partiellement ou en totalité issu de l’article de Wikipédia en anglais intitulé « Rosser's trick » (voir la liste des auteurs).
• (en) Mendelson, Introduction to Mathematical Logic, 1977, p. 160
• (en) Craig Smorynski, « The incompleteness theorems », dans Jon Barwise, Handbook of Mathematical Logic, North Holland, 1977 (p. 840)
  
• (en) Craig Smorynski, Logical Number Theory I -- An Introduction, Springer Verlag, 1991 (ISBN 3-540-52236-0 et 0-387-52236-0).
• (en) Rosser, « Extensions of some theorems of Gödel and Church », Journal of Symbolic Logic, vol. 1,‎ 1936, p. 87–91.

Liens externes

• (en) "Computability and Incompleteness", notes prises par Avigad (2007).