La seconda rivoluzione scientifica: matematica e logica. I teoremi di incompletezza di Gödel

La seconda rivoluzione scientifica: matematica e logica. I teoremi di incompletezza di Godel

I teoremi di incompletezza di Gödel

Nei giorni 5-7 settembre 1930 ebbe luogo a Königsberg la II Conferenza sull'epistemologia delle scienze esatte, organizzata dalla Gesellschaft für empirische Philosophie. Il primo giorno furono tenute le relazioni di Rudolf Carnap, Arend Heyting, John von Neumann e Friedrich Waismann, che presentarono, rispettivamente, il punto di vista logicista, intuizionista, formalista e wittgensteiniano sui fondamenti della matematica. Le tematiche affrontate in tali relazioni furono riprese in una discussione, coordinata da Hans Hahn (1879-1934), che ebbe luogo il 7 settembre 1930.

La discussione fu avviata da Hahn e Carnap, entrambi sostenitori della posizione logicista. Dopo di loro intervenne Heyting che, se da un lato sottolineò l'inconciliabilità della posizione intuizionista con quella logicista, dall'altro assunse un atteggiamento accomodante nei confronti della posizione formalista. Egli ammise infatti che, una volta data una dimostrazione finitista di coerenza come richiesto dal programma hilbertiano, anche gli intuizionisti avrebbero potuto usare i sistemi non costruttivi dal momento che questi ultimi, in virtù di tale dimostrazione, avrebbero ammesso un'interpretazione intuizionista. In margine a questa dichiarazione di Heyting, che sembrava dare per scontato che il programma hilbertiano potesse essere realizzato, un giovane virtualmente sconosciuto al di fuori di Vienna, Kurt Gödel (1906-1978), osservò quanto segue:

Secondo la concezione formalista, alle asserzioni dotate di significato della matematica transfinita si aggiungono (pseudo-) asserzioni che in sé non hanno alcun significato ma servono solo a semplificare il sistema, esattamente come in geometria si semplifica il sistema introducendo i punti infinitamente distanti. Questa concezione assume che, se al sistema S delle asserzioni dotate di significato, si aggiunge il sistema T delle asserzioni e degli assiomi transfiniti, e se poi a partire da S si dimostra un teorema attraverso una deviazione via teoremi ottenuti a partire da T, allora anche quel teorema è contenutisticamente corretto, e perciò nessun teorema contenusticamente falso diventa dimostrabile attraverso l'aggiunta degli assiomi transfiniti. Questo requisito di solito viene sostituito con quello della coerenza. Ora, vorrei osservare che tali due requisiti non possono essere considerati in alcun modo equivalenti senza ulteriori giustificazioni. Infatti, se in un sistema coerente A (diciamo, quello della matematica classica) si può dimostrare una proposizione p dotata di significato con l'aiuto di assiomi transfiniti, dalla coerenza di A segue solo che non-p non è formalmente derivabile nel sistema A. Tuttavia rimane concepibile che si possa percepire non-p attraverso considerazioni contenutistiche (intuizioniste) di qualche tipo, non rappresentabili formalmente in A. In questo caso, nonostante la coerenza di A, in A sarebbe dimostrabile una proposizione la cui falsità potrebbe essere percepita attraverso considerazioni finitiste. Interpretando il concetto di "asserzione dotata di significato" in modo sufficientemente restrittivo (per es., limitandolo alle equazioni numeriche finitarie), una cosa del genere certo non può accadere. D'altro canto, è possibile che si possa dimostrare un'asserzione della forma (Ex)F(x) dove F è una proprietà finitaria dei numeri naturali (per es., la negazione della congettura di Goldbach ha tale forma) con i metodi transfiniti della matematica classica, e che d'altra parte si possa stabilire attraverso considerazioni contenutistiche che tutti i numeri hanno la proprietà non-F; in effetti, vorrei sottolineare che questo sarebbe ancora possibile persino se fosse stata dimostrata la coerenza del sistema formale della matematica classica. Infatti di nessun sistema formale si può affermare con certezza che tutte le considerazioni contenutistiche sono rappresentabili in esso. (Gödel 1931a, pp. 147-148)

Questa incisiva critica del programma hilbertiano non suscitò alcuna reazione da parte dei partecipanti alla discussione, salvo quella di von Neumann il quale sottolineò che era ancora aperto il problema se tutte le regole di inferenza intuizionisticamente ammissibili fossero rappresentabili in un sistema formale. A questo punto Gödel fece la sua rivelazione:

