Logica matematica/Incompletezza/Teoremi di incompletezza di Gödel: differenze tra le versioni

Contenuto cancellato Contenuto aggiunto
Riga 92:
 
:<math>\gamma(y)\equiv \neg\exists x
\text{Dim}_S(x,\text{sost}(y,\text{g}('y'),y))</math>
 
<math>\gamma(y)</math> afferma che non esiste una dimostrazione in <math>S</math> per la formula ottenuta dalla formula di gödeliano <math>y</math>, sostituendo (all'interno di essa) le occorrenze libere della variabile il cui gödeliano è <math>g('y')</math> (cioè <math>y</math>) con il gödeliano della formula stessa, cioè <math>y</math>. In breve, essa afferma che la formula ottenuta da tale sostituzione non è dimostrabile.
 
Supponiamo ora che <math>q</math> sia il gödeliano di <math>\gamma(y)</math>, cioè: <math>q=g('\gamma(y)')</math>.
 
Eseguiamo la seguente sostituzione su <math>\gamma(y)</math>: sostituiamo la variabile <math>y</math> con il numerale di <math>q</math>. Otteniamo così la formula chiusa <math>\gamma</math>:
Riga 102:
:<math>\gamma\equiv \neg\exists x
\text{Dim}_S(x,\text{sost}(\overline q,
\text{g}('y'),\overline q))</math>
 
<math>\gamma</math> afferma che non esiste una dimostrazione in <math>S</math> per la formula ottenuta dalla formula di gödeliano <math>q</math>, sostituendo (all'interno di essa) le occorrenze libere della variabile <math>y</math> con il gödeliano della formula stessa, cioè <math>q</math>. In pratica, <math>\gamma</math> afferma che la formula che si ottiene tramite tale sostituzione non è dimostrabile, ma tale formula è esattamente <math>\gamma</math>, dato che <math>\gamma \equiv \gamma(y)[\overline{q}/y]</math>, quindi abbiamo che <math>g('\gamma')=sost(q,
g('y'),q)</math>. Dunque, <math>\gamma</math> afferma di non essere un teorema, cioè, è l'aritmetizzazione dell'enunciato metamatematico che afferma l'indimostrabilità di <math>\gamma</math>.
 
# Supponiamo che valga <math>\vdash_S \gamma</math>, allora esiste un <math>x</math> tale per cui esso è il gödeliano di una dimostrazione di <math>\gamma</math>. Essendo <math>Dim_S</math> rappresentabile in <math>S</math>, vale <math>\vdash_S \exists x
\text{Dim}_S(x,\text{g}('\gamma'))</math>. Ma, essendo che <math>g('\gamma')=sost(q,
g('y'),q)</math>, abbiamo che <math>\vdash_S \exists x
\text{Dim}_S(x,\text{sost}(\overline q,
\text{g}('y'),\overline q))</math>, dunque <math>\vdash_S \neg\gamma</math>. Perciò, se <math>\gamma</math> è dimostrabile, allora <math>S</math> è incoerente.
# Supponiamo che <math>S</math> sia ω-coerente, ma che, per assurdo, valga <math>\vdash_S \neg\gamma</math>, allora abbiamo che <math>\vdash_S \exists x
\text{Dim}_S(x,\text{g}('\gamma'))</math>. Essendo <math>S</math> ω-coerente, per il [[Logica/Incompletezza/Teoremi di incompletezza di Gödel#Lemma di coerenza|lemma di coerenza]] esso è anche coerente, dunque, per il punto 1, vale <math>\nvdash_S \gamma</math>, cioè <math>\nvdash_S \neg\exists x
\text{Dim}_S(x,\text{g}('\gamma'))</math>. Quindi, essendo <math>Dim_S</math> rappresentabile in <math>S</math>, abbiamo che, per ogni <math>n</math>, <math>\vdash_S \neg\text{Dim}_S(\overline{n},\text{g}('\gamma'))</math>. Dunque, valendo sia <math>\vdash_S \exists x
\text{Dim}_S(x,\text{g}('\gamma'))</math> che <math>\vdash_S \neg\text{Dim}_S(\overline{n},\text{g}('\gamma'))</math> per ogni <math>n</math>, segue che <math>S</math> è ω-incoerente, contraddicendo l'ipotesi iniziale.
 
Perciò, se <math>S</math> è ω-coerente, allora <math>\gamma</math> è indecidibile all'interno di <math>S</math> stesso.