Il problema della decisione di Hilbert chiedeva se esistesse un metodo algoritmico generale per stabilire la verità di ogni formula logica. I lavori di Gödel, Church e Turing hanno dimostrato che tale metodo non esiste: il problema è indecidibile. Questo risultato ha segnato la nascita dell’informatica teorica moderna e ha definito i limiti fondamentali della computazione.
Il problema della decisione di Hilbert (in tedesco Entscheidungsproblem) è uno dei problemi fondamentali della logica matematica e dell’informatica teorica del XX secolo. Nasce all’interno del programma di ricerca di David Hilbert, che mirava a fondare la matematica su basi formali complete, coerenti e meccanicamente verificabili. Hilbert si chiese se fosse possibile trovare una procedura generale e meccanica capace di stabilire, per qualunque enunciato della logica matematica, se esso fosse vero oppure falso. In termini moderni: esiste un algoritmo che, data una formula logica, possa sempre decidere in modo automatico se essa è dimostrabile?
All’inizio del Novecento Hilbert propose un vasto programma di formalizzazione della matematica. L’idea centrale era che ogni teoria matematica potesse essere espressa con un linguaggio formale, che le dimostrazioni fossero sequenze di regole simboliche e che la correttezza potesse essere verificata in modo puramente meccanico.
Esiste un metodo finito, generale e automatico che permetta di decidere la validità di qualsiasi formula della logica del primo ordine? Questa “procedura di decisione” dovrebbe funzionare sempre e terminare in tempo finito con una risposta sì/no.
Qual è il significato informatico del problema? In termini di informatica teorica, il problema della decisione equivale a chiedere se esiste un algoritmo universale che prende in input una formula logica e stabilisce sempre se è logicamente valida? È una domanda sulla decidibilità dei problemi formali e anticipa direttamente i concetti di algoritmo, calcolabilità, macchina astratta e limite computazionale.
Negli anni Trenta il problema ricevette una risposta definitiva: no, una tale procedura generale non esiste. I risultati chiave furono quelli di Kurt Gödel (1931) che con i teoremi di incompletezza mostrò che esistono proposizioni vere, ma non dimostrabili, che nessun sistema formale sufficientemente potente può essere completo e coerente.
Non risolve direttamente l’Entscheidungsproblem, ma ne mina le basi. Abbiamo quindi Alonzo Church (1936) che dimostrò l’indecidibilità usando il lambda-calcolo: non esiste un algoritmo generale di decisione per la logica del primo ordine.
Alan Turing (1936) arrivò allo stesso risultato con un modello diverso. Con la macchina di Turing, collegando il problema alla non risolvibilità del problema dell’arresto (halting problem) mostrò che: non esiste una macchina che possa decidere universalmente la validità logica e quindi il problema della decisione è indecidibile.
Le conseguenze teoriche della non risolvibilità del problema della decisione ha conseguenze fondamentali: nasce la teoria della calcolabilità che definisce cosa può essere calcolato e cosa non può essere calcolato. Non tutti i problemi formalizzabili sono decidibili e/o risolvibili da procedure automatiche.
I fondamenti dell’informatica teorica portano allo sviluppo di: macchine di Turing, teoria degli algoritmi, complessità computazionale e linguaggi formali.