Des formes récursives de la déclaration de Godel sont-elles possibles?

L'auto-référentialité du problème P / NP a parfois été mise en évidence comme un obstacle à sa résolution, voir, par exemple, l'article de Scott Aaronson, P vs NP est-il formellement indépendant ? L'une des nombreuses résolutions envisageables pour P / NP serait une démonstration que le problème est formellement indépendant de ZFC ou vrai mais non prouvable.

Il est concevable que l'auto-référentialité du problème puisse poser un défi plus profond dans les preuves d'indépendance, par exemple, si les déclarations sur sa prouvabilité sont elles-mêmes non prouvables ou autrement impossibles à raisonner.

Supposons que nous appelons un théorème T Godel_0 s'il est vrai mais non prouvable au sens du théorème de Godel. Appelez T Godel_1 si la déclaration "T is Godel_0" est vraie, mais impossible à prouver. Appelez T Godel_i si l'énoncé "T est Godel _ {(i-1)} est vrai.

Nous savons que les instructions Godel_0 existent, et quelques exemples ont été trouvés "à l'état sauvage" qui ne sont pas construits explicitement à cet effet, comme dans cet article .

Ma question est: existe-t-il des déclarations Godel_1 ou plus? Ces déclarations sont-elles une conséquence naturelle du théorème de Godel?

Qu'en est-il d'une affirmation dont nous ne pouvons prouver absolument rien: c'est-à-dire, pour laquelle pour tout k > 0, T est Godel_k?

Je peux poser une question analogue pour l'indépendance formelle, bien que je soupçonne que la réponse est "non".

Pour revenir à la question P vs NP, permettez-moi de demander s'il y a même un indice que le théorème de Godel est pertinent pour les questions de séparabilité des classes. Des déclarations vraies mais non prouvables ont-elles été identifiées en ce qui concerne les classes de complexité - au-delà, bien sûr, du lien évident entre le problème d'arrêt et le théorème de Godel?

Comme d'autres l'ont souligné, l'énoncé de votre question présente certaines difficultés techniques. Pour les redresser, commençons par éviter d'utiliser le terme "indémontrable" sans qualification, et expliquons de quel ensemble d'axiomes votre énoncé T est censé être indémontrable. Par exemple, supposons que nous nous intéressions aux énoncés T qui ne sont pas prouvables de PA, les axiomes de l'arithmétique Peano de premier ordre.

Le premier ennui est que "T est vrai" n'est pas exprimable dans le langage arithmétique de premier ordre, par le théorème de Tarski. Nous pourrions contourner cela en travaillant dans une métathéorie suffisamment puissante pour définir la vérité d'une déclaration arithmétique, mais je pense que pour vous, c'est une voie inutilement compliquée à prendre. Je pense que vous n'êtes pas tellement intéressé par la vérité en soi mais par la prouvabilité. Autrement dit, je soupçonne que vous seriez satisfait de définir T comme Godel_0 si T est vrai mais non démontrable en PA, et de définir T comme Godel_1 si T n'est pas démontrable en PA mais "T est non démontrable en PA" n'est pas démontrable en PA, et définissant T comme étant Godel_2 si T est indémontrable en PA et "T est indémontrable en PA" est indémontrable en PA mais "'T est indémontrable en PA' est indémontrable en PA" est indémontrable en PA, etc. De cette façon, nous ne '

Cela suffit pour rendre votre question précise, mais malheureusement, il existe alors une solution plutôt banale. Prenez T = "PA est cohérent." Alors T est vrai parce que PA est cohérent, et T n'est pas prouvable dans PA par le 2ème théorème d'incomplétude de Goedel. De plus, "T est indémontrable en PA" est également indémontrable en PA pour une raison quelque peu idiote: toute déclaration de la forme "X est indémontrable en PA" est indémontrable en PA car "X n'est pas démontrable en PA" implique trivialement "PA est cohérent "(puisque les systèmes incohérents prouvent tout ). Donc, T est Godel_n pour tous les n, mais je ne comprends pas vraiment à votre question.

Nous pourrions essayer de "corriger" votre question pour éviter de telles banalités, mais laissez-moi plutôt essayer de répondre à ce que je pense être votre question. Tacitement, je crois que vous confondez la force logique nécessaire pour prouver un théorème avec la difficulté psychologiquede le prouver. Autrement dit, vous interprétez un résultat de la forme "T n'est pas démontrable dans X" comme disant que T est en quelque sorte au-delà de notre capacité à comprendre. Il y a ces conjectures monstrueuses là-bas, et nous chérissons les humains à casser des fouets PA ou ZFC ou ce que vous avez à ces bêtes féroces, en essayant de les apprivoiser. Mais je ne pense pas que "T ne soit pas prouvable en X" devrait être interprété comme signifiant "T est impossible à raisonner". Il s'agit plutôt de mesurer une propriété technique particulière de T, à savoir sa force logique. Donc, si vous essayez de trouver l'über-monstre, je ne pense pas que trouver quelque chose qui est non seulement improuvable, mais dont l'improvabilité est indémontrable, etc., est la bonne direction à suivre.

Enfin, concernant votre question à savoir si l'improvabilité semble liée à la séparabilité des classes de complexité, il existe des liens entre l'intractabilité informatique et l'improvabilité dans certains systèmes d'arithmétique bornée. Une partie de cela est mentionnée dans le document d'Aaronson que vous citez; voir aussi le livre de Cook et Nguyen, Logical Foundations of Proof Complexity .

Je ne suis pas sûr de la définition de Godel_1. Pouvez-vous essayer de le formaliser un peu plus?

Comment pouvez-vous encoder la formule "T is Godel_0"? Pour cela, vous devrez en quelque sorte coder que "T est sémantiquement vrai" sans faire référence à la notion de preuve. Comment peux-tu faire ça?

Les instructions Godel_n existent pour chaque n. Vous pourriez être intéressé par The Unprovability of Consistency, un livre de George Boolos. Il définit une logique modale dans laquelle Box signifie "est prouvable," Diamond signifie "est cohérent", puis procède à une enquête sur le comportement des phrases de type Godel. (Il a également écrit un livre de suivi, The Logic of Provability.)