Addirittura (assumendo la coerenza della matematica classica) si possono dare esempi di asserzioni (in effetti del tipo di quella di Fermat o di Goldbach) che, pur essendo contenutisticamente corrette, sono indimostrabili nel sistema formale della matematica classica. Perciò, se si aggiunge la negazione di una tale proposizione agli assiomi della matematica classica, si ottiene un sistema coerente in cui è dimostrabile una proposizione contenutisticamente falsa. (ibidem, p. 148)

Gödel diede così il primo annuncio pubblico del suo primo teorema di incompletezza. Egli aveva già comunicato privatamente tale risultato sia a Hahn sia a Carnap, che però non sembrano averne compreso il significato. Chi invece si rese immediatamente conto della sua portata fu von Neumann che, subito dopo la discussione pubblica al convegno di Königsberg, ebbe una discussione privata con Gödel.

Poco dopo, il 20 novembre 1930, von Neumann scrisse a Gödel per annunciargli di aver scoperto un notevole corollario del suo risultato: l'indimostrabilità della coerenza (secondo teorema di incompletezza). Nel frattempo, però, tale risultato era stato ottenuto anche da Gödel ed era stato comunicato da Hahn all'Accademia delle Scienze di Vienna il 23 ottobre 1930. Il 1° novembre 1930 i "Monatshefte für Mathematik und Physik" ricevettero l'articolo epocale di Gödel, Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I (Sulle proposizioni formalmente indecidibili dei Principia mathematica e di sistemi simili) pubblicato nel 1931. Tale articolo conteneva una dimostrazione dettagliata del primo teorema di incompletezza e un enunciato del secondo teorema di incompletezza, la cui dimostrazione sarebbe dovuta apparire in una seconda parte dell'articolo che però non vide mai la luce. L'articolo in questione fu anche presentato da Gödel all'Università di Vienna come Habilitationsschrift.

I risultati di Gödel furono accolti non senza contrasti. Da un lato fu avanzato il dubbio che la loro validità potesse essere legata al particolare sistema formale considerato (una versione della teoria dei tipi), dall'altro si usarono i risultati di Gödel come argomento per abbandonare i sistemi formali. In parte per superare queste obiezioni, Gödel estese i suoi risultati a una classe più ampia di sistemi, e nell'introduzione dell'articolo del 1931 ne diede dimostrazioni informali nelle quali si sostituiva la proprietà formale della coerenza con la proprietà semantica della correttezza. I risultati di incompletezza di Gödel furono estesi da John Barkley Rosser sostituendo l'ipotesi della ω-coerenza con quella più debole della coerenza (Rosser 1936) e da Stephen C. Kleene in termini della teoria delle funzioni ricorsive (Kleene 1936). Nel 1939 apparve il secondo volume dell'opera di David Hilbert e Paul Bernays, Grundlagen der Mathematik (Fondamenti di matematica), che conteneva non soltanto una dimostrazione del primo teorema di incompetezza, ma anche una dimostrazione se non completa, almeno abbastanza dettagliata, del secondo teorema di incompletezza. Il secondo volume dell'opera di Hilbert e Bernays segnò la consacrazione definitiva dei risultati di Gödel presso la comunità dei logici.

Il programma hilbertiano

Secondo la formulazione cui si riferisce Gödel nella discussione di Königsberg, che è quella di Hilbert (1928), la concezione hilbertiana della matematica può essere descritta nel modo seguente.

La matematica consta di un nucleo costituito da asserzioni e metodi dimostrativi elementari, detti da Hilbert finitari (finit). Le asserzioni finitarie sono asserzioni del tipo della proposizione di Fermat ∀x∀y∀z∀w(x>0∧y>0∧z>0∧ w>2→x^w+ +y^w≠z^w). Un tipico metodo dimostrativo finitario è il procedimento di dimostrazione per induzione applicato ad asserzioni finitarie. Ciò che è caratteristico del nucleo finitario è che in esso si considerano soltanto oggetti controllabili in ogni loro parte e si usano solo metodi assolutamente sicuri, che quindi non possono condurre ad alcuna falsità. Il nucleo finitario, però, è molto limitato, e per le esigenze della matematica attuale dev'essere arricchito con le asserzioni e i metodi transfiniti della teoria degli insiemi. In ogni caso, le asserzioni finitarie sono le uniche dotate di significato, mentre le asserzioni transfinite ne sono prive e sono utili solamente per semplificare la dimostrazione di asserzioni finitarie.

