Come spiegare il problema dell'Entscheidungs in poche frasi alla gente senza confondere le persone

Partiamo dal non usare il termine tedesco ad un pubblico inglese.

Hilbert's Entscheidungsproblem, enunciato nel 1928, è il problema di decisione per le teorie del primo ordine: Esiste una procedura efficace (un algoritmo) che, dato un insieme di assiomi e una proposizione matematica, decida se è o non è dimostrabile dagli assiomi?

Alla luce del teorema di completezza di Gödel, ciò equivale a chiedere: Esiste un algoritmo per determinare se un'affermazione è vera in tutti i modelli di una teoria?

Al tempo in cui Hilbert lo affermava, le idee delle teorie del primo ordine e dei loro modelli erano chiaramente formate, ma l'idea di un algoritmo era ancora in fase di chiarimento.

Nel 1936 Church e Turing risposero al problema generale in modo negativo. No, non esiste un tale algoritmo, in particolare nessun algoritmo per la teoria dell'aritmetica. Hanno dimostrato che un algoritmo per rispondere al problema generale della decisione era impossibile. Church ha usato il suo calcolo lambda per farlo, mentre Turing ha usato le sue macchine teoriche, ora chiamate macchine di Turing.

Nella fine del 1920's Church ha proposto il calcolo lambda come modello di calcolo. Il suo studente, Turing, sviluppò il concetto di macchina di Turing nel 1936. Turing dimostrò che i due concetti erano equivalenti nel 1937. Vedere la domanda Come il calcolo lambda è equivalente alla macchina di Turing? per saperne di più.

Anche se il problema generale della decisione è indecidibile, per alcune teorie specifiche è decidibile mentre per altre no. L'aritmetica di Presburger, che può esprimere solo uguaglianza e addizione, è decidibile come dimostrato da Presburger nel 1929. La teoria dei campi reali chiusi e la teoria della geometria euclidea sono decidibili come dimostrato da Tarski nel 1949. Sempre nel 1949 Mostowski mostrò che tutta l'aritmetica non era necessaria per ottenere l'indecidibilità; l'aritmetica che può esprimere solo uguaglianza, addizione e moltiplicazione non è decidibile. È stata determinata anche la decidibilità di diverse altre teorie.