Entscheidungsproblem

Na área da matemática e na ciência da computação, o Entscheidungsproblem (alemão para "problema de decisão") é um desafio lógico colocado pelos matemáticos alemães David Hilbert e Wilhelm Ackermann em 1928. Ele pede um algoritmo que considere uma declaração inserida e responda "sim" ou "não" de acordo com se ela é universalmente válida, ou seja, válida em todas as estruturas.

Teorema da completude

Pelo teorema da completude da lógica de primeira ordem, uma afirmação é universalmente válida se e somente se ela pode ser deduzida usando regras lógicas e axiomas, então o Entscheidungsproblem também pode ser visto como pedindo um algoritmo para decidir se uma determinada afirmação é demonstrável usando as regras da lógica.

Em 1936, Alonzo Church e Alan Turing publicaram artigos independentes mostrando que uma solução geral para o Entscheidungsproblem é impossível, assumindo que a noção intuitiva de "efetivamente calculável" é capturada pelas funções computáveis por uma máquina de Turing (ou equivalentemente, por aquelas expressáveis no cálculo lambda). Essa suposição é agora conhecida como tese de Church-Turing.

História

A origem do Entscheidungsproblem remonta a Gottfried Leibniz, que no século XVII, depois de ter construído uma máquina de calcular mecânica bem-sucedida, sonhou em construir uma máquina que pudesse manipular símbolos para determinar os valores de verdade das afirmações matemáticas. Ele percebeu que o primeiro passo teria que ser uma linguagem formal limpa, e grande parte de seu trabalho subsequente foi direcionado para esse objetivo. Em 1928, David Hilbert e Wilhelm Ackermann colocaram a questão na forma descrita acima.

Na continuação de seu "programa", Hilbert fez três perguntas em uma conferência internacional em 1928, a terceira das quais ficou conhecida como "Entscheidungsproblem de Hilbert". Em 1929, Moses Schönfinkel publicou um artigo sobre casos especiais do problema da decisão, que foi preparado por Paul Bernays.

Ainda em 1930, Hilbert acreditava que não haveria um problema insolúvel.

Resposta negativa

Antes que a pergunta pudesse ser respondida, a noção de "algoritmo" teve que ser formalmente definida. Isso foi feito por Alonzo Church em 1935 com o conceito de "calculabilidade efetiva" com base em seu cálculo λ, e por Alan Turing no ano seguinte com seu conceito de máquinas de Turing. Turing reconheceu imediatamente que esses são modelos equivalentes de computação.

Uma resposta negativa ao Entscheidungsproblem foi então dada por Alonzo Church em 1935-36 (teorema de Church) e independentemente logo depois por Alan Turing em 1936 (prova de Turing). Church provou que não existe uma função computável que decida, para duas expressões de cálculo λ dadas, se elas são equivalentes ou não. Ele se baseou fortemente em trabalhos anteriores de Stephen Kleene. Turing reduziu a questão da existência de um "algoritmo" ou "método geral" capaz de resolver o Entscheidungsproblem à questão da existência de um "método geral" que decide se uma dada máquina de Turing pára ou não (o problema da parada). Se 'algoritmo' é entendido como significando um método que pode ser representado como uma máquina de Turing, e com a resposta à última pergunta negativa (em geral), a questão sobre a existência de um algoritmo para o Entscheidungsproblem também deve ser negativa (em geral). Em seu artigo de 1936, Turing diz: "Correspondendo a cada máquina de computação 'it', construímos uma fórmula 'Un(it)' e mostramos que, se existe um método geral para determinar se 'Un(it)' é demonstrável, então existe um método geral para determinar se 'it' imprime 0".

O trabalho de Church e Turing foi fortemente influenciado pelo trabalho anterior de Kurt Gödel em seu teorema da incompletude, especialmente pelo método de atribuição de números (uma numeração de Gödel) a fórmulas lógicas, a fim de reduzir a lógica à aritmética.

O Entscheidungsproblem está relacionado ao décimo problema de Hilbert, que pede um algoritmo para decidir se as equações diofantinas têm uma solução. A inexistência de tal algoritmo, estabelecido pelo trabalho de Yuri Matiyasevich, Julia Robinson, Martin Davis e Hilary Putnam, com a peça final da prova em 1970, também implica uma resposta negativa ao Entscheidungsproblem.

Generalizações

Usando o teorema da dedução, o Entscheidungsproblem engloba o problema mais geral de decidir se uma dada sentença de primeira ordem é implicada por um dado conjunto finito de sentenças, mas a validade em teorias de primeira ordem com infinitos axiomas não pode ser diretamente reduzida ao Entscheidungsproblem. Esses problemas de decisão mais gerais são de interesse prático. Algumas teorias de primeira ordem são decidíveis algoritmicamente; exemplos disso incluem aritmética de Presburger, campos fechados reais e sistemas de tipos estáticos de muitas linguagens de programação. Por outro lado, a teoria de primeira ordem dos números naturais com adição e multiplicação expressa pelos axiomas de Peano não pode ser decidida com um algoritmo.

