title: Astuce de Rosser
text: # Astuce de Rosser
  
  En logique mathématique, l’astuce de Rosser (en anglais Rosser’s trick) 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é, appelé parfois théorème de Gödel-Rosser, en l'étendant à des théories cohérentes qui ne sont pas forcément ω-cohérentes.
  
  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 une théorie cohérente qui n'est 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
  
  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, 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):
  
  * T ne prouve pas ρ
  * 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
  
      $\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.
  
  