Sulla base di questa concezione, Hilbert formulò un programma di fondazione della matematica che ammetteva due formulazioni equivalenti, dette rispettivamente 'programma della conservazione' e 'programma della coerenza'. Sia S un sistema contenente le asserzioni e i metodi dimostrativi finiti, e T un sistema contenente anche le asserzioni e i metodi dimostrativi transfiniti, per cui S⊆T. Supponiamo che S contenga un'espressione per ogni numero naturale n.

Programma della conservazione: dimostrare in S che, per ogni asserzione φ di S, se T⊦φ allora S⊦φ (dove T⊦φ significa: φ é dimostrabile in T; il significato di S⊦φ è analogo).

Programma della coerenza: dimostrare in S la coerenza di T.

È facile vedere che, per realizzare il programma della coerenza, è sufficiente realizzare quello della conservazione. Infatti, supponiamo che si possa dimostrare in S che, per ogni asserzione φ di S, se T⊦φ allora S⊦φ. In particolare, si può dimostrare in S che se T⊦0=1 allora S⊦0=1. Ma, per la natura di S, in S non si può dimostrare alcuna falsità, dunque S⊬0=1. Perciò si conclude che T⊬0=1. Ciò dimostra in S che T è coerente, come desiderato. Viceversa, come osserva Gödel, interpretando il concetto di asserzione dotata di significato in modo sufficientemente restrittivo ‒ specificamente identificandolo con quello di asserzione finita ‒ per realizzare il programma della conservazione è sufficiente realizzare quello della coerenza. Questa circostanza è illustrata da Hilbert riferendosi alla proposizione di Fermat:

Supponiamo di aver trovato la dimostrazione del grande teorema di Fermat, facendo uso della ε-funzione logica. Questa dimostrazione può essere trasformata in una dimostrazione finitaria nel seguente modo. Supponiamo di disporre di segni numerici p,a,b,c (p>2) che soddisfano l'equazione di Fermat a^p+b^p=c^p; allora potremmo ottenere questa equazione anche come formula dimostrabile, esprimendo nella forma di una dimostrazione la determinazione della coincidenza dei segni numerici a^p+b^p e c^p. D'altro canto, per la nostra ipotesi, avremmo una dimostrazione della formula (Z(a)&Z(b)&Z(c)&Z(p)&(p>2))→(a^p+b^p≠c^p) dalla quale, mediante sostituzione e inferenza, si ottiene a^p+b^p≠c^p. Così sarebbero dimostrabili tanto a^p+b^p=c^p quanto anche a^p+b^p≠c^p. Ma ciò, come è mostrato in una maniera finitaria dalla dimostrazione di non-contraddittorietà, non può darsi. (Hilbert 1928, pp. 281-282)

L'argomentazione di Hilbert è del tipo seguente. Supponiamo che si possa dimostrare in S la coerenza di T e che T⊦φ dove φ≡∀x∀y∀z∀w(x>0∧y>0∧z>0∧w>2→x^w+y^w≠z^w). Dobbiamo dimostrare in S che S⊦φ. Per dimostrarlo, ragioniamo in S come di seguito. Poiché T⊦φ, esiste una dimostrazione d di φ in T e ciò può essere verificato in S. Dunque, per tale d:

[1] S⊦ 'd è una dimostrazione di φ in T'.

Assumiamo ¬φ. Allora per qualche a,b,c,p tale che a>0∧b>0∧c>0∧p>2 si ha a^p+b^p=c^p e ciò può essere verificato in base a un semplice computo in T.

Perciò esiste anche una dimostrazione d′ di ¬φ in T, e questo fatto può essere verificato in S. Dunque per tale d′:

[2] S⊦ 'd′ è una dimostrazione di ¬φ in T'.

D'altra parte, dall'ipotesi che in S si può dimostrare la coerenza di T, segue che:

[3] S⊦¬('d è una dimostrazione di φ in T'∧ 'd′ è una dimostrazione di ¬φ in T').

Da [1]-[3] segue che in S si può dimostrare una contraddizione. Ma, per la natura di S, in S non si può dimostrare alcuna falsità, dunque questo è impossibile. Dal momento che l'assunzione ¬φ porta a una conclusione impossibile, si conclude che S⊦φ, come desiderato.

Dunque, come osserva Gödel, se si interpreta il concetto di 'asserzione dotata di significato' in modo sufficientemente restrittivo, in particolare se lo si limita alle equazioni numeriche finitarie come la congettura di Fermat, per realizzare il programma della conservazione basta realizzare quello della coerenza. In effetti la restrizione in questione è essenziale per dimostrare [2] nell'argomentazione precedente.