Fragmentos

Por padrão, as citações na seção são de Pratt-Hartmann (2023).

O clássico Entscheidungsproblem pergunta que, dada uma fórmula de primeira ordem, se ela é verdadeira em todos os modelos. O problema finitário pergunta se é verdade em todos os modelos finitos. O teorema de Trakhtenbrot mostra que isso também é indecidível.

Algumas anotações: ${\rm {{Sat}(\Phi )}}$ significa o problema de decidir se existe um modelo para um conjunto de fórmulas lógicas $\Phi$. ${\rm {{FinSat}(\Phi )}}$ é o mesmo problema, mas para modelos finitos. O problema ${\rm {Sat}}$ para um fragmento lógico é chamado decidível se existe um programa que pode decidir, para cada conjunto finito de fórmulas lógicas no fragmento, se ${\rm {{Sat}(\Phi )}}$ ou não.

Aristotélico e relacional

A lógica aristotélica considera 4 tipos de sentenças: "Todos os p são q", "Todos os p não são q", "Alguns p são q", "Alguns p não são q". Podemos formalizar esses tipos de frases como um fragmento da lógica de primeira ordem:$$\forall x,p(x)\to \pm q(x),\quad \exists x,p(x)\wedge \pm q(x)$$Onde $p,q$ são predicados atômicos, e $+q:=q,\;-q:=\neg q$. Dado um conjunto finito de fórmulas lógicas aristotélicas, é NLOGSPACE-completo decidir seu ${\rm {Sat}}$. Também é NLOGSPACE-completo para decidir ${\rm {Sat}}$ para uma ligeira extensão (Teorema 2:7):$$\forall x,\pm p(x)\to \pm q(x),\quad \exists x,\pm p(x)\wedge \pm q(x)$$A lógica relacional estende a lógica aristotélica ao permitir um predicado relacional. Por exemplo, a frase em inglês "everybody loves somebody" (todo mundo ama alguém) pode ser escrito como ${\textstyle \forall x,{\rm {{body}(x),\exists y,{\rm {{body}(y)\wedge {\rm {{love}(x,y)}}}}}}}$. Geralmente, temos oito tipos de sentenças:$${\begin{aligned}\forall x,p(x)\to (\forall y,q(x)\to \pm r(x,y)),&\quad \forall x,p(x)\to (\exists y,q(x)\wedge \pm r(x,y))\\\exists x,p(x)\wedge (\forall y,q(x)\to \pm r(x,y)),&\quad \exists x,p(x)\wedge (\exists y,q(x)\wedge \pm r(x,y))\end{aligned}}$$É NLOGSPACE-completo para decidir seu ${\rm {Sat}}$ (Teorema 2:15). A lógica relacional pode ser estendida para 32 tipos de sentenças, permitindo $\pm p,\pm q$, mas esta extensão é EXPTIME-completa (Teorema 2.24).

Aridade

O fragmento lógico de primeira ordem em que os únicos nomes de variáveis são $x,y$ é NEXPTIME-completo (Teorema 3.18). Com $x,y,z$, é RE-completo decidir sua ${\rm {Sat}}$, e co-RE-completar para decidir ${\rm {FinSat}}$ (Teorema 3:15), portanto, indecídivel.

O cálculo de predicados monádicos é o fragmento em que cada fórmula contém apenas predicados 1-ários e nenhum símbolo de função. Seu ${\rm {Sat}}$ é NEXPTIME-completo (Teorema 3.22).

Prefixo do quantificador

Qualquer fórmula de primeira ordem tem uma forma normal prenex. Para cada prefixo quantificador possível para a forma normal prenex, temos um fragmento de lógica de primeira ordem. Por exemplo, a classe Bernays-Schönfinkel, $[\exists ^{*}\forall ^{*}]_{=}$, é a classe de fórmulas de primeira ordem com prefixo quantificador $\exists \cdots \exists \forall \cdots \forall$, símbolos de igualdade e símbolos sem função.

Por exemplo, o artigo de Turing de 1936 (p. 263) observou que, uma vez que o problema da parada para cada máquina de Turing é equivalente a uma fórmula lógica de primeira ordem da forma $\forall \exists \forall \exists ^{6}$, o problema ${\rm {{Sat}(\forall \exists \forall \exists ^{6})}}$ é indecídivel.

Os limites precisos são conhecidos, nitidamente:

• ${\rm {{Sat}(\forall \exists \forall )}}$ and ${\rm {{Sat}([\forall \exists \forall ]_{=})}}$ são co-RE-completos, e os problemas ${\rm {FinSat}}$ são RE-completos (Teorema 5:2)
• Mesmo para $\forall ^{3}\exists$ (Teorema 5:3).
• $\exists ^{*}\forall ^{2}\exists ^{*}$ é decídivel, provado independentemente por Gödel, Schütte e Kalmár.
• $[\forall ^{2}\exists ]_{=}$ é indecídivel.
• Para qualquer $n\geq 0$, tanto ${\rm {{Sat}(\exists ^{n}\forall ^{*})}}$ quanto ${\rm {{Sat}([\exists ^{n}\forall ^{*}]_{=})}}$ são NEXPTIME-completos (Teorema 5.1).
  • Isso implica que ${\rm {{Sat}([\exists ^{*}\forall ^{*}]_{=})}}$ é decídivel, um resultado primeiramente publicado por Bernays e Schönfinkel.
• Para qualquer $n\geq 0,m\geq 2$, ${\rm {{Sat}(\exists ^{n}\forall \exists ^{m})}}$ é EXPTIME-completo (Seção 5. 4. 1.).
• Para qualquer $n\geq 0$, ${\rm {{Sat}([\exists ^{n}\forall \exists ^{*}]_{=})}}$ é NEXPTIME-completo (Seção 5. 4. 2.).
  • Isso implica que ${\rm {{Sat}(\exists ^{*}\forall ^{*}\exists ^{*})}}$é decídivel, um resultado primeiramente publicado por Ackermann.
• Para qualquer $n\geq 0$, ${\rm {{Sat}(\exists ^{n}\forall \exists )}}$ e ${\rm {{Sat}([\exists ^{n}\forall \exists ]_{=})}}$ são PSPACE-completo (Seção 5. 4. 3.)

Börger et al. (2001) descreve o nível de complexidade computacional para cada fragmento possível com todas as combinações possíveis de prefixo quantificador, aridade funcional, aridade de predicado e igualdade / não igualdade.

Procedimentos práticos de decisão

Ter procedimentos práticos de decisão para classes de fórmulas lógicas é de considerável interesse para verificação de programas e verificação de circuitos. Fórmulas lógicas booleanas puras são geralmente decididas usando técnicas de resolução de SAT baseadas no algoritmo DPLL.

Para problemas de decisão mais gerais de teorias de primeira ordem, fórmulas conjuntivas sobre aritmética linear real ou racional podem ser decididas usando o algoritmo simplex, fórmulas em aritmética inteira linear (aritmética de Presburger) podem ser decididas usando o algoritmo de Cooper ou o teste Omega de William Pugh. Fórmulas com negações, conjunções e disjunções combinam as dificuldades do teste de satisfatibilidade com a decisão de conjunções; eles são geralmente decididos hoje em dia usando técnicas de resolução SMT, que combinam a resolução de SAT com procedimentos de decisão para conjunções e técnicas de propagação. A aritmética polinomial real, também conhecida como teoria dos corpos fechados reais, é decidível; este é o teorema de Tarski-Seidenberg, que foi implementado em computadores usando a decomposição algébrica cilíndrica.

Referências

• Alonzo Church, "An unsolvable problem of elementary number theory", American Journal of Mathematics, 58 (1936), pp 345 - 363
• Alonzo Church, "A note on the Entscheidungsproblem", Journal of Symbolic Logic, 1 (1936), pp 40 - 41.
• Alan Turing, "On computable numbers, with an application to the Entscheidungsproblem", Proceedings of the London Mathematical Society, Series 2, 42 (1936), pp 230 - 265. Online version. Errata appeared in Series 2, 43 (1937), pp 544 - 546.
• Martin Davis, "The Undecidable, Basic Papers on Undecidable Propositions, Unsolvable Problems And Computable Functions", Raven Press, New York, 1965. Turing's paper is #3 in this volume. Papers include those by Godel, Church, Rosser, Kleene, and Post.
• Andrew Hodges, Alan Turing: The Enigma, Simon and Schuster, New York, 1983. Allen M. Turing's biography. Cf Chapter "The Spirit of Truth" for a history leading to, and a discussion of, his proof.
• Toulmin, Stephen, "Fall of a Genius", a book review of "Alan Turing: The Enigma by Andrew Hodges", in The New York Review of Books, January 19, 1984, p. 3ff.
• Alfred North Whitehead and Bertrand Russell, Principia Mathematica to *56, Cambridge at the University Press, 1962. Re: the problem of paradoxes, the authors discuss the problem of a set not be an object in any of its "determining functions", in particular "Introduction, Chap. 1 p. 24 "...difficulties which arise in formal logic", and Chap. 2.I. "The Vicious-Circle Principle" p.37ff, and Chap. 2.VIII. "The Contradictions" p.60 ff.