Entscheidungsproblem
La domanda se esista una procedura meccanica in grado di decidere quali enunciati matematici discendano dagli assiomi — e il no che inventò per caso il computer.
David Hilbert e Wilhelm Ackermann la formularono nel loro manuale di logica del 1928: esiste una procedura che, per ogni enunciato della logica dei predicati, decida se è universalmente valido? Hilbert si aspettava di sì. Il suo programma mirava a rendere la matematica completa, coerente e decidibile, e il terzo punto era il più concreto dei tre. Un algoritmo che stabilisse i teoremi avrebbe posto fine alla matematica come campo di ricerca, riducendola a girare una manovella.
La risposta arrivò nel 1936 da due direzioni insieme. Alonzo Church usò il calcolo lambda, Alan Turing una macchina immaginaria con un nastro infinito. Entrambi: no. Alcune parti della logica sono decidibili — la logica proposizionale lo è, tramite le tavole di verità — ma la logica dei predicati nel suo insieme no.
Per la storia dell'informatica conta ciò che Turing dovette fare prima. Per dimostrare che nessuna procedura meccanica basta, bisogna prima dire che cos'è una procedura meccanica. La definizione che scrisse — un nastro, una testina, una tabella di stati — divenne la macchina di Turing e, con essa, la prima descrizione precisa di che cosa sia un computer. Il computer nacque come effetto collaterale di un risultato negativo.