Dato che il teorema di Gödel ricorre spesso in questo NG, ho pensato che possa essere utile cercare di spiegare che cosa veramente dice questo teorema.
Dato che non sono né un logico né un matematico, non garantisco di non commettere errori: vuol dire che qualcuno mi correggerà...
Inoltre dovrò saltare passaggi anche importanti. Gli esperti mi scuseranno o completeranno il quadro.

La storia comincia nei primi anni del 20-mo secolo, quando sulla scia delle ricerche di Cantor, di Russell, ecc. ferve la discussione circa la possibilità di "provare rigorosamente" qualcosa in matematica, o anche di precisare che cosa sia una dimostrazione. O ancora: di dimostrare che un sistema assiomatico è non contraddittorio.

Hilbert propone questa strada: formalizzare rigorosamente le dimostrazioni.
La tecnica da seguire è oggi molto familiare, grazie all'informatica, che però allora era assai di là da venire. Si tratta in primo luogo di scrivere tutte le proposizioni matematiche in un linguaggio preciso, del tutto privo di ambiguità, come "stringhe" di simboli di un certo alfabeto.
In questo spirito le proposizioni non vanno viste come dotate di significato (interpretate), ma solo per la loro struttura sintattica, ossia per le relazioni fra i simboli. Ancora una volta, l'analogia informatica aiuta: un programma scritto in un linguaggio come BASIC, C, PASCAL ha per noi un significato; ma il compilatore che deve tradurlo in linguaggio macchina si occupa in primo luogo della correttezza sintattica (ci sono i ";" al posto giusto? le parentesi aperte sono anche chiuse? le variabili sono state dichiarate? ecc.).

Una volta ridotte le proposizioni a stringhe, si debbono introdurre gli "assiomi", che sono soltanto proposizioni di partenza, che non vogliamo dimostrare. Poi dobbiamo dare le "regole di deduzione", ossia i procedimenti coi quali è lecito "dedurre" una proposizione da un'altra. Per esempio: se la proposizione "a = a" è un assioma (o se è già stata dimostrata) è lecito sostituire alla variabile "a" qualsiasi espressione corretta: potrò quindi dare per dimostrato ad es. "b+c/7=b+c/7". Ci sono (ci vogliono) regole di deduzione più "furbe" di questa regola di sostituzione, ma non occorre qui precisare quali potranno essere.
Una successione finita di applicazioni di regole di deduzione a partire dagli assiomi termina in una proposizione finale: questa proposizione è un "teorema", e la successione si chiama la "dimostrazione" del teorema.

Una volta fatto questo (formalizzata una teoria, che può essere la geometria euclidea, l'aritmetica elementare, o altro) ci si può porre alcune domande, di cui quelle centrali sono:
1) la teoria è coerente?
2) la teoria è completa?
Coerente è lo stesso che "non contraddittoria": vuol dire che non è possibile che siano teoremi (quindi dimostrabili) una proposizione e la sua negazione.
Completa vuol dire che è possibile dimostrare tutte le proposizioni "vere". Questa seconda asserzione va spiegata, perché il termine "vero" appartiene a un diverso livello di discorso.

Il fatto è che la teoria che abbiamo formalizzata ha di solito un'interpretazione (la geometria parla di rette, angoli...) e in questa interpretazione certe proposizioni potranno essere vere o false, indipendentemente dal fatto che ci sia riuscito di trovarne una dimostrazione. (So bene che qui si sfiora un grosso problema, che ci porta non solo alla semantica, appena si parla d'interpretazione, ma anche alla filosofia. Per es.: ha senso parlare di una verità diversa da quella esprimibile con le dimostrazioni formali? Mi accontento di questa osservazione: chiunque fa matematica ragiona per lo più in modo non formale, ed è convinto della validità delle sue conclusioni. Quindi esiste una verità, almeno nella pratica, che non si riduce a quella formale.)

Le due domande centrali che dicevo sopra hanno un'altra caratteristica comune: sono domande metamatematiche. Non mi sto chiedendo se "la somma dei quadrati dei cateti..." ossia se una certa proposizione matematica è vera; sto chiedendo se vale una certa proprietà di una teoria matematica. Ossia guardo la matematica "dal di fuori", "dal di sopra".
L'obbiettivo formalistico di Hilbert si può riassumere così: formalizzare non solo la matematica, ma anche la metamatematica, ossia dare dimostrazioni formali delle risposte a quelle due domande (e ad altre consimili).