Il primo teorema di incompletezza di Gödel dimostrò che il programma della conservazione non è realizzabile, costruendo un'asserzione dotata di significato φ tale che T⊦φ ma S⊦/φ. Dal canto suo il secondo teorema di incompletezza di Gödel dimostrò che il programma della coerenza non è realizzabile. In realtà, in vista di quanto si è detto sopra, ciascuno dei due teoremi di incompletezza implica, di per sé, che tanto il programma della conservazione quanto quello della coerenza non sono realizzabili.

L'incompletezza dell'aritmetica

Tav. I

Ai fini della trattazione dei teoremi di incompletezza identifichiamo il sistema S consistente delle asserzioni e dei metodi dimostrativi finitari, dotati di significato, con PRA. Identifichiamo inoltre il sistema T consistente delle asserzioni e dei metodi dimostrativi transfiniti, privi di significato, con qualsiasi sistema T′ tale che PA⊆T′ (Tav. I).

Il teorema del punto fisso

Assegnamo a ogni formula φ di T un numero naturale n, detto il codice di φ. Se n è il codice di φ, scriviamo ⌈φ⌉ per designare n. Analogamente assegniamo un codice a ogni termine t e a ogni derivazione d in T.

Il linguaggio di S contiene costanti funzionali neg e imp tali che, per ogni formula φ e ψ, S⊦ neg(⌈φ⌉)=⌈¬φ⌉, S⊦ imp(⌈φ⌉), ⌈ψ⌉)=⌈φ→ψ⌉. Esso contiene, inoltre, una costante funzionale sub tale che, per ogni formula φ(a) contenente un unico parametro individuale a e per ogni termine t, S⊦ sub(⌈φ(a)⌉,⌈t⌉)=⌈φ(t)⌉.

Si può definire una formula Prov_T(a,b) contenente due soli parametri individuali a e b tale che, per ogni derivazione d in T e ogni formula φ, si ha: S⊦ Prov(⌈d⌉,⌈φ⌉) se d è una derivazione di φ in T; S⊦¬Prov(⌈d⌉,⌈φ⌉) se d non è una derivazione di φ in T. Scriviamo Pr_T(b) per indicare ∃xProv_T(x,b).

I teoremi di incompletezza dipendono dal seguente risultato (Gödel 1934). Per ogni formula ψ(a) contenente un unico parametro individuale a, esiste un enunciato φ tale che S⊦φ→ψ(⌈φ⌉).

Per dimostrare tale risultato, per una ψ(a) come nell'enunciato del teorema, sia χ(a₀)≡ψ(sub(a₀,a₀)), sia k=⌈χ(a₀)⌉ e sia φ≡χ(k). Otteniamo quindi φ≡χ(k)=ψ(sub(k,k)), perciò S⊦φ → ψ(sub(k,k))→ψ(sub(⌈χ(a₀)⌉, k)→ψ(⌈χ(k)⌉)→ψ(⌈φ⌉), come desiderato.

Sebbene il teorema del punto fisso costituisca attualmente il principale strumento per dimostrare il primo teorema di incompletezza, esso non fu formulato nell'articolo che Gödel scrisse nel 1931, in cui si considera solo un particolare esempio di enunciato φ tale che S⊦φ→¬Pr_T(⌈φ⌉). In una nota aggiunta nel 1965 agli appunti delle sue lezioni (Gödel 1934), si afferma che il teorema del punto fisso venne notato per la prima volta nel 1934 da Carnap. Esso, comunque, fu formulato da Gödel nel 1934 e in seguito ripreso da Rosser nel 1939, ma il suo uso è diventato standard solo a partire dall'articolo di Solomon Feferman del 1960. Un'estensione del teorema del punto fisso a formule ψ(a) contenenti altri parametri individuali oltre a venne data nel 1962 da Richard Montague.

Il teorema dell'indefinibilità della verità

Una prima applicazione del teorema del punto fisso è costituita dal seguente risultato (Gödel 1934; Tarski 1933):

Teorema dell'indefinibilità della verità: se T è coerente, non esiste alcuna formula Tr(a) contenente un unico parametro individuale a tale che, per ogni formula chiusa φ, T⊦φ→Tr(⌈φ⌉).

Per dimostrare questo risultato, supponiamo che una tale formula Tr(a) esista. Allora per il teorema del punto fisso esiste una formula chiusa φ tale che

[4] S⊦φ→¬Tr(⌈φ⌉).

D'altra parte per ipotesi T⊦φ→Tr(⌈φ⌉). Da quest'ultima e da [4] segue T⊦φ→¬φ e perciò T⊦φ e T⊦¬φ, cioè T è incoerente contraddicendo l'ipotesi.

