Máquinas de Turing cuja terminação é improvável?

Tenho uma pergunta ingênua: existe uma máquina de Turing cujo término é verdadeiro, mas não pode ser provado por nenhuma teoria natural, consistente e finamente axiomatizável? Peço uma mera prova de existência e não um exemplo específico.

Isso pode ter alguma conexão com a análise ordinal . De fato, para uma máquina de Turing , podemos definir como o menos ordinal de uma teoria consistente que comprove sua terminação (ou o menor desses ordinais). Então eu acho que seria equivalente perguntar se existe tal que ? $M$ $O(M)$ $M$ $O(M) \geq \omega_1^{CK}$

turing-machines proof-theory halting-problem Super8
fonte

A quantificação não deveria funcionar ao contrário? Simplesmente adicionar TM TM para como um axioma seria consistente para qualquer X que realmente parar em todas as entradas (e finito se você fizer isso apenas para a TM em questão). Com os quantificadores invertidos, que tal uma TM que interrompe se a entrada não é uma prova de consistência para o sistema axiomático e, caso contrário, entra em um loop infinito.

Yonatan N

Sua sugestão é interessante, obrigado. Eu estava ciente de sua preocupação ao formular a pergunta, por isso acrescentei "natural" nos requisitos. Obviamente, o problema é se podemos dar uma definição formal de "naturalidade" que excluiria essa construção artificial.

8 em

acho que a resposta é não, porque, se parar, basta rodar a máquina e ela irá parar em um número finito de etapas, e isso é uma prova, e esse fato pode ser convertido em qualquer sistema de prova razoavelmente poderoso. por outro lado, pense que é possível codificar / converter / traduzir o thm improvável de godel em uma máquina sem interrupção para a qual a não interrupção é improvável. esta questão é semelhante, há uma TM que pára em todas as entradas, mas a propriedade não é demonstrável cs.se

vzn

Você pode construir uma máquina de Turing que calcula a sequência de Goodstein da entrada e pára quando atinge A parada de não pode ser provada na aritmética do Peano; isto é, o teorema de Goodstein não é comprovável usando os axiomas aritméticos de Peano. Veja Laurie Kirby, Jeff Paris, resultados de independência acessíveis para aritmética Peano (1982)

M

$M$

G (n)

$G(n)$

n

$n$

0

$0$

M

$M$

Marzio De Biasi

Obrigado, eu não conhecia essas entradas. O que estou pedindo é mais forte, porém, gostaria de provar a improbabilidade de qualquer teoria razoável (em vez de uma teoria específica como a PA). Não tenho certeza se a pergunta tem uma resposta definitiva.

8 em

Respostas:

Rescisão de uma máquina de Turing (em uma entrada fixa) é um frase e todas as teorias aritméticas habitual de primeira ordem estão completas para frases, isto é tudo verdade declarações são demonstráveis nessas teorias. $\Sigma^0_1$ $\Sigma^0_1$ $\Sigma^0_1$

Se você olhar para a totalidade no lugar de parada , ou seja, um TM paradas em todas as entradas, então isso é um frase -completo e por qualquer teoria consistente computably axiomatizable que é forte o suficiente (por exemplo, estende-se dizer de Robinson teoria), há uma TM cuja totalidade não pode ser provada nessa teoria. $\Pi^0_2$ $Q$

Kaveh
fonte

Sim, eu estava procurando por totalidade, pois é claro que o problema é trivial para uma entrada fixa. Pensarei na sua afirmação e como provar isso, mas neste momento não vejo como a consideração de teorias "computacionalmente axiomatizáveis" exclui o problema mencionado acima. Além disso, na sua afirmação, a MT depende da teoria considerada, podemos obter minha afirmação mais forte por algum tipo de diagonalização?

Super8

Aqui está uma maneira fácil: o conjunto de funções computáveis comprovadamente totais de tal teoria é ce, o conjunto de funções computáveis totais não é ce ou, alternativamente, você pode diagonalizar em relação às funções comprovadamente totais da teoria.

Kaveh

Pensando bem, sugiro considerar uma restrição do problema da seguinte maneira. Dado um sistema de notação ordinal

representando um

ordinal , podemos definir uma "teoria elementar" correspondente

que permite indução transfinita até

. Dado um TM

, definiríamos

como o menor

ordinal, de modo que a terminação de

possa ser provada por uma teoria

σ

$\sigma$

α

$\alpha$

T (α, σ)

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

α

$\alpha$

M

$M$

O (M)

$O(M)$

α

$\alpha$

M

$M$

T (α, σ)

$\mathcal{T}(\alpha,\sigma)$ (ou seja, o sistema de notação pode ser escolhido livremente). Essa definição faz sentido?

Super8

@ Super8, não tenho certeza. Geralmente, a associação de ordinais a teorias não é canônica; existem várias maneiras de associar isso. Você pode começar com uma teoria fraca como a PRA e adicionar indução sobre ordinais computáveis com boas seqüências fundamentais, etc. mas não sei ao certo por que você gostaria de fazê-lo.

Kaveh

Ok, eu não tinha percebido o problema, vou tentar encontrar uma definição melhor por conta própria.

Super8

Não sou especialista em lógica, mas acredito que a resposta é não . Se a máquina de Turing parar e o sistema for forte o suficiente, você poderá escrever o histórico completo de computação da máquina de Turing em sua entrada. Quando se verifica que o resultado da computação é uma sequência final de transições, pode-se ver que a máquina pára. Independentemente de como você formaliza as máquinas de Turing em sua teoria, você deve ser capaz de mostrar em qualquer teoria razoável que uma máquina que para de fato pára. Por analogia, pense em tentar provar que uma soma finita é igual ao que é igual; por exemplo, prove que 5 + 2 + 3 + 19 + 7 + 6 = 42 ou 5 + 5 + 5 = 15. Assim como isso sempre é possível, desde que o número de etapas seja finito, o mesmo ocorre com o resultado de um cálculo finito.

Apenas como um ponto óbvio adicional - mesmo que sua teoria seja inconsistente, você ainda pode mostrar que a máquina pára, na verdade mesmo que não seja, pois você pode provar qualquer problema em uma teoria inconsistente, independentemente de ser ou não realmente verdade.

Philip White
fonte

Concordo com o seu primeiro ponto, veja a minha resposta abaixo. Com relação ao seu segundo ponto, uma teoria inconsistente também provará o término de uma MT (na verdade não-terminativa), daí a restrição a teorias consistentes.

Super8

Eu acho que estamos dizendo a mesma coisa; Acabei de perceber que você disse "consistente" na pergunta, desculpe por ter perdido isso. Acho que a resposta de Kaveh cobre todas as mesmas coisas e, de qualquer maneira, é escrita com mais elegância.

Philip White