In logica matematica, i teoremi di incompletezza di Gödel sono due famosi teoremi dimostrati da Kurt Gödel nel settembre del 1930. Essi fanno parte dei teoremi limitativi, che precisano le proprietà che i sistemi formali non possono avere.

Storia Gödel enunciò il suo primo teorema di incompletezza durante una tavola rotonda a margine della Seconda Conferenza sull'epistemologia delle scienze esatte di Königsberg. John von Neumann, presente alla discussione, riuscì a dimostrare il teorema per conto suo verso la fine del 1930 e, inoltre, fornì una dimostrazione del secondo teorema di incompletezza, che annunciò a Gödel in una lettera datata 20 novembre 1930. Gödel aveva, nel frattempo, a sua volta ottenuto una dimostrazione del secondo teorema di incompletezza e lo incluse nel manoscritto ricevuto dalla rivista Monatshefte für Mathematik il 17 novembre 1930.John W. Dawson, Jr., Logical Dilemmas: The Life and Work of Kurt Gödel, p. 70, A. K. Peters, Wellesley Mass, 1997.

Primo teorema di incompletezza

Sia P una formalizzazione dell'aritmetica di Peano.

Con il teorema di incompletezza di Gödel si è dimostrato che tale teoria risulta completa per i soli assiomi logici, ossia: per ogni formula "R", esiste una formula ad essa corrispondente "r" tale che:

se sussiste ; se non sussiste .

Il Primo Teorema di incompletezza di Gödel dice che:

In ogni teoria matematica T sufficientemente espressiva da contenere l'aritmetica, esiste una formula tale che, se T è coerente, allora né né la sua negazione sono dimostrabili in T.

Con qualche semplificazione, il primo teorema afferma che:

In ogni formalizzazione coerente della matematica che sia sufficientemente potente da poter assiomatizzare la teoria elementare dei numeri naturali — vale a dire, sufficientemente potente da definire la struttura dei numeri naturali dotati delle operazioni di somma e prodotto — è possibile costruire una proposizione sintatticamente corretta che non può essere né dimostrata né confutata all'interno dello stesso sistema.L'idea di fondo della dimostrazione può essere così riassunta: Supponiamo esista una proposizione G la cui interpretazione standard sia "G non è dimostrabile in P". Se , cioè se G fosse dimostrabile in P, G risulterebbe falsa. Ma per il teorema di completezza di Gödel, ogni proposizione dimostrabile in P risulta vera, dunque G non può essere dimostrabile in P e quindi è vera. Quindi G risulta falsa e, per lo stesso motivo, non può essere dimostrabile in P. Pertanto se esiste una proposizione il cui contenuto è "io non sono dimostrabile in P", tale proposizione risulterà vera ma non dimostrabile.

Intuitivamente, la dimostrazione del primo teorema ruota attorno alla possibilità di definire una formula logica che neghi la propria dimostrabilità: si prova quindi che, affinché T sia coerente, né né possono essere dimostrabili. È dunque cruciale che T consenta di codificare formule autoreferenziali, che parlino cioè di se stesse: questa richiesta è garantita dal fatto che T è espressiva almeno quanto l'aritmetica o più in generale che T sia in grado di rappresentare tutte le funzioni ricorsive primitive.

Merito di Gödel fu dunque l'aver esibito tale proposizione e la vera potenza di tale teorema è che vale "per ogni teoria affine", cioè per qualsiasi teoria formalizzata, forte quanto l'aritmetica elementare. In particolare Gödel dimostrò che l'aritmetica stessa risulta incompleta: vi sono dunque realtà vere ma non dimostrabili.

Questo teorema esprime uno dei limiti più discussi della matematica ed è uno dei più fraintesi. È un teorema proprio della logica formale e fuori da questo contesto si presta a interpretazioni erronee. Ci sono molti enunciati in apparenza simili al primo teorema di incompletezza di Gödel, ma che non sono veri. Essi saranno presentati più avanti nella sezione Fraintendimenti sul teorema di incompletezza di Gödel.

