Teoremi di incompletezza di Gödel

Questa voce o sezione sull'argomento matematica è priva o carente di note e riferimenti bibliografici puntuali.

---

Sebbene vi siano una bibliografia e/o dei collegamenti esterni, manca la contestualizzazione delle fonti con note a piè di pagina o altri riferimenti precisi che indichino puntualmente la provenienza delle informazioni. Puoi migliorare questa voce citando le fonti più precisamente. Segui i suggerimenti del progetto di riferimento.

In logica matematica, i teoremi di incompletezza di Gödel sono due famosi teoremi dimostrati da Kurt Gödel nel 1930. Gödel enunciò il suo primo teorema di incompletezza in 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 che fu ricevuto dalla rivista Monatshefte für Mathematik il 17 novembre 1930.^[1] Essi fanno parte dei teoremi limitativi, che precisano le proprietà che i sistemi formali non possono avere.

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 ${\displaystyle R(x)}$ sussiste ${\displaystyle \rightarrow P\vdash r(x)}$;
• se ${\displaystyle R(x)}$ non sussiste ${\displaystyle \rightarrow P\vdash \lnot r(x)}$.

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

In ogni teoria matematica T sufficientemente espressiva da contenere l'aritmetica, esiste una formula ${\displaystyle \varphi }$ tale che, se T è coerente, allora né ${\displaystyle \varphi }$ né la sua negazione ${\displaystyle \lnot \varphi }$ 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.^[2]

Intuitivamente, la dimostrazione del primo teorema ruota attorno alla possibilità di definire una formula logica ${\displaystyle \varphi }$ che neghi la propria dimostrabilità: si prova quindi che, affinché T sia coerente, né ${\displaystyle \varphi }$ né ${\displaystyle \lnot \varphi }$ 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 possono essere entrambe feconde di conseguenze.

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.

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.

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 che 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.

Nel 1973 si è dimostrato che il problema di Whitehead della teoria dei gruppi è indecidibile nel sistema della teoria degli insiemi. Nel 1977, Kirby, Paris e Harrington dimostrarono che un enunciato della combinatorica, una variazione del teorema di Ramsey, è indecidibile nella assiomatizzazione dell'aritmetica data dagli assiomi di Peano ma che può essere dimostrato nel sistema più ampio della teoria degli insiemi. Anche il teorema di Kruskal, che trova applicazioni in informatica, è indecidibile a partire dagli assiomi di Peano, ma può essere dimostrato in teoria degli insiemi. Il teorema di Goodstein propone un'affermazione relativamente semplice sui numeri naturali che è indecidibile nell'aritmetica di Peano.

Gregory Chaitin ha formulato enunciati indecidibili nella teoria algoritmica dell'informazione e ha di fatto dimostrato un suo teorema di incompletezza valido in questo settore.

Uno dei primi problemi sospettati di essere indecidibili fu il problema della parola per i gruppi, proposto da Max Dehn nel 1911, secondo cui esiste un gruppo finitamente generato che non possiede nessun algoritmo in grado di stabilire se due parole sono equivalenti. Solo nel 1952 si è dimostrata l'indecidibilità di questo problema.

L'ampia discussione sul primo teorema ha prodotto molti fraintendimenti. Qui chiariamo i più comuni.

