Astuce de Rosser

Les hypothèses du théorème de Gödel-Rosser reprennent 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[1], 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.

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 :

${\displaystyle \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

${\displaystyle \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) :

${\displaystyle \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

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

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

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 une preuve de ¬ ρ dans T. Etant donné que T est consistante, il n'y a aucun code d’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 une démonstration de ρ).

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

${\displaystyle \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)

${\displaystyle \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

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

Donc T prouve

${\displaystyle \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.

• (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).