E qui arriva Gödel, a rompere le uova nel paniere...
Non posso che riportare in forma "divulgativa" il risultato del suo lavoro, che appare nel 1931, col titolo Über formal unentscheidbare Sätze der "Principia mathematica" und verwandter Systeme (sulle proposizioni formalmente indecidibili dei "Principia matematica" e sistemi affini).
Richiamo l'attenzione su due parole: "formalmente indecidibili"; poi vedremo perché. I "Principia mathematica" sono un trattato di logica matematica di Whitehead e Russell: una pietra miliare della ricerca di cui dicevo all'inizio, ma non abbiamo bisogno di occuparcene.

In sostanza si tratta di questo: con un lavoro faticoso quanto geniale, Gödel riesce a costruire una proposizione del sistema formale dell'aritmetica, che indicherò con G, la cui interpretazione è semplicemente

Notare che l'incompletezza non è un problema, come non lo è per la geometria. Se alla geometria euclidea togliete il postulato delle parallele, sappiamo che questo non può essere dimostrato a partire dagli altri. Abbiamo allora due vie:
a) aggiungere il nuovo postulato (e abbiamo la geometria euclidea)
b) aggiungere un postulato diverso, che nega quello (e abbiamo la geometria non euclidea).

Sull'esposizione del teorema di Gödel mi fermo qui.

Solo un commento: molto spesso il teorema di Gödel viene citato a sproposito, dimenticando la parola chiave del titolo. Ricordate? "formalmente indecidibili". Tutto ruota attorno a quel formalmente, che ora sappiamo che cosa significa.
Gödel ci ha dimostrato che esistono proposizioni formalmente indecidibili (e non solo nell'aritmetica, ma in tutti i sistemi formali utili alla matematica). Ma non ci ha vietato di dare dimostrazioni non formali, come facciamo sempre.
Il prezzo che si paga è che non possiamo essere certi del rigore che garantisce una dimostrazione formale. O in altre parole: in una dimostrazione non formale probabilmente usiamo delle regole di deduzione più ricche di quelle che sappiamo formalizzare.

Perciò non è giusto dire che la congettura di Goldbach (o altre proposizioni: era stato supposto anche del teorema di Fermat, ora dimostrato) possa essere indecidibile, rifacendosi al teorema di Gödel. Di fatto per la quasi totalità dei teoremi della matematica che conosciamo nessuno ha mai neppure provato a scrivere dimostrazioni formali, per cui la possibile inesistenza di tali dimostrazioni non cambia niente. E infatti dopo Gödel i matematici non hanno cambiato mestiere, hanno continuato a riscuotere lo stipendio (Gödel incluso) ecc.
Né la difficoltà di trovare una dimostrazione (o la dimostrazione della negazione) di una congettura dice niente circa la sua indecidibilità formale; e di indecidibilità "non formale" non ha neppure senso parlare.

Sto dicendo che il teorema di Gödel è inutile? Niente affatto.
In primo luogo, ha chiarito lo status logico delle teorie e delle dimostrazioni matematiche: quello che si può e quello che non si può pretendere/raggiungere.
In secondo luogo - questo è il punto di vista malizioso di un fisico, lo ammetto ;-) - dovrebbe aver insegnato ai matematici un po' di modestia: non possono più guardare dall'alto in basso gli altri scienziati, ritenendosi i soli e veri depositari di un rigore inattaccabile.
Rifiuto invece le interpretazioni (care a certi filosofi) circa la pretesa prova dei limiti della ragione umana, inconoscibilità della verità, e palle consimili. Queste interpretazioni sono semplicemente forzature, derivanti da un'accoppiata di ignoranza e malafede: ignoranza, perché nessuno di quelli che parlano cosí ha mai provato a capire il teorema di Gödel sul serio (e non ne sarebbero capaci!); malafede, perché cercano solo di volgere a vantaggio di una propria tesi (sempre antiscientifica) qualcosa che ha un altro significato.