Per comprendere il significato del teorema dell'indefinibilità della verità si noti che, secondo la ormai classica formulazione data da Alfred Tarski nel 1936, una definizione di verità richiede che, per ogni asserzione P, 'P' è vera se e solo se P. Perciò, perchè una formula Tr(a) contenente un unico parametro individuale a possa essere considerata una definizione di verità, occorre che, per ogni formula chiusa φ,T⊦Tr(⌈φ⌉)→φ. Il teorema dell'indefinibilità della verità stabilisce, allora, che una tale definizione di verità non esiste. Il teorema dell'indefinibilità della verità non fu formulato da Gödel nel 1931 ma solo nel 1934. In una nota aggiunta nel 1965 ai già citati appunti delle lezioni del 1934 (nota 25) si rimanda, per una discussione più approfondita del teorema, ai lavori di Tarski del 1933 e 1944. In una lettera del 1966, Gödel dichiara che il teorema dell'indefinibilità della verità fu scoperto indipendentemente da lui e da Tarski e che esso è la vera ragione dell'esistenza di enunciati come quello considerato nel primo teorema di incompletezza (von Neumann 1966). Ciò indurrebbe a supporre che Gödel fosse già pervenuto al teorema nel 1931, anche se egli non lo incluse nell'articolo pubblicato lo stesso anno. Tale ipotesi è avvalorata dal fatto che, in una lettera a Gödel del 20 aprile 1931, Bernays confessava di non comprendere perché non fosse possibile dare una definizione di verità e addirittura proponeva un candidato per una tale definizione, mentre in una successiva lettera a Gödel del 3 maggio 1931 egli riconosceva il proprio errore. Questo prova indirettamente che all'epoca Gödel era consapevole dell'indefinibilità della verità. C'è da chiedersi perché Gödel evitasse ogni riferimento al concetto di verità nei risultati principali del 1931. La risposta va forse ricercata nelle tendenze filosofiche predominanti a quel tempo, che guardavano con grande sospetto al concetto di verità oggettiva e perlopiù lo rifiutavano come privo di significato. Una conferma di questa ipotesi si trova in un passo cancellato di un abbozzo di risposta di Gödel a una lettera di uno studente datata 27 maggio 1970, in cui si legge

Tuttavia, in conseguenza dei pregiudizi filosofici dei nostri tempi (1) nessuno ricercava una dimostrazione di coerenza relativa perché veniva considerato assiomatico che una dimostrazione di coerenza dovesse essere finitaria per aver senso, e (2) un concetto di verità matematica oggettiva in quanto contrapposto a quello di dimostrabilità veniva guardato con grandissimo sospetto ed era ampiamente rifiutato come privo di significato. (in Feferman 1984, p. 107)

Questo passo sembra provare che, sebbene già a quell'epoca Gödel aderisse al concetto di verità matematica oggettiva ‒ a cui egli attribuiva un'influenza positiva ai fini della sua scoperta del primo teorema di incompletezza ‒ tuttavia egli temeva che risultati contenenti un riferimento a tale concetto potessero essere visti con sospetto negli ambienti fondazionali, allora dominati dalle idee hilbertiane. Perciò nel 1931 egli si limitò a pubblicare quei risultati che non avrebbero potuto suscitare obiezioni in quegli ambienti (Feferman 1984).

Il primo teorema di incompletezza

Diciamo che T è ω-coerente se, per ogni enunciato della forma ∃xφ(x), se T⊦∃xφ(x) allora per qualche numero naturale n si ha che T⊬¬φ(n); diciamo che T è ω-incoerente se non è ω-coerente.

La principale applicazione del teorema del punto fisso è costituita dal seguente risultato (Gödel 1931b).

Primo teorema di incompletezza: esiste un enunciato φ tale che:

1) se T è coerente allora T⊬φ;

2) se T è ω-coerente allora T⊬¬φ;

3) se T è coerente allora φ è vero.

Per dimostrare tale risultato si noti anzitutto che, per il teorema del punto fisso, esiste un enunciato φ tale che:

a) S⊦φ↔¬Pr_T(⌈φ⌉).

1) Supponiamo che T⊦φ. Allora esiste una derivazione di φ in T, dunque per un certo k si ha S⊦Prov_T(k,⌈φ⌉), per cui S⊦Pr_T(⌈φ⌉). Da ciò per (a) segue S⊦¬φ, donde T⊦¬φ. Dunque T è incoerente, contraddicendo l'ipotesi.