Una costruzione assiomatica non può soddisfare al tempo stesso le proprietà di coerenza e completezza. Se dagli assiomi viene dedotta l'intera aritmetica, essi portano a una contraddizione; se i teoremi derivati non sono contraddittori, esiste almeno un teorema non dimostrabile a partire da quei soli assiomi, un caso indecidibile di cui non si può dire se sia vero o falso. Insistendo a postulare con un nuovo assioma la verità di un teorema indecidibile, il problema viene semplicemente spostato e la costruzione ripropone un secondo caso di indecisione. Il caso di indecisione è detto ipotesi e, come l'assioma, non è dimostrabile, ma diversamente da questo, può essere accettato o meno; la distinzione fra assioma e ipotesi dipende dal fatto che la non-accettazione di un assioma impone subito di arrestare l'analisi, mentre l'accettazione è feconda di conseguenze e teoremi. Invece, l'accettazione o meno di un'ipotesi può essere feconda di conseguenze.

Secondo teorema di incompletezza

Il secondo teorema di incompletezza di Gödel si dimostra formalizzando una parte della dimostrazione del primo all'interno del sistema stesso. Esso afferma:

Sia T una teoria matematica sufficientemente espressiva da contenere l'aritmetica: se T è coerente, non è possibile provare la coerenza di T all'interno di T.

Con qualche semplificazione,

Nessun sistema abbastanza coerente ed espressivo da contenere l'aritmetica si può utilizzare per dimostrare la sua stessa coerenza.

Questo risultato ebbe effetti devastanti sull'approccio filosofico alla matematica noto come programma di Hilbert. David Hilbert riteneva che si potesse dimostrare la coerenza di sistemi formali complessi, ad esempio l'analisi matematica sul campo dei reali, scomponendo il sistema in sistemi più semplici. Si sarebbe potuto così ricondurre la coerenza di tutta la matematica alla coerenza dell'aritmetica elementare. Il secondo teorema di incompletezza di Gödel mostra che nemmeno un sistema semplice come l'aritmetica elementare si può utilizzare per provare la sua stessa coerenza, per cui, a maggior ragione, non si può utilizzare per dimostrare la coerenza di sistemi più potenti.

Significato dei teoremi di Gödel

Quelli di Gödel sono teoremi di logica del primo ordine e vanno visti in questo contesto. Nella logica formale, gli enunciati matematici e le dimostrazioni si scrivono in un linguaggio simbolico in cui la loro validità si può verificare meccanicamente, e non possono esservi dubbi che un teorema sia conseguenza degli assiomi elencati all'inizio. In teoria, un computer può verificare qualsiasi dimostrazione sviluppata entro un sistema formale; di fatto ci sono programmi per controllare le dimostrazioni o cercarne di nuove: si chiamano dimostratori automatici dei teoremi o General Theorem Prover - G.T.P.

Per definire una teoria formale bisogna conoscere e definire alcuni assiomi di partenza. Ad esempio si può partire da un insieme finito di assiomi, come nella geometria euclidea, o, con maggiore generalità, si può consentire che esista un insieme infinito di assiomi. In questo caso deve essere possibile controllare meccanicamente se un qualsiasi enunciato è un assioma di quell'insieme o no (si parla in questo caso di schema di assiomi). In informatica si direbbe che esiste un insieme ricorsivo di assiomi. Anche se un elenco infinito di assiomi può sembrare strano, lo si usa nella assiomatizzazione dei numeri naturali nella logica del primo ordine: quando vogliamo convertire gli assiomi di Peano in un linguaggio del primo ordine, il principio di induzione diventa uno schema di assiomi: esso dice che per ogni possibile proprietà se lo zero ha quella certa proprietà e il successore di qualsiasi numero naturale che abbia quella proprietà ha anch'esso quella proprietà, allora tutti i numeri naturali hanno quella proprietà. Poiché ciò deve valere per ogni possibile proprietà e nel linguaggio del primo ordine non si può quantificare sulle proprietà, l'unico modo per definire il principio di induzione in questo contesto è considerare un numero infinito di assiomi, uno per ogni possibile proprietà che si può definire nel linguaggio del primo ordine. La teoria assiomatica che si ottiene così è nota in logica matematica come PA (Peano Arithmetic).

