Existem programas que nunca são interrompidos e não têm prova de rescisão?

Como buracos negros na ciência da computação. Só podemos saber que eles existem, mas quando temos um deles, nunca saberemos que é um deles.

De fato, existem programas como este. Para provar isso, vamos supor ao contrário que, para toda máquina que não para, há uma prova de que ela não para.

Estas provas são strings de comprimento finito, então podemos enumerar todas as provas de comprimento inferior para algum inteiro s .$s$$s$

Em seguida, podemos usar isso para resolver o problema de parada da seguinte forma: Dada uma máquina de Turing e uma entrada x , usamos o seguinte algoritmo:$M$$x$

s := 0
while (True)
    test if machine M halts on input x in s steps
    look at all proofs of length s and see if they prove M doesn't halt on input x
    set s := s + 1

Se parar na entrada x , então ele pára em um número finito de etapas s , então nosso algoritmo termina.$M$$x$$s$

$M$$x$$s$$M$

Assim, temos um algoritmo que decide o problema da parada que sempre termina. Mas sabemos que isso não pode existir, portanto, nossa suposição de que sempre há uma prova de não parar deve ser falsa.

Para um exemplo um pouco mais concreto, vamos supor que a teoria que estamos usando para nossas provas tenha os seguintes recursos (bastante razoáveis, IMO):

1. É consistente ; isto é, não pode provar uma contradição.
2. Seu conjunto de axiomas é recursivamente enumerável.
3. Suas provas podem ser escritas como bits de bits finitos.
4. A questão de saber se uma determinada cadeia codifica uma prova correta e bem formada é algoritmicamente decidível em tempo finito.
5. É expressivo o suficiente para admitir uma prova do segundo teorema da incompletude de Gödel , que diz que ele não pode provar sua própria consistência.

Com essas suposições, o programa a seguir nunca será interrompido, mas não poderá ser provado (dentro do escopo da teoria que estamos usando) para não ser interrompido:

let k := 0;
repeat:
    let k := k + 1;
    let s := binary expansion of k, excluding leading 1 bit;
while s does not encode a proof of a contradiction;
halt.

O detalhe chave aqui é a primeira suposição acima, a saber, que a teoria que estamos usando para nossas provas é consistente. Obviamente, precisamos assumir isso, para que nossas provas valham qualquer coisa, mas o segundo teorema da incompletude de Gödel diz que, para qualquer teoria razoavelmente expressiva e efetivamente axiomatizada, não podemos realmente provar isso (exceto possivelmente em alguma outra teoria, cuja consistência então precisa assumir, etc. etc.).