Astuce de Rosser
Pour les articles homonymes, voir Rosser (homonymie).
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é GT 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é GT 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 GT, 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 GT 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 modifier
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 DemT(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 PvblT (y) est définie comme ⱻ x DemT(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 GT telle que T prouve que GT ⇔ ¬ PvblT(#GT). La démonstration de Gödel montre que si T est consistante, alors GT n'est pas prouvable dans T. Mais pour montrer que la négation de GT 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 + ¬ GPA a pour conséquence ¬ GT. 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 modifier
Dans une théorie arithmétique fixée T, associons respectivement ProofT (x, y) et neg(x) au prédicat de la preuve et à la fonction de négation.
Un prédicat de preuve modifié ProofRT(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))],}](https://wikimedia.org/api/rest_v1/media/math/render/svg/2a5a56db1ef8858fd31c91955553d4b62d913a6d)
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))].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/8a0a5807eb9759ae5ec9939eda6d0132942c341f)
Ce prédicat de preuve modifié est utilisé pour définir un prédicat de prouvabilité modifié PvblRT(y) :
Informellement parlant, PvblRT(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 PvblRT(#φ) tiendra si et seulement si PvblT(#φ) 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
- (#ρ).
La formule ρ est l’assertion de Rosser de la théorie T.
Le théorème de Rosser modifier
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 ProofRT(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 ))]),}](https://wikimedia.org/api/rest_v1/media/math/render/svg/b3cbe310143539dcd665c31bfcd8488fb51ddf1a)
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 )].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/7e4ca6728e92f79d2aa695bcda52be4e038b422d)
Partant de cette dernière formule, les hypothèses sur T permettent de démontrer
Donc T prouve
![{\displaystyle \mathrm {\forall } x[\mathrm {Proof} _{T}(x,\#\rho )]\to \exists z\leq x[\mathrm {Proof} _{T}(z,\mathrm {neg} (\#\rho ))].}](https://wikimedia.org/api/rest_v1/media/math/render/svg/f124409ac8357883898f3c5f4105bbc47e0b4fc9)
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.
Notes et références modifier
- (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).
- Raphael Robinson a mis en évidence que cette hypothèse était un peu moins minimale pour la démonstration du théorème de Gödel-Rosser que pour celle du théorème de Gödel : pour le théorème de Gödel il suffit de supposer que les énoncés Σ0 (donc Σ1) vrais sont démontrables, pour Gödel-Rosser il faut ajouter les énoncés universels exprimant qu'un entier standard est toujours comparable avec un entier, voir Smorynski 1991.
Bibliographie modifier
- (en) Mendelson, Introduction to Mathematical Logic, , p. 160
- (en) Craig Smorynski, « The incompleteness theorems », dans Jon Barwise, Handbook of Mathematical Logic, North Holland, (p. 840)
- (en) Craig Smorynski, Logical Number Theory I -- An Introduction, Berlin/New York, Springer Verlag, , 405 p. (ISBN 978-3-540-52236-2 et 0-387-52236-0, BNF 37385798).
- (en) Rosser, « Extensions of some theorems of Gödel and Church », Journal of Symbolic Logic, vol. 1, , p. 87–91.
Lien externe modifier
• (en) "Computability and Incompleteness", notes prises par Avigad (2007).