2) Supponiamo che T⊦¬φ. Da quest'ultima per (a) si ottiene T⊦Pr_T(⌈φ⌉), cioè:

b) T⊦∃xProv_T(x,⌈φ⌉).

D'altra parte per (1) non esiste alcuna derivazione di φ in T, perciò per ogni n si ha S⊦¬Prov_T(n,⌈φ⌉), dunque:

c) per ogni n si ha T⊦¬Prov_T(n,⌈φ⌉).

Da (b) e (c) segue che T è ω-incoerente, contraddicendo l'ipotesi.

3) Per (1) non esiste alcuna derivazione di φ in T, dunque φ è vera poiché per (a) φ esprime la propria inderivabilità in T.

Per vedere come il primo teorema di incompletezza refuti il programma della conservazione consideriamo l'asserzione ψ≡∀x¬Prov_T(x,⌈φ⌉), dove φ è l'enunciato dato dal primo teorema di incompletezza. Si noti che, poiché Prov_T(a,b) è una formula dotata di significato, anche ψ è dotata di significato; inoltre per (a) si ha T⊦φ→ψ. Ora, poiché per la parte (3) del teorema φ è vera, si ha T⊦φ, quindi anche T⊦ψ. Inoltre per la parte (1) del teorema T⊬φ, perciò S⊬φ, quindi anche S⊬ψ. Dunque ψ fornisce un esempio di formula dotata di significato tale che T⊦ψ ma S⊬ψ.

Il secondo teorema di incompletezza

Per dimostrare il secondo teorema di incompletezza occorre introdurre alcune assunzioni sulla formula Pr_T(b). Supponiamo che, per ogni enunciato φ e ψ, valgano le seguenti condizioni, dette le condizioni di derivabilità

D1) Se T⊦φ allora S⊦Pr_T(⌈φ⌉)

D2) S⊦Pr_T(⌈φ⌉)∧Pr_T(⌈φ→ψ⌉)→Pr_T(⌈ψ⌉)

D3) S⊦Pr_T(⌈φ⌉)→Pr_T(⌈Pr_T(⌈φ⌉)⌉).

Si noti che D1 segue immediatamente dalle assunzioni su Prov_T(a,b) già fatte in precedenza.

L'idea di introdurre condizioni di derivabilità che formalizzino alcune proprietà fondamentali del 'predicato di dimostrabilità' Pr_T(b) risale a Bernays, che le formulò allo scopo di semplificare la dimostrazione del secondo teorema di incompletezza. La formulazione originaria di Bernays delle condizioni di derivabilità, però, era piuttosto inelegante. La presente formulazione D1-D3 si deve a Martin Hugo Löb (Löb 1955).

Possiamo allora formulare il seguente risultato (Gödel 1931b).

Secondo teorema di incompletezza: esiste un enunciato φ tale che:

1) Se T è coerente allora T⊬φ;

2) S⊦Con_T→φ, dove Con_T≡¬Pr_T(⌈0=1⌉);

3) Se T è coerente allora S⊬Con_T.

Per dimostrare tale risultato usiamo anche in questo caso il fatto che, per il teorema del punto fisso, esiste un enunciato φ tale che:

a) S⊦φ→¬Pr_T(⌈φ⌉).

1) Come nella dimostrazione del primo teorema di incompletezza.

2) Per (a) T⊦Pr_T(⌈φ⌉)→¬φ, da cui per D1 e D3 si ottiene:

b) S⊦Pr_T(⌈Pr_T(⌈φ⌉)⌉)→Pr_T(⌈¬φ⌉).

D'altra parte per D3:

c) S⊦Pr_T(⌈φ⌉)→Pr_T(⌈Pr_T(⌈φ⌉)⌉).

Da (b) e (c) segue:

d) S⊦Pr_T(⌈φ⌉)→Pr_T(⌈φ⌉)∧Pr_T(⌈¬φ⌉).

Poiché T⊦φ→(¬φ→0=1), usando D1 e D2 si ottiene S⊦Pr_T(⌈φ⌉)→(Pr_T(⌈¬φ⌉)→Pr_T(⌈0=1⌉)), da cui:

e) S⊦Pr_T(⌈φ⌉)∧Pr_T(⌈¬φ⌉)→Pr_T(⌈0=1⌉).

Da (d) e (e) segue S⊦Pr_T(⌈φ⌉)→Pr_T(⌈0=1⌉), da cui per contrapposizione si ottiene

f) S⊦Con→¬Pr_T(⌈φ⌉).

