Teorema di Godel per riduzione dal problema della Fermata

[CUCU]

Sia TN l'insieme delle formule ben formate dell'aritmetica (Teoria dei Numeri).
Sia TR l'insieme delle sentenze (formule ben formate con nessuna variabile libera) vere dell'aritmetica (TRue).
Una sentenza G appartenente a TR è o vera o falsa ma non entrambe.
Una regola di inferenza R1 è un predicato (n+1)-ario R1(F1,F2,...,Fn+1) su TN.
Un sistema formale è una coppia ordinata F=(AX,R), dove AX incluso in TR è denominato un insieme di assiomi, and R è un insieme finito di regole d'inferenza (nota che imponiamo la finitezza di R) tale che se R1 appartiene ad R e
R(F1,F2,...,Fn+1) è vero e F1,F2,...,Fn appartengono a TR allora Fn+1 appartiene a TR (si dice in questo caso che la regola d'inferenza è "sound", ossia che preserva la verità).
Se R1 è una regola d'inferenza in R, e R1(F1,F2,...,Fn+1) è vero diremo che Fn+1 è provabile da F1,F2,....Fn per mezzo di R1.

Una sentenza G è un teorema d F=(AX,R) se G è un assioma o G è provabile per mezzo di una regola d'inferenza in R o dagli assiomi o da teoremi già provati.

Sia THM(F) l'insieme dei teoremi di F.

Un sistema formale è completo se e solo se ogni formula appartenente a TR è provabile.

Un sistema formale F=(AX,R) è ricorsivo se sia AX che R sono ricorsivi.
Stiamo assumendo implicitamente una numerazione di godel (ossia un'aritmetizzazione delle formule). Se P è una formula, definiamo con gn(P) il numero di godel di P.

Il predicato che asserisce "la macchina di Turing il cui numero di godel è z con input i si ferma in esattamente y mosse" è definibile dalla formula T(z,i,y), ossia possiamo scrivere nel linguaggio dell'aritmetica una formula che è vera se e solo quando è vero questo predicato (è un fatto ben noto dalla teoria della computabilità).

L'insieme { (z,i) | Esiste y T(z,i,y) } è ricorsivamente enumerabile ma NON ricorsivo (è il problema della Fermata Generale di Turing, e la dimostrazione è un risultato ben noto della teoria della calcolabilità).


THM(P) è ricorsivamente enumerabile: non presenterò una dimostrazione formale ma è un risultato ben noto ed è intuitivamente evidente dal momento che basta enumerare gli assiomi, poi tutti i teoremi provabili con una sola applicazioni di una regola di inferenza, e così via.


Teorema di Godel
Se F è un sistema formale ricorsivo allora F è incompleto.

Supponiamo che per assurdo F sia completo.
Ogni sentenza "Esiste y T(z,i,y)" è o vera o falsa e non entrambe.
Se è vera allora per la completezza "Esiste y T(z,i,y)".
Se è falsa, allora è vera "NOT Esiste y T(z,i,y)" e per la completezza "NOT Esiste y T(z,i,y)" è un teorema.

Dal momento che THM(F) è ricorsivamente enumerabile, allora, per un ben noto teorema (o a volte lo si pone per definizione) della t.c., esiste un predicato calcolabile P tale che x appartiene a THM(F) se e solo se Esiste y P(y,x).

(z,i) appartiene a { (m,n) | Esiste y T(m,n,y) }
se e solo se
Esiste y T(z,i,y) appartiene a TR
se e solo se
Esiste y T(z,i,y) è provabile
se e solo se
gn("Esiste y T(z,i,y)") appartiene a THM(F)
se e solo se
Esiste y P(y,a(z,i)), dove a è la funzione (totalmente) calcolabile che manda (z,i) in gn("Esiste y T(z,i,y)") .



(z,i) appartiene a COMPLEMENTO di { (m,n) | Esiste y T(m,n,y) }
se e solo se
"Esiste y T(z,i,y)" NON appartiene a TR
se e solo se
"Esiste y T(z,i,y)" NON è provabile
se e solo se
"NOT Esiste y T(z,i,y)" è provabile
gn("NOT Esiste y T(z,i,y)") appartiene a THM(F)
se e solo se
Esiste y P(y,b(z,i)), dove b è la funzione (totalmente) calcolabile che manda (z,i) in gn("NOT Esiste y T(z,i,y)").

Allora la funzione h(z,i)= min y [P(y,a(z,i)) o P(y,b(z,y))] è totale e quindi calcolabile.
Ma allora (z,i) appartiene a { (m,n) | Esiste y T(m,n,y) }
se e solo se
P(h(z,i),z,i).

Così l'insieme { (m,n) | Esiste y T(m,n,y) } è ricorsivo.
Assurdo.
Ciò conlude la dimostrazione.