Il problema della decisione in Turing è la formulazione computazionale della risposta negativa al problema della decisione proposto da Hilbert. Alan Turing, nel 1936, dimostrò che non esiste una procedura algoritmica generale capace di stabilire automaticamente la verità o dimostrabilità di tutte le formule della logica del primo ordine. Lo fece introducendo un modello formale di calcolo — oggi chiamato macchina di Turing — che divenne il riferimento teorico per definire cosa sia un algoritmo.
L’idea centrale del problema della decisione secondo Turing è la seguente: se esistesse una procedura meccanica generale per decidere la verità di ogni enunciato logico, allora dovrebbe esistere una macchina capace di eseguire tale procedura. Turing trasformò quindi il problema logico in un problema di calcolo automatico.
Turing definì un modello astratto di calcolatore composto da: un nastro infinito diviso in celle, una testina di lettura/scrittura, un insieme finito di stati, una tabella di transizione di regole. La macchina legge un simbolo, cambia stato, scrive un simbolo, si sposta sul nastro. Questo modello formalizza il concetto di procedura meccanica o algoritmo.
Qui possiamo introdurre la tesi di Church–Turing: tutto ciò che è calcolabile con un metodo effettivo è calcolabile da una macchina di Turing. Il passaggio chiave è nel problema dell’arresto. Turing dimostrò l’indecidibilità del problema della decisione collegandolo a un altro problema fondamentale: il problema dell’arresto (Halting Problem).
Il problema dell’arresto parte da una domanda: esiste un algoritmo che, dato un programma e un input, stabilisce sempre se il programma terminerà oppure no? Turing dimostrò che una tale procedura non può esistere e che il problema è indecidibile. La dimostrazione usa un ragionamento per contraddizione e auto-riferimento: costruisce una macchina che si comporta in modo opposto alla previsione del decisore, generando un paradosso.
C’è chiaramente un collegamento con il problema della decisione di Hilbert. Turing mostrò che se esistesse una procedura generale per decidere la validità logica allora si potrebbe risolvere anche il problema dell’arresto, ma il problema dell’arresto è indecidibile; quindi, anche il problema della decisione è indecidibile. Perciò, non esiste una macchina universale capace di decidere automaticamente la verità di tutte le formule logiche.
Le conseguenze teoriche del risultato di Turing hanno effetti profondi. Essi riguardano i limiti della computazione: non tutti i problemi formalizzabili sono risolvibili, decidibili e algoritmicamente trattabili. Dal lavoro di Turing derivano la teoria della calcolabilità, quella degli algoritmi, lo studio dei problemi decidibili/indecidibili e i fondamenti dei linguaggi formali.
Dunque, un problema è decidibile se esiste un algoritmo che termina sempre e fornisce risposta corretta sì/no. Il problema della decisione generale è non decidibile.
Turing affrontò il problema della decisione trasformandolo in un problema di calcolo automatico. Introducendo la macchina di Turing dimostrò che non esiste un algoritmo generale capace di decidere la verità di tutte le formule logiche. La prova passa attraverso l’indecidibilità del problema dell’arresto. Questo risultato stabilisce i limiti fondamentali delle macchine di calcolo e segna la nascita della teoria moderna della computazione.