Machines de Turing dont l'arrêt n'est pas démontrable?

J'ai une question naïve: existe-t-il une machine de Turing dont la terminaison est vraie mais non démontrable par aucune théorie naturelle, cohérente et finement axiomatisable? Je demande une simple preuve d'existence plutôt qu'un exemple spécifique.

Cela pourrait avoir un lien avec l'analyse ordinale . En effet, pour une machine de Turing , on peut définir comme le moins ordinal d'une théorie cohérente prouvant sa terminaison (ou l'infimum de ces ordinaux). Je suppose donc qu'il serait équivalent de se demander s'il existe tel que ? $M$ $O(M)$ $M$ $O(M) \geq \omega_1^{CK}$

turing-machines proof-theory halting-problem Super8
la source

La quantification ne devrait-elle pas fonctionner dans l'autre sens? Le simple ajout de TM X s'arrête comme axiome serait cohérent pour tout X qui s'arrête réellement sur toutes les entrées (et fini si vous le faites uniquement pour la MT en question). Avec les quantificateurs inversés, que diriez-vous d'une MT qui s'arrête si l'entrée n'est pas une preuve de cohérence pour le système axiomatique et entre dans une boucle infinie sinon.

Yonatan N

Votre suggestion est intéressante, merci. J'étais conscient de votre inquiétude lors de la formulation de la question, c'est pourquoi j'ai ajouté "naturel" dans les exigences. Bien sûr, le problème est de savoir si nous pouvons donner une définition formelle du «naturel» qui exclurait cette construction artificielle.

Super8

pense que la réponse est non parce que si elle s'arrête, alors on exécute simplement la machine et elle s'arrêtera en un nombre fini d'étapes, et c'est une preuve, et ce fait peut être converti en n'importe quel système de preuve raisonnablement puissant. d'autre part, pense qu'il est possible de coder / convertir / traduire le thm non démontrable de godel en une machine sans arrêt pour laquelle le non-arrêt n'est pas démontrable. cette question est similaire, existe-t-il une TM qui s'arrête sur toutes les entrées mais la propriété n'est pas prouvable cs.se

vzn

Vous pouvez construire une machine de Turing

qui calcule la séquence de Goodstein

de l'entrée

et s'arrête lorsqu'elle atteint

L'arrêt de

ne peut pas être prouvé en arithmétique Peano; c'est-à-dire que le théorème de Goodstein n'est pas prouvable en utilisant les axiomes Peano de l'arithmétique. Voir Laurie Kirby, Jeff Paris, Résultats de l'indépendance accessible pour l'arithmétique Peano (1982)

M

$M$

G (n)

$G(n)$

n

$n$

0

$0$

M

$M$

Marzio De Biasi

Merci, je ne connaissais pas ces entrées. Ce que je demande est plus fort cependant, j'aimerais que l'on prouve l'improvisibilité de toute théorie raisonnable (plutôt qu'une théorie spécifique telle que l'AP). Je ne sais pas si la question a une réponse définitive.

Super8

Réponses:

La terminaison d'une machine de Turing (sur une entrée fixe) est une phrase et toutes les théories arithmétiques de premier ordre habituelles sont complètes pour les phrases , c'est-à-dire que toutes les vraies déclarations sont prouvables dans ces théories. $\Sigma^0_1$ $\Sigma^0_1$ $\Sigma^0_1$

Si vous regardez la totalité à la place de l' arrêt , c'est-à-dire qu'un TM s'arrête sur toutes les entrées, alors c'est une phrase complète de et pour toute théorie cohérente axiomatisable calculable qui est suffisamment forte (par exemple, prolonge la théorie de Robinson ), il y a TM dont la totalité ne peut être prouvée dans cette théorie. $\Pi^0_2$ $Q$

Kaveh
la source

Oui, je cherchais la totalité, car bien sûr le problème est trivial pour une entrée fixe. Je vais réfléchir à votre affirmation et à la façon de la prouver, mais à ce stade, je ne vois pas comment le fait de considérer les théories "axiomatisables par ordinateur" exclut le problème susmentionné? De plus, dans votre déclaration, la MT dépend de la théorie considérée, pouvons-nous obtenir ma déclaration plus forte par une sorte de diagonalisation?

Super8

Voici un moyen simple: l'ensemble des fonctions calculables prouvées totales d'une telle théorie est ce, l'ensemble des fonctions calculables totales n'est pas ce, ou bien vous pouvez diagonaliser par rapport aux fonctions prouvées totales de la théorie.

Kaveh

σ

$\sigma$

α

$\alpha$

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$

α

$\alpha$

M

$M$

O (M)

$O(M)$

α

$\alpha$

M

$M$

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$ (c'est-à-dire que le système de notation peut être librement choisi). Cette définition a-t-elle un sens?

Super8

@ Super8, je ne suis pas sûr. Généralement, l'association des ordinaux aux théories n'est pas canonique, il existe différentes façons de s'associer pour le faire. Vous pouvez commencer avec une théorie faible comme PRA et ajouter une induction sur des ordinaux calculables avec de belles séquences fondamentales, etc. mais je ne sais pas pourquoi vous aimeriez le faire.

Kaveh

Ok, je n'avais pas réalisé le problème, je vais essayer de trouver une meilleure définition par moi-même.

Super8

Je ne suis pas un expert en logique, mais je pense que la réponse est non . Si la machine Turing s'arrête et que le système est suffisamment puissant, vous devriez pouvoir écrire l'historique complet de calcul de la machine Turing sur son entrée. Quand on vérifie que le résultat du calcul est une séquence terminale de transitions, on peut voir que la machine s'arrête. Quelle que soit la façon dont vous formalisez les machines de Turing dans votre théorie, vous devriez être en mesure de montrer dans toute théorie raisonnable qu'une machine qui s'arrête s'arrête en fait. Par analogie, pensez à essayer de prouver qu'une somme finie est égale à ce qu'elle est égale; par exemple, prouver que 5 + 2 + 3 + 19 + 7 + 6 = 42, ou 5 + 5 + 5 = 15. Tout comme cela est toujours possible tant que le nombre d'étapes est fini, il en va de même pour le résultat d'un calcul fini.

Juste comme un point évident supplémentaire - même si votre théorie est incohérente, vous pouvez toujours montrer que la machine s'arrête, même si ce n'est pas le cas, car vous pouvez prouver tout wff dans une théorie incohérente, qu'elle soit ou non en fait vrai.

Philip White
la source

Je suis d'accord avec votre premier point, voir ma réponse ci-dessous. En ce qui concerne votre deuxième point, une théorie incohérente prouvera également la fin d'une MT (en fait non permanente), d'où la restriction à des théories cohérentes.

Super8

Je pense que nous disons la même chose; Je viens de remarquer que vous avez dit "cohérent" dans la question, désolé de l'avoir manqué. Je pense que la réponse de Kaveh couvre toutes les mêmes choses et est de toute façon plus élégamment écrite.

Philip White