Il primo teorema di incompletezza di Gödel dimostra che ogni sistema che permette di definire i numeri naturali è per forza incompleto: contiene affermazioni la cui verità o falsità non si può dimostrare. Che esistano sistemi incompleti non è una scoperta sorprendente. Se si elimina il postulato delle parallele dalla geometria euclidea si ottiene un sistema incompleto, nel senso che non dimostra tutte le proposizioni vere. Per un sistema formale, essere incompleto significa che non include tutti gli assiomi necessari a caratterizzare in modo univoco uno specifico modello: è il caso dei primi quattro assiomi di Euclide, che ammettono come modello sia la geometria euclidea sia quelle non euclidee.

Ciò che Gödel ha mostrato è che, in molti casi importanti, come nella teoria dei numeri, nella teoria degli insiemi o nell'analisi matematica, non è mai possibile giungere a definire la lista completa degli assiomi che permetta di dimostrare tutte le verità. Ogni volta che si aggiunge un enunciato all'insieme degli assiomi, ci sarà sempre un altro enunciato non incluso. Si possono sempre aggiungere infiniti assiomi; ad esempio, si possono aggiungere tutti gli enunciati veri sui numeri naturali alla lista degli assiomi, ma tale lista non è un insieme ricorsivo. Se si prende un qualsiasi enunciato casuale, non sarà possibile stabilire se è o non è un assioma del sistema. Pertanto, data qualsiasi dimostrazione, in generale, non sarà più possibile verificarne la correttezza.

Il teorema di Gödel ha un'altra interpretazione esprimibile nel contesto informatico. Nella logica del primo ordine l'insieme di tutti i teoremi di una teoria è un insieme ricorsivamente enumerabile: ciò significa che è possibile scrivere un algoritmo che possa generare, prima o poi, ogni dimostrazione valida. Ci si può chiedere se questi teoremi soddisfino la proprietà più restrittiva di essere anche ricorsivi. È possibile scrivere un programma per computer in grado di determinare con certezza se un'affermazione è vera o falsa? Il teorema di Gödel dice che, in generale, non è possibile.

Molti studiosi di logica sostengono che i teoremi di incompletezza di Gödel abbiano affossato il programma di David Hilbert volto a costruire un formalismo matematico universale. L'idea generalmente condivisa è che nel secondo teorema si trovi il colpo di grazia al programma di Hilbert, altri pensano che si trovi nel primo teorema, ma c'è anche chi ritiene che nessuno dei due conduca necessariamente a questo tipo di conclusione.

Esempi di enunciati indecidibili

L'esistenza di un enunciato indecidibile all'interno di un sistema formale non è un fatto di per sé stesso particolarmente sorprendente.

Nel successivo lavoro congiunto di Gödel e Paul Cohen si trovano esempi concreti di enunciati indecidibili (enunciati che non possono essere né provati né refutati): sia l'assioma della scelta sia l'ipotesi del continuo sono indecidibili nella assiomatizzazione tradizionale della teoria degli insiemi. Questi risultati non si basano sul teorema di incompletezza.

Nel 1936, Alan Turing ha dimostrato che il problema dell'arresto — se cioè una macchina di Turing si arresta eseguendo un certo programma — è indecidibile. Questo risultato fu successivamente generalizzato nel campo delle funzioni ricorsive con il teorema di Rice che mostra come tutti i problemi non banali di decisione sono indecidibili in un sistema completo secondo Turing.