Como explicar o problema Entscheidungs em algumas frases às pessoas sem confundir as pessoas

Inicie não usando o termo alemão para um público inglês.

Hilbert's Entscheidungsproblem, declarado em 1928, é o problema de decisão para teorias de primeira ordem: Existe um procedimento eficaz (um algoritmo) que, dado um conjunto de axiomas e uma proposta matemática, decide se é ou não provável a partir dos axiomas?

à luz do teorema de Gödel's completeness teorem, que's equivale a perguntar: Existe um algoritmo para determinar se uma afirmação é verdadeira em todos os modelos de uma teoria?

Na altura em que Hilbert a afirmou, as ideias das teorias de primeira ordem e os seus modelos foram claramente formados, mas a ideia de um algoritmo ainda estava a ser esclarecida.

Em 1936 Church e Turing responderam ao problema geral de forma negativa. Não, não existe tal algoritmo, especificamente nenhum algoritmo para a teoria da aritmética. Eles mostraram que um algoritmo para responder ao problema de decisão geral era impossível. Church usou seu cálculo lambda para fazer isso, enquanto Turing usou suas máquinas teóricas, agora chamadas de máquinas Turing.

No final de 1920's Church inventou o cálculo lambda como modelo para computação. Seu aluno, Turing , desenvolveu o conceito das máquinas Turing em 1936. Turing mostrou que os dois conceitos eram equivalentes em 1937. Veja a pergunta Como o Cálculo Lambda é equivalente à máquina Turing? para saber mais sobre isso.

Embora o problema de decisão geral seja indecidível, para algumas teorias específicas ele é decidível enquanto para outras não é. A aritmética de Presburger, que só pode expressar igualdade e adição, é decidível, como mostrado por Presburger em 1929. A teoria dos verdadeiros campos fechados e a teoria da geometria euclidiana são decidíveis, como mostrado por Tarski em 1949. Também em 1949 Mostowski mostrou que toda a aritmética era' não é necessária para obter undecidablility; aritmética que só pode expressar igualdade, adição e multiplicação não é decidível. A decidibilidade de várias outras teorias também foi determinada.