Da (f) e (a) segue infine S⊦Con_T→φ.

(3) Per (1) e (2).

Le parti (1) e (3) del primo teorema di incompletezza ci dicono che esiste un enunciato vero ma non dimostrabile in T. La parte (3) del secondo teorema di incompletezza fornisce un esempio specifico di tale enunciato, cioè Con_T, che esprime la coerenza di T. È immediato che la parte (3) del secondo teorema di incompletezza refuta il programma della coerenza.

Si noti che la refutazione del programma hilbertiano operata dai teoremi di incompletezza si basa in modo essenziale sull'assunzione del tutto naturale che S⊆T. L'unico modo per mantenere in vita il programma hilbertiano sarebbe mostrare che tale assunzione è falsa. Questa possibilità venne ammessa da Gödel:

Desidero osservare espressamente che il teorema XI [secondo teorema di incompletezza] (e i risultati corrispondenti per M e A) non contraddicono il punto di vista formalista di Hilbert. Infatti tale punto di vista presuppone solo l'esistenza di una dimostrazione di coerenza in cui non si usano altro che metodi dimostrativi formalisti, ed è concepibile che esistano dimostrazioni finitarie che non possano essere espresse nel formalismo di P (o di M o di A). (Gödel 1931b, p. 197)

Tuttavia a settanta anni dalla scoperta di Gödel non esiste alcun elemento che lasci supporre la plausibilità dell'ipotesi che S⊈T. Lo stesso Gödel respinse successivamente tale ipotesi (Gödel 1958).

Forma diofantea del primo teorema di incompletezza

Sebbene la formula ∀x¬Prov_T(x,⌈φ⌉), dove φ è l'enunciato dato dal primo teorema di incompletezza, sia dotata di significato, essa non è dello stesso tipo dell'enunciato di Fermat, cioè non è un'equazione numerica finitaria. Sorge il problema se essa possa essere sostituita, nel primo teorema di incompletezza, da una formula della forma di un'equazione numerica finitaria.

Un primo passo verso la soluzione di tale problema venne compiuto da Gödel nel 1934 mostrando che ∀x¬-Prov_T(x,⌈φ⌉) può essere sostituita da una formula della forma Q₁x₁…Q_nx_n(t(x₁,…,x_n)=u(x₁,…,x_n)), dove ciascun Q_i,1≤i≤n, è ∀ oppure ∃ e dove t e u sono polinomi a coefficienti interi. In un poscritto del 3 giugno 1964 Gödel asserì, senza dimostrazione, che questo risultato può essere migliorato mostrando che la formula in questione può essere sostituita da una della forma ∀x₁…∀x_m∃y₁…∃y_n(t(x₁,…,x_n)= =u(x₁,…,x_n)), dove t e u sono polinomi a coefficienti interi.

Un miglioramento molto più rilevante venne ottenuto successivamente, grazie ai lavori di Jurij Vladimirovič Matijasevič dei primi anni Settanta; egli mostrò che ∀x¬ Prov_T(x,⌈φ⌉) può essere sostituita da una formula della forma ∃x₁…∃x_n(t(x₁,…,x_n)=u(x₁,…,x_n)), dove t e u sono polinomi a coefficienti interi. Chiamiamo formula diofantea una formula di tale forma. Questa estensione dei risultati di Gödel può essere stabilita nel modo seguente.

Diciamo che una formula φ(a) contenente un unico parametro individuale rappresenta numericamente un insieme di numeri naturali A in T se, per ogni numero naturale n, si ha: (1) se n∈A allora T⊦φ(n); (2) se n∉A allora T⊦¬φ(n).

In virtù del lavoro di Matijasevič si può dimostrare il seguente risultato (Dyson 1982):

Lemma: ogni insieme ricorsivo è rappresentato numericamente in T da una formula diofantea.

Sia W₀, W₁,… un'enumerazione di tutti gli insiemi ricorsivi. Per ogni i indichiamo con ψ_i(a) la formula diofantea che rappresenta numericamente W_i in T, che esiste in virtù del lemma. Possiamo allora stabilire il seguente risultato:

Forma diofantea del primo teorema di incompletezza: esiste un n tale che, se T è coerente:

1) T⊬ψ_n(n);

2) T⊬¬ψ_n(n);

3) ¬ψ_n(n) è vero.

Per dimostrare le parti (1) e (2) di questo risultato supponiamo:

a) per ogni n, T⊦ψ_n(n) oppure T⊦¬ψ_n(n).