1. Il teorema si applica solo ai sistemi che consentono di definire i numeri naturali come un insieme. Non basta che il sistema contenga i numeri naturali. È necessario che, usando gli assiomi del sistema e la logica del primo ordine, si possa esprimere il concetto "${\displaystyle x}$ è un numero naturale". Molti sistemi che contengono i numeri naturali sono completi; i numeri reali e i numeri complessi hanno assiomatizzazioni complete.
2. È possibile dimostrare una proposizione indecidibile in un sistema di assiomi aggiungendo assiomi appositi. Ad esempio è possibile dimostrare il Teorema di Goodstein, che tratta di numeri interi, accettando gli assiomi dei numeri transfiniti, che sono classi di infinito superiori all'infinito dei numeri interi. Ed è possibile innalzare al rango di nuovo assioma proprio l'affermazione indecidibile (o la sua negazione, anch'essa indecidibile), ottenendo una nuova teoria matematica, come nel caso dell'analisi non-standard. Questo meccanismo è ripetibile all'infinito. Si potrebbe quindi dire che la goedelizzazione funge da generatore di assiomi sensati.
3. Gödel non credeva che i suoi teoremi avrebbero distrutto la fede nella matematica: disse infatti che la completezza dell'aritmetica non poteva essere dimostrata dagli assiomi dell'aritmetica, ma che occorreva qualcos'altro.

Le conseguenze dell'incompletezza influenzano la filosofia della matematica, e in particolare alcune sue scuole di pensiero, come il formalismo, che basa la definizione dei suoi principi sulla logica formale. Il primo teorema può essere parafrasato dicendo che "non è possibile costruire un sistema assiomatico omnicomprensivo che sia allo stesso tempo in grado di provare tutte le verità matematiche, e nessuna falsità."

D'altro canto, da un punto di vista strettamente formalista, questa parafrasi dovrebbe essere considerata priva di senso, perché presuppone che la "verità" e la "falsità" matematiche siano concetti ben definiti in senso assoluto, e non concetti relativi a ciascun specifico sistema formale.

La seguente riformulazione del secondo teorema è ancor più sconcertante per chi si occupa dei fondamenti della matematica:

Se un sistema assiomatico può dimostrare la sua stessa coerenza, allora esso deve essere incoerente.

Pertanto, per poter stabilire la coerenza di un sistema S, è necessario utilizzare un altro sistema T. Ma una dimostrazione in T non è del tutto convincente a meno che la coerenza di T non sia già stata stabilita senza usare il sistema S. Ad esempio, la coerenza degli assiomi di Peano per i numeri naturali può essere dimostrata nella teoria degli insiemi, ma non nella sola teoria dei numeri naturali. Ciò fornisce una risposta negativa al problema numero 2 del famoso elenco di David Hilbert sulle più importanti questioni aperte della matematica (noto come elenco dei problemi di Hilbert).

In linea di principio i teoremi di Gödel lasciano ancora qualche speranza: potrebbe essere possibile creare un algoritmo generale che determina, per un dato enunciato, se esso sia indecidibile oppure no, permettendo in questo modo ai matematici di evitare del tutto le proposizioni indecidibili. Comunque, la risposta negativa data all'Entscheidungsproblem mostra che tale algoritmo non può esistere.

Alcuni studiosi ritengono che un enunciato, che non può essere dimostrato all'interno di un sistema deduttivo, può essere ben dimostrabile con l'uso di un metalinguaggio. E che ciò che non può essere dimostrato in quel metalinguaggio può probabilmente essere dimostrato tramite un meta-metalinguaggio. Questo processo, in teoria, può essere riprodotto all'infinito in modo ricorsivo. Se ci si richiama a una specie di super teoria dei tipi con un assioma di riducibilità — che con un procedimento induttivo si estende all'intero universo stratificato dei linguaggi — sarebbe possibile, di volta in volta, aggirare l'ostacolo dell'incompletezza.

Occorre notare che i teoremi di Gödel sono applicabili solamente a quei sistemi assiomatici sufficientemente potenti.

"Sufficientemente potenti" vuol dire che la teoria contiene un numero sufficiente di regole aritmetiche per consentire la costruzione della codifica necessaria alla dimostrazione del primo teorema di incompletezza. In pratica, tutto ciò che si richiede sono alcune regole elementari riguardanti l'addizione e la moltiplicazione, come ad esempio avviene nella formalizzazione nella aritmetica di Robinson. Esistono sistemi assiomatici ancora più deboli che sono coerenti e completi, ad esempio l'aritmetica di Presburger, in cui si può dimostrare qualsiasi enunciato vero del primo ordine che riguarda la sola addizione.

Il sistema assiomatico può consistere di un numero infinito di assiomi (come nell'aritmetica del primo ordine di Peano), ma, per poter applicare il teorema di Gödel, deve esistere un algoritmo che sia effettivamente in grado di verificare la correttezza delle dimostrazioni. Ad esempio, l'insieme di tutti gli enunciati del primo ordine che sono veri nel modello dei numeri naturali è una teoria completa, ovviamente; qui, il teorema di Gödel non si può applicare perché non esiste una procedura in grado di decidere se un certo enunciato sia o non sia un assioma. Infatti, questo fatto è proprio una conseguenza del primo teorema di incompletezza di Gödel.

Un altro esempio di una teoria specificata in modo tale che ad essa non si possa applicare il primo teorema di Gödel può essere costruito nel seguente modo. Si ordinano tutti i possibili enunciati sui numeri naturali prima per lunghezza, e poi seguendo l'ordinamento lessicografico. Si parte da un sistema assiomatico inizialmente equivalente al sistema degli assiomi di Peano. Si scorre poi la lista degli enunciati uno ad uno e, se non si può dimostrare la verità o la falsità dell'enunciato corrente sulla base degli assiomi correnti, lo si aggiunge al sistema. In questo modo si costruisce un sistema che è coerente e sufficientemente potente, ma non ricorsivamente enumerabile.

Gödel stesso dimostrò una versione dei precedenti teoremi che è tecnicamente leggermente più povera, mentre la prima dimostrazione dei teoremi nella forma qui presentata è stata fornita da J. Barkley Rosser nel 1936.

Fondamentalmente, la dimostrazione del primo teorema consiste nella costruzione, all'interno di un sistema assiomatico formale, di una certa affermazione p a cui si può dare la seguente interpretazione meta-matematica:

p = "Questa affermazione non può essere dimostrata"

In questa veste, essa può essere vista come una moderna variante del paradosso del mentitore. Diversamente dall'affermazione del mentitore, p non fa riferimento diretto a se stessa; la precedente interpretazione può solamente essere formulata dall'esterno del sistema formale.

Se il sistema formale è coerente, la prova di Gödel mostra che p (e la sua negazione) non possono essere dimostrate nel sistema. Pertanto p è «vera» (p dice che non può essere dimostrata, ed effettivamente non può essere dimostrata) ma appunto non può essere formalmente dimostrata nel sistema. Si noti che aggiungere p all'elenco degli assiomi non aiuterebbe a risolvere il problema: ci sarebbe un'altra, simile affermazione di Gödel costruibile nel sistema allargato.

Secondo Roger Penrose questa differenza tra «ciò che può meccanicamente essere dimostrato» e «ciò che può essere riconosciuto come vero dagli uomini» mostra che l'intelligenza umana non ha una natura algoritmica. Questa convinzione è sottoscritta anche da JR Lucas in Minds, Machines and Gödel Archiviato il 6 maggio 2018 in Internet Archive..

Questa opinione non è generalmente condivisa perché, come ha sostenuto Marvin Minsky, l'intelligenza umana può commettere errori e può comprendere affermazioni che sono in realtà incoerenti o false. Ciò nonostante, Marvin Minsky ha raccontato che Kurt Gödel gli disse personalmente della sua convinzione nel fatto che gli esseri umani possiedono una modalità intuitiva, non solo computazionale, per arrivare alla verità e che quindi il suo teorema non pone limiti a ciò che può essere riconosciuto come vero dall'uomo.

La questione se il teorema mostrerebbe la capacità degli uomini di trascendere la logica formale trapassa dalla matematica alla filosofia. Se veramente non fosse possibile sapere dall'esterno se l'affermazione p è vera nel caso in cui il sistema è coerente, cadrebbe la possibilità di prestare fede anche al teorema stesso.

Tutto ciò che si può conoscere stando invece all'interno del sistema è la verità della seguente affermazione:

O p non è dimostrabile nel sistema, oppure il sistema non è coerente.

Questa affermazione può facilmente essere dimostrata all'interno del sistema. Infatti, tale dimostrazione sarà ora schematicamente delineata.

Il problema principale che deve essere affrontato per sviluppare l'idea di dimostrazione precedentemente formulata è il seguente: per costruire un enunciato p che sia equivalente a "p non può essere dimostrato", p deve in qualche modo contenere un riferimento a p, ovvero a se stesso, il che potrebbe dare facilmente origine ad un processo infinito di autoreferenziamento. Il geniale stratagemma di Gödel, utilizzato successivamente anche da Alan Turing per risolvere l'Entscheidungsproblem, è il seguente.

Per cominciare, ad ogni formula o enunciato che può essere formulato nel sistema è assegnato un numero univoco, che è chiamato il suo numero di Gödel. Ciò è fatto in modo che si possa facilmente effettuare una conversione meccanica tra le formule e i relativi numeri di Gödel, e viceversa. Dato che il sistema considerato è abbastanza potente da poter operare con i numeri, sarà ora possibile operare allo stesso modo anche con le formule.

Una formula F(x) che contiene una sola variabile libera x è chiamata forma dichiarativa. Quando a x si sostituisce uno specifico numero, la forma dichiarativa si trasforma in un enunciato, potenzialmente vero o falso, che può essere o non essere dimostrabile nel sistema. Le forme dichiarative non sono enunciati e quindi non possono essere dimostrate vere o false. Comunque, ogni forma dichiarativa F(x) ha un suo numero di Gödel che si può denotare con la scrittura G(F). La scelta della variabile libera utilizzata nell'espressione F(x) non è rilevante per l'assegnazione del numero di Gödel G(F).

A partire da un'analisi attenta degli assiomi e delle regole del sistema, si può costruire una forma dichiarativa P(x) che traduce il seguente concetto: x è il numero di Gödel di un enunciato che può essere dimostrato nel sistema. Formalmente: P(x) può essere dimostrata se x è il numero di Gödel di un enunciato dimostrabile, e la sua negazione ¬P(x) può essere dimostrata se non lo è.

(Anche se la precedente descrizione può essere ritenuta sufficiente a delineare lo schema della dimostrazione, essa è tecnicamente non del tutto accurata. Si veda l'articolo di Gödel per l'esposizione del problema e quello di Rosser per la sua risoluzione. La parola chiave è "omega-coerenza".)

A questo punto interviene l'idea risolutiva: chiamiamo auto-indimostrabile una formula che afferma meta-matematicamente la propria non dimostrabilità. Applicando questa definizione, una forma dichiarativa F(x) è auto-indimostrabile se la forma F, applicata al suo stesso numero di Gödel, non è dimostrabile. Questo concetto può essere definito formalmente, dato che si può costruire una forma dichiarativa SU(z) la cui interpretazione dice che z è il numero di Gödel di una forma dichiarativa auto-indimostrabile. Formalmente, SU(z) è definita come: sia F(x) la formula per cui si ha z = G(F), e sia y è il numero di Gödel dell'enunciato F(G(F)), allora SU(z) = ¬P(y). A questo punto, l'enunciato cercato p, precedentemente introdotto può essere definito come:

p = SU(G(SU)).

Intuitivamente, quando ci si chiede se p è vero, ci si pone la domanda: "La proprietà di essere auto-indimostrabile è di per sé stessa auto-indimostrabile?" Tutto ciò ricorda molto da vicino il paradosso del barbiere che racconta di quel barbiere che rade unicamente quelle persone che non si radono da sole: chi rade il barbiere?

Assumiamo ora che il nostro sistema assiomatico sia coerente.

Se p fosse dimostrabile, allora SU(G(SU)) sarebbe vero, e per la definizione di SU, z = G(SU) sarebbe il numero di Gödel di una forma proposizionale auto-indimostrabile. Pertanto SU sarebbe auto-indimostrabile, e ciò implica, per la stessa definizione di auto-indimostrabilità che SU(G(SU)) non è dimostrabile, ma questo è il nostro enunciato p: p non è dimostrabile. Questa contraddizione porta a concludere che p non può essere dimostrabile.

Se la negazione di p= SU(G(SU)) fosse dimostrabile, allora per la definizione di SU ciò significherebbe che z = G(SU) non è il numero di Gödel di una forma auto-indimostrabile, il che implica che SU non è auto-indimostrabile. Per la definizione di auto-indimostrabilità, si conclude che SU(G(SU)) è dimostrabile, e quindi p è dimostrabile. Ancora una volta si giunge a una contraddizione. Quest'ultima contraddizione implica che anche la negazione di p non può essere dimostrata.

Quindi l'enunciato p non può essere né dimostrato né confutato all'interno del nostro sistema.

Sia p l'enunciato indecidibile costruito prima, e si assuma che la coerenza del sistema sia dimostrabile all'interno del sistema stesso. Precedentemente si è mostrato che se il sistema è coerente, allora p non è dimostrabile. La dimostrazione di questa implicazione può essere formalizzata nel sistema stesso, e quindi l'affermazione "p non è dimostrabile", o "¬P(p)" può essere dimostrata nel sistema.

Ma quest'ultima affermazione è equivalente allo stesso enunciato p (e questa equivalenza può essere dimostrata nel sistema), quindi p può essere dimostrato nel sistema. Questa contraddizione implica che il sistema deve essere incoerente.

• Italo Aimonetto, Il fondamento del teorema di Gödel: da Peano a Frege e Russell - Rivista Filosofia - Torino
• Francesco Berto, Tutti pazzi per Godel, Laterza, 2008 (ISBN 978-88-420-8590-4)
• John L. Casti, Werner DePauli, Gödel, l'eccentrica vita di un genio, Raffaello Cortina (ISBN 88-7078-711-7)
• Alfred Driessen, "Philosophical consequences of the Gödel theorem", in Human Approach to the Universe, Ed. Eeva Martikainen, Luther-Agricola-Society, 2005, Helsinki, pp. 66-74.
• Hao Wang: A Logical Journey: From Gödel to Philosophy Bradford Books (10 gennaio 1997) ISBN 0-262-23189-1
• Douglas Hofstadter, Gödel, Escher, Bach: un'eterna ghirlanda brillante, Adelphi (ISBN 88-459-0755-4)
• E. Nagel, J.R. Newman, La prova di Gödel, Universale Bollati Boringhieri (ISBN 88-339-0309-5)
• P. Pasolini, Il teorema di Gödel di fronte alla logica, alla cibernetica e all'assoluto - Rivista Nuova Umanità n. 1, Ed. Città Nuova, Roma
• Maurizio Cotti Piccinelli, Il teorema di Gödel. Un trattato sulla conoscenza, Il Melangolo 2018, ISBN 978-88-6983-168-3
• B. Rosser: Extensions of some theorems of Gödel and Church. Journal of Symbolic Logic, 1 (1936), N1, pp. 87–91

• Autoreferenza
• Coerenza logica
• Logicismo
• Macchina Gödel-incompleta
• Paradosso di Berry
• Paradosso di Richard
• Paradosso di Russell
• Prova ontologica di Gödel
• Raymond Smullyan
• Teorema di completezza di Gödel
• Teoria del primo ordine

• Wikiquote contiene citazioni sui teoremi di incompletezza di Gödel
• Wikibooks contiene testi o manuali sui teoremi di incompletezza di Gödel

• (EN) William L. Hosch, incompleteness theorem / logic, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
• (EN) Panu Raatikainen, Gödel’s Incompleteness Theorems, su Stanford Encyclopedia of Philosophy.
• (EN) Opere riguardanti Teoremi di incompletezza di Gödel, su Open Library, Internet Archive.
• (DE) Kurt Gödel: Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme, I. Monatshefte für Mathematik und Physik, 38 (1931), pp. 173–198. Translated in van Heijenoort: From Frege to Gödel. Harvard University Press, 1971.
• (EN) J.R. Lucas: Minds, Machines and Gödel Archiviato il 19 agosto 2007 in Internet Archive.
• (EN) Kārlis Podnieks: Around Goedel's Theorem, http://www.ltn.lv/~podnieks/gt.html
• (EN) Voce su "Kurt Gödel" in MacTutor History of Mathematics Archive, su www-gap.dcs.st-and.ac.uk. URL consultato il 20 aprile 2005 (archiviato dall'url originale il 24 marzo 2005).
• (EN) Hilbert's second problem (English translation)

Portale Filosofia

Portale Matematica