Entscheidungsproblem
De Wikipedia, a enciclopédia encyclopedia
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.
Este artigo ou secção contém uma lista de referências no fim do texto, mas as suas fontes não são claras porque não são citadas no corpo do artigo, o que compromete a confiabilidade das informações. (Outubro de 2016) |
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.