Sia A={n∣T⊦¬ψ_n(n)}. Poiché T è ricorsivamente enumerabile, anche A è ricorsivamente enumerabile. Ma per (a)-A = {n∣T⊬¬ψ_n(n)}={n∣T⊦ψ_n(n)}, dunque −A è ricorsivamente enumerabile. Poiché sia A sia −A sono ricorsivamente enumerabili, A è un insieme ricorsivo. Perciò esiste un j tale che ψ_j(a) rappresenta A in T, cioè per ogni n:

b) se n∈A allora T⊦ψ_j(n)

c) se n∉A allora T⊦¬ψ_j(n).

Se j∈A allora per (b) T⊦ψ_j(j), da cui per l'ipotesi che T sia coerente segue T⊬¬ψ_j(j) e perciò, per la definizione di A, j∉A. Se invece j∉A allora per (c) T⊦¬ψ_j(j), da cui per la definizione di A si ottiene j∈A. In entrambi i casi si ha una contraddizione. Si conclude, perciò, che esiste un n che soddisfa (1) e (2).

Per dimostrare che anche (3) è soddisfatto supponiamo che ¬ψ_n(n) non sia vero. Allora ψ_n(n) è vero, dunque T⊦ψ_n(n) poichè ogni enunciato diofanteo vero è dimostrabile in T. Ma ciò contraddice (1).

IIa

IIb

Tavola IIa e IIb

L'incompletezza e la pratica matematica

Le proposizioni metamatematiche vere ma indimostrabili di Gödel sono state spesso viste dalla comunità dei matematici come costruzioni artificiose, di scarso interesse. La situazione è cambiata in seguito alla scoperta, a partire dal 1977, di vari esempi di proposizioni matematiche vere ma indimostrabili nell'aritmetica di Peano PA. Gli esempi comprendono una variante del teorema di Ramsey finito, la versione finita di Friedman del teorema di Kruskal, il teorema di Goodstein, un teorema sui giochi di Gentzen e vari altri.

Se il secondo volume dell'opera di Hilbert e Bernays segnò la consacrazione definitiva dei risultati di Gödel presso i logici, l'accettazione tra i matematici, invece, è stata molto più lenta. Fino agli anni Settanta le proposizioni metamatematiche vere ma indimostrabili di Gödel sono state generalmente considerate come costruzioni piuttosto artificiose, interessanti per i fondamenti della matematica ma non per la matematica in quanto tale. In effetti esse non hanno avuto applicazioni rilevanti alla pratica matematica. La situazione sembra ben riassunta dal seguente giudizio di Hao Wang:

Nel limitato campo della logica matematica la presenza di Gödel naturalmente è cospicua. Nessuno può negare che egli sia il più grande logico del secolo, il cui lavoro è al centro stesso dell'intero campo. Ma, come per Hilbert, il suo interesse per i fondamenti della matematica era fortemente motivato dalla credenza che sviluppi fondamentali in tale area dovessero in qualche modo rivoluzionare l'intero campo della matematica (pura), forse come il lavoro di Einstein fece per la fisica. Sotto questo aspetto il risultato è stato, temo, piuttosto deludente [...]. Molti matematici non accetterebbero il giudizio implicito che l'opera di Gödel occupi nella matematica un posto paragonabile a quello di Einstein nella fisica. L'opera di Gödel ha avuto poca influenza sulla pratica della ricerca e sulla concezione della matematica della maggioranza dei matematici. (Wang 1987, p. 168)

Con la scoperta di proposizioni matematiche vere ma indimostrabili nell'aritmetica di Peano PA i teoremi di incompletezza, sia pure in una forma diversa da quella originaria, sembrano essere entrati a far parte della cultura corrente della comunità matematica, bensì la loro incidenza sulla pratica matematica rimane marginale. Sono state anche avanzate obiezioni sul carattere realmente aritmetico di tali proposizioni (Isaacson 1987). In particolare è stato sostenuto che, perché una proposizione vera sia aritmetica, occorre non solo che essa sia esprimibile nel linguaggio di PA, ma anche che la sua verità sia dimostrabile usando solo concetti aritmetici. Ora la dimostrazione del teorema di Goodstein, per esempio, non soddisfa questo requisito poiché fa uso di concetti di ordine superiore come quelli di numero ordinale e di buon ordinamento degli ordinali; lo stesso vale per le altre proposizioni matematiche vere ma indimostrabili in PA. Ciò fa nascere il problema se i teoremi di incompletezza rivelino l'incompletezza di PA rispetto a concetti realmente aritmetici, oppure mostrino la sua incompletezza rispetto a concetti di ordine superiore.