Entscheidungsproblem

O Entscheidungsproblem (termo alemão para "problema de decisão") é um problema da lógica simbólica que consiste em achar um algoritmo genérico para determinar se um dado enunciado da lógica de primeira ordem pode ser provado. Em 1936-37, trabalhando independentemente, Alonzo Church e Alan Turing mostraram que é impossível decidir algoritmicamente se um enunciado na lógica de primeira ordem é verdadeiro ou falso.

A questão retoma a Gottfried Leibniz, que no século XVII, depois de construir uma máquina de calcular mecânica, sonhou em construir uma máquina que pudesse manipular símbolos a fim de determinar os valores de verdade dos enunciados matemáticos. Ele percebeu que o primeiro passo teria que ser uma linguagem formal precisa, e muito do seu trabalho subsequente foi nesse sentido. Em 1928, David Hilbert e Wilhelm Ackermann propuseram tal questão da forma mostrada logo abaixo.

Um enunciado de primeira ordem é chamado "universalmente válido" ou "logicamente válido" se segue dos axiomas do cálculo de predicados de primeira ordem. O Teorema da completude de Gödel indica que um enunciado é universalmente válido se, e somente se, é verdadeiro em toda interpretação num modelo.

Na continuação do seu "programa" com o qual ele desafiou a comunidade matemática em 1900, na Conferência Internacional de 1928 David Hilber fez três questionamentos, ficando o terceiro conhecido como "O problema de decisão de Hilbert" ("Hilbert's Entscheidungsproblem") [Hodges p.91]. Em meados de 1930 ele acreditava que não existiria um problema insolúvel (Hodges p.92, citando Hilbert).

Antes que a questão pudesse ser respondida, a noção de "algoritmo" tinha que ser formalmente definida. Isso foi feito por Alonzo Church em 1936 com o conceito de "calculabilidade efetiva", baseada no seu cálculo λ , e por Alan Turing, no mesmo ano, com o seu conceito de Máquinas de Turing. As duas abordagens são equivalentes, uma instância da Tese de Church-Turing.

A resposta negativa ao Entscheidungsproblem foi dada por Alonzo Church em 1936 e, logo em seguida, de forma independente, por Alan Turing, também em 1936. Church provou que não existe algoritmo (função computável) que decide para duas expressões do cálculo λ se elas são equivalentes ou não. Ele se baseou no trabalho anterior de Stephen Kleene. Turing reduziu o problema da parada para as Máquinas de Turing ao Entscheidungsproblem, e o seu artigo é considerado muito mais influente do que o de Church. O trabalho de ambos autores foi muito influenciado por Kurt Gödel e o seu teorema da completude, principalmente pela enumeração de Gödel para fórmulas lógicas a fim de reduzir a lógica a aritmética.

A seguir o argumento de Turing. Suponha que temos um algoritmo de decisão genérico para a lógica de primeira ordem. A questão se uma determinada Máquina de Turing pára ou não pode ser formulada como um enunciado de primeira ordem, o qual seria suscetível ao algoritmo de decisão. Mas Turing provou anteriormente que nenhum algoritmo genérico pode decidir se uma determinada Máquina de Turing pára.

O Entscheidungsproblem é relacionado ao "Décimo problema de Hilbert", que pede a um algoritmo decidir se uma equação diofantina tem solução. A não-existência de tal algoritmo (provado por Yuri Matiyasevich em 1970) implica numa resposta negativa ao Entscheidungsproblem. (veja Teorema de Matiyasevich)

É importante perceber que se nós nos restringirmos a uma teoria de primeira ordem específica com objetos específicos constantes, funções constantes, predicados constantes e axiomas subjetivos, a verdade dos enunciados nessa teoria pode muito bem ser algoritmicamente decidível. Exemplos disso incluem Aritmética de Presburger, campos reais fechados e tipos de variáveis em linguagens de programação.

Entretanto, a teoria de primeira ordem dos números naturais expressa nos axiomas de Peano não pode ser decidida por tal algoritmo. Isso segue do argumento de Turing mostrado acima.

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.