Visualizza wikitesto di Teoremi di incompletezza di Gödel

{{NN|matematica|giugno 2020}}
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.<ref>John W. Dawson, Jr., ''Logical Dilemmas: The Life and Work of Kurt Gödel'', p. 70, A. K. Peters, Wellesley Mass, 1997.</ref> Essi fanno parte dei ''teoremi limitativi'', che precisano le proprietà che i [[Sistema formale|sistemi formali]] non possono avere.

== Primo teorema di incompletezza ==

Sia P una formalizzazione dell'[[aritmetica di Peano]].

Con il '''teorema di incompletezza''' di [[Kurt Gödel|Gödel]] si è dimostrato che tale teoria risulta [[Completezza_(logica_matematica)|completa]] per i soli [[Assioma logico|assiomi logici]], ossia: per ogni formula "R", esiste una formula ad essa corrispondente "r" tale che:

* se <math>R(x)</math> sussiste <math>\rightarrow P \vdash r(x)</math>;
* se <math>R(x)</math> non sussiste <math>\rightarrow P \vdash \lnot r(x)</math>.

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

: ''In ogni teoria matematica'' '''T''' ''sufficientemente espressiva da contenere l'aritmetica, esiste una [[formula ben formata|formula]] <math>\varphi</math> tale che, se'' '''T''' ''è [[Coerenza (logica matematica)|coerente]], allora né <math>\varphi</math> né la sua negazione <math>\lnot \varphi</math> sono [[dimostrabilità (logica matematica)|dimostrabili]] in'' '''T'''''.''

Con qualche semplificazione, il primo teorema afferma che:

:''In ogni formalizzazione [[Coerenza (logica matematica)|coerente]] della matematica che sia sufficientemente potente da poter [[Assioma (matematica)|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.''<ref>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 <math>P\vdash G</math>, 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.</ref>

Intuitivamente, la dimostrazione del primo teorema ruota attorno alla possibilità di definire una formula logica <math>\varphi</math> che neghi la propria dimostrabilità: si prova quindi che, affinché '''T''' sia coerente, né <math>\varphi</math> né <math>\lnot \varphi</math> 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 [[Rappresentabilità (logica matematica)|rappresentare]] tutte le [[funzione ricorsiva primitiva|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|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.

== 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 reale|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 [[dimostratore automatico dei teoremi|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 (matematica)|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 [[Insieme ricorsivo|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 [[decidibilità|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 (matematico)|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 della fermata|problema dell'arresto]] — se cioè una [[macchina di Turing]] si arresta eseguendo un certo programma — è indecidibile. Questo risultato fu successivamente generalizzato nel campo delle [[funzione ricorsiva|funzioni ricorsive]] con il [[teorema di Rice]] che mostra come tutti i problemi non banali di decisione sono indecidibili in un sistema [[Turing completo|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 (matematica)|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.

== Fraintendimenti sul teorema di incompletezza di Gödel ==
L'ampia discussione sul primo teorema ha prodotto molti fraintendimenti. Qui chiariamo i più comuni.
<!--
TOLGO LA PARTE SOTTO

# Il teorema non implica che ogni sistema di assiomi abbastanza interessante sia incompleto. Ad esempio la [[geometria euclidea]] può essere assiomatizzata in modo da essere un sistema completo.  (Di fatti, gli assiomi originali di [[Euclide]] si avvicinano molto all'essere un'assiomatizzazione completa. Gli assiomi mancanti esprimono proprietà talmente ovvie che se ne è notata la mancanza solamente nel momento in cui è sorta l'esigenza di scrivere dimostrazioni formali.)

In realtà, l'assiomatizzazione della geometria sposta il problema della completezza dalla geometria all'aritmetica: infatti è possibile rappresentare l'aritmetica nella geometria: se questa fosse completa, lo sarebbe anche l'aritmetica, in contraddizione con il primo teorema. Un po' come la rappresentazione delle geometrie non euclidee con cerchi e linee sposta la correttezza di queste a quella della geometria euclidea.
--> 
# 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 "<math>x</math> è un numero naturale". Molti sistemi che contengono i numeri naturali sono completi; i [[numeri reali]] e i [[numeri complessi]] hanno assiomatizzazioni complete. 
# È 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 [[Numero transfinito|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.
# 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.

== Discussioni e implicazioni ==

Le conseguenze dell'incompletezza influenzano la [[filosofia della matematica]], e in particolare alcune sue scuole di pensiero, come il [[filosofia della matematica#Formalismo|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'[[ordine lessicografico|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 [[Insieme ricorsivamente enumerabile|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 bugiardo|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'' è «[[verità|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ò [[meccanismo|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 ''[https://web.archive.org/web/20180506135515/http://users.ox.ac.uk/~jrlucas/mmg.html Minds, Machines and Gödel] {{Webarchive|url=https://web.archive.org/web/20180506135515/http://users.ox.ac.uk/~jrlucas/mmg.html |date=6 maggio 2018 }}''.

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à [[intuizione|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 [[trascendenza|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.
{{citazione|Il principio di Godel è applicabile solo ai sistemi strettamente formali, ma noi non siamo sempre inseriti in un sistema formale, non portiamo avanti un monologo, come fa un sistema formale, siamo animali dialogici. Il problema è [[semantica|semantico]] e non sintattico, e si può dimostrare che il principio di Godel non è applicabile ad un universo semantico.|[[Heinz von Foerster]] <ref>Trad. it. in Mauro Maldonato, '' Certe estremità della coscienza. Scritti sul sentimento del limite'', Effata Editrice, 2005</ref>}}

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.

== Schema della dimostrazione del primo teorema ==
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''&nbsp;=&nbsp;''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''&nbsp;=&nbsp;'''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''&nbsp;=&nbsp;'''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.

== Schema della dimostrazione del secondo teorema ==

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.

== Note ==
<references/>

== Bibliografia ==
* 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, "[https://www.academia.edu/25087365/Philosophical_consequences_of_the_Gödel_Theorem 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.&nbsp;87–91

== Voci correlate ==
* [[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]]

== Altri progetti ==
{{interprogetto|q|b=Logica/Incompletezza/Teoremi_di_incompletezza_di_Gödel|preposizione=sui}}

== Collegamenti esterni ==
* {{Collegamenti esterni}}
* {{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.&nbsp;173–198. Translated in van Heijenoort: ''From Frege to Gödel''. Harvard University Press, 1971.
* {{en}}J.R. Lucas: [http://users.ox.ac.uk/~jrlucas/Godel/mmg.html Minds, Machines and Gödel] {{Webarchive|url=https://web.archive.org/web/20070819165214/http://users.ox.ac.uk/~jrlucas/Godel/mmg.html |date=19 agosto 2007 }}
* {{en}}Kārlis Podnieks: ''Around Goedel's Theorem'', http://www.ltn.lv/~podnieks/gt.html
* {{cita web|1=http://www-gap.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html|2=Voce su "Kurt Gödel" in ''MacTutor History of Mathematics Archive''|lingua=en|accesso=20 aprile 2005|urlarchivio=https://web.archive.org/web/20050324025823/http://www-gap.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html|dataarchivio=24 marzo 2005|urlmorto=sì}}
* {{en}}[http://aleph0.clarku.edu/~djoyce/hilbert/problems.html#prob2 Hilbert's second problem] (English translation)

{{Controllo di autorità}}
{{Portale|filosofia|matematica}}
[[Categoria:Kurt Gödel]]
[[Categoria:Teoremi nella teoria della computazione|Incompletezza, Gödel]]
[[Categoria:Filosofia della matematica]]