Por que a VALIDIDADE da lógica de primeira ordem (sem aritmética) é apenas recursivamente enumerável e não recursiva?

A "Complexidade Computacional" de Papadimitriou afirma que VALIDITY, o problema de decidir se uma fórmula de lógica de primeira ordem (sem aritmética) é válida, é recursivamente enumerável. Isso decorre dos teoremas da completude e da solidez, que igualam VALIDITY e THEOREMHOOD, sendo este último o problema de encontrar uma prova para uma fórmula, que anteriormente havia se mostrado recursivamente enumerável.

No entanto, não estou vendo por que VALIDITY também não é recursiva, porque, dada uma fórmula $\phi$ , pode-se executar duas máquinas de Turing para THEOREMHOOD, uma em $\phi$ e o outro em $\neg \phi$ simultaneamente. Como pelo menos um deles é válido, é sempre possível decidir se $\phi$ é válido ou não é válido. o que estou perdendo?

Nota: esta questão se refere à lógica de primeira ordem sem aritmética, portanto o Teorema da Incompletude de Gödel não tem influência aqui.

complexity-theory undecidability first-order-logic user118967
fonte

Relevante (eu acho): en.wikipedia.org/wiki/G%C3%B6del%27s_incompleteness_theorems

Respostas:

No entanto, não estou vendo por que VALIDITY também não é recursiva, porque, dada uma fórmula $\phi$ , pode-se executar duas máquinas de Turing para THEOREMHOOD, uma em $\phi$ e o outro em $\neg \phi$ simultaneamente. Como pelo menos um deles é válido, é sempre possível decidir se $\phi$ é válido ou não é válido. o que estou perdendo?

Isto está errado. Uma fórmula $\phi$ é válido se for válido em todos os modelos.

Não é verdade que pelo menos um dos $\phi$ e $\lnot\phi$ deve ser válido: ambos podem conter alguns modelos, mas não todos.

Exemplo trivial: tome FOL com dois símbolos constantes ${\sf a}, {\sf b}$ e a fórmula $\phi \equiv {\sf a}={\sf b}$ . Então $\phi$ vale em alguns modelos (aqueles que interpretam $\sf a$ e $\sf b$ com o mesmo ponto), mas não todos (um modelo pode mapeá-los para pontos distintos). E, de fato, a FOL não pode provar ${\sf a} = {\sf b}$ nem ${\sf a} \neq {\sf b}$ .

chi
fonte

Obrigado por descobrir o que estava faltando, isso faz sentido. Mas acho que o conjunto de frases válidas (fórmulas sem variáveis livres) é recursivo, pois nesse caso

ϕ

$\phi$ ou

\neg ϕ

$\neg \phi$ Deve ser válido.

user118967

Não.

\forall x, y . x = y

$\forall x, y.\ x=y$ é verdadeiro em modelos com apenas um elemento e falso em modelos com mais de um. Não é válido, não é sua negação. E sem variáveis livres.

chi

Na verdade, pensando um pouco mais sobre isso. Se o conjunto de frases válidas for recursivo, parece que posso mostrar que o conjunto de fórmulas válidas também é recursivo, fazendo o seguinte: dada uma fórmula

ϕ

$\phi$ com constantes

a_{1}, \dots, a_{m}

$a_1,\dots,a_m$ , decida se a sentença

\forall a_{1}, \dots, a_{m} ϕ

$\forall a_1,\dots,a_m \phi$ é válido. Se for,

ϕ

$\phi$ é válido; de outra forma,

ϕ

$\phi$ não é válido. De qualquer forma, posso decidir se está no conjunto de fórmulas válidas. O que estou perdendo agora?

user118967

Considere também

\forall x . p (x) ⟹ q (x)

$\forall x. \ p(x) \implies q(x)$ - só é válido em modelos em que predicados

p

$p$ e

q

$q$ são interpretados adequadamente. No FOL, você tem predicados, símbolos constantes e símbolos de função. Mesmo sem variáveis livres, você pode usar predicados etc. para escrever coisas complexas que podem ou não ser verdadeiras.

chi

Claro que sim. Este último ponto realmente deixa tudo claro. Obrigado.

user118967

Uma sentença de primeira ordem é válida se for verdadeira em todos os modelos possíveis, isto é, se for verdadeira para todas as escolhas do que significam os símbolos de relação, símbolos de função (se houver) e símbolos constantes. Uma sentença é comprovável em algum sistema de prova se esse sistema de prova contiver uma prova da sentença.

Observe que a provabilidade e a validade são dois conceitos separados, mas sua tentativa de mostrar que a validade é recursiva na verdade determina provabilidade, não validade.

A validade e a provabilidade estão ligadas por mais duas noções:

um sistema de prova é som se tudo pode provar é válido, ou seja, só permite que você provar as coisas que são realmente verdade;
um sistema de provas está completo se puder provar tudo o que é válido, ou seja, permite provar todas as coisas verdadeiras.

Portanto, o método proposto seria bom se você estivesse usando um sistema de prova completo e completo: isso significaria que você poderia provar exatamente todas as frases válidas, portanto, decidir a provabilidade seria o mesmo que decidir a validade. Infelizmente, os famosos teoremas da incompletude de Gödel dizem que não existe um sistema de prova completo e sólido para a lógica de primeira ordem.

Portanto, se o seu sistema for sólido (ele só prova coisas verdadeiras), ele está incompleto (não prova todas as coisas verdadeiras). Em particular, existem algumas frases $\varphi$ de modo que nem $\varphi$ nem $\neg\varphi$ possui uma prova em seu sistema, o que significa que sua máquina de Turing não para na entrada $\varphi$ , para que ele não decida realmente nenhum idioma. Como alternativa, se o seu sistema estiver completo (ele prova todas as coisas verdadeiras), ele não é doentio: prova pelo menos uma coisa falsa e, de fato, como falso implica alguma coisa, prova que todas as frases são válidas. Nesse caso, a máquina de Turing que você pensou que iria decidir a validade realmente decide $\Sigma^*$ .

David Richerby
fonte

Seu uso do teorema da incompletude refere-se à lógica de primeira ordem com aritmética, mas minha pergunta se refere à lógica pura de primeira ordem, para a qual existe um sistema de prova completo e sólido, de acordo com o livro que estou lendo, e o Teorema da Completude de Gödel. Então, acho que minha pergunta permanece sem resposta neste momento (vou esclarecê-la).

user118967

O seu sistema de provas é poderoso o suficiente para provar declarações sobre aritmética de primeira ordem; nesse caso, Goedel se aplica, ou não, caso em que obviamente não pode provar todas as verdadeiras declarações de primeira ordem, pois não pode provar aqueles sobre aritmética.

David Richerby

Direita. Mas eu estou falando sobre lógica de primeira ordem sem aritmética, enquanto você fala sobre FOL com aritmética. Para FOL sem aritmética, existe de fato um sistema de prova que é sólido e completo. A totalidade da questão, incluindo a definição de VALIDITY, refere-se ao FOL sem aritmética, portanto, nesse cenário, não há necessidade de provar declarações sobre aritmética para estabelecer a completude.

user118967

De Godel integralidade mostra teorema que lá não existe um sistema dedutivo completa de som e para a lógica de primeira ordem, de tal forma que uma sentença de primeira ordem é uma tautologia se e somente se ele tem uma dedução finito. O teorema da incompletude mostra que pode haver sentenças formalmente independentes dos axiomas de sua teoria: nem a sentença nem sua negação são uma tautologia. No que diz respeito à aritmética, o teorema da incompletude mostra que o esquema de indução do axioma PA de primeira ordem pode falhar, ao contrário do axioma de indução "verdadeiro" (que é uma sentença de segunda ordem).

Mike Battaglia