Entscheidungsproblem

Da Wikipedia, l'enciclopedia libera.

L'Entscheidungsproblem è il secondo dei Problemi di Hilbert, la lista di problemi aperti in matematica stilata dal matematico tedesco nel 1900.

[modifica] Il problema della decisione

Nell'agosto del 1900, il matematico tedesco David Hilbert partecipò al Congresso internazionale di matematica di Parigi e, nel suo intervento, presentò una lista di problemi che la matematica era chiamata a risolvere. La lista contava ventitré problemi che apparivano, all'attuale stato della scienza matematica, irrisolti. Il secondo di questi problemi era appunto l'Entscheidungsproblem (letteralmente "problema della decisione"): dimostrare cioè, come si era fatto per gli assiomi della geometria euclidea, che gli assiomi dell'aritmetica dei numeri reali erano anch'essi coerenti. Questa questione coinvolgeva direttamente i fondamenti stessi della matematica. Fino ad allora le prove di non-contraddittorietà erano sempre state prove di coerenza relativa, cioè avevano semplicemente ridotto la coerenza di un certo sistema di assiomi a quella di un altro. Hilbert si rese conto che con l'aritmetica non si poteva più fare riferimento a un altro sistema di assiomi, si era giunti cioè al fondamento logico della matematica e a quel punto bisognava affrontare il problema in termini del tutto generali, non più relativi.

[modifica] Il contributo di Gödel

Il lavoro di Gödel dimostrò di fatto l'impossibilità del programma di Hilbert. Con il suo teorema di incompletezza, Gödel dimostrava l'esistenza di una proposizione indecidibile all'interno di un sistema logico formale. È importante sottolineare che questa indecidibilità è soltanto interna al sistema. Da un punto di vista esterno, la proposizione è chiaramente vera. Gödel dimostra quindi che è impossibile provare la coerenza di sistemi formali, come i Principia Mathematica, al loro interno. Il programma di Hilbert, almeno nella forma originaria, era morto.

Dopo il lavoro di Gödel era difficile pensare che potesse esistere un algoritmo che fornisse regole esplicite per dimostrare, all'interno di un sistema formale e in tutti i casi, che da un insieme di premesse si potesse derivare tramite la logica del primo ordine un'ipotetica conclusione. Alan Turing, riducendo il concetto di calcolabilità effettiva a quello di procedura meccanica, con la sua Macchina di Turing, (vedi Tesi di Church-Turing) mostrò che un simile algoritmo in effetti non esisteva.