Les théorèmes d'indécidabilité peuvent-ils être détectés par une machine? [fermé

Question

Cette question a été initialement écrite dans Mathoverflow, mais un commentaire m'a recommandé de le réécrire en tant que question CS.

Ce n'est pas une question mathématiquement formalisée. Je suis désolé pour cela, mais je pense que cela ressemble plus aux mathématiques qu'à la philosophie.

Lorsque nous avons prouvé un théorème B qui dit "B est indécidable", nous n'essayons pas de prouver ni b ni (pas b). Une machine peut-elle faire la même chose? Peut-il détecter le "sens" d'une déclaration, comme "quelque chose est indécidable"?

Voici une raison pour laquelle je ne pense pas.

Supposons une phrase

universal_Turing_machine(program, input, output)

est vrai si et seulement si la sortie résultant de "programme" avec "entrée" donnée est "sortie". Bien sûr, si le programme ne s'arrête pas, il serait faux pour toute "entrée" et "sortie".

Maintenant, soit x un nombre de dieu d'une phrase. Considérez la phrase suivante:

there is no y such that:
y is a Godel number of a string which ends with a sentence encoded as x, 
and universal_Turing_machine(program, y, true)

Si le programme agit comme un "programme de décision acceptant des preuves valides", cette phrase signifie évidemment "une phrase codée comme X n'est pas prouvable". Sinon, cette phrase ne signifie aucune indécidabilité. Par conséquent, si une machine peut détecter les théorèmes indécidabilité, il doit détecter des programmes qui agissent comme "des programmes de décision acceptant des preuves valides"

Mais selon le théorème de Rice, la détection de programmes qui a une propriété spécifique n'est pas possible.

Pensez-vous que cette "raison" a du sens? Comme ce n'est pas une pure question mathématique, j'espère écouter vos opinions. Merci.