I teoremi di incompletezza di Gödel

Kurt Gödel

Introduzione

In questa nota saranno descritti i due teoremi di incompletezza di Gödel. Innanzitutto introduciamo alcuni concetti di base, senza dei quali sarebbe impossibile enunciare e spiegare i due teoremi.

Logica matematica

La logica matematica è la scienza che si occupa di studiare il modo di codificare i calcoli e le dimostrazioni effettuate nell'ambito di una logica formale.

Ma cos'è una logica formale? È un insieme di:

un alfabeto utilizzato;
una grammatica che specifica quali sequenze costituiscono "formule" del sistema;
un insieme di "assiomi", ossia, intuitivamente, formule che nel sistema si assumono vere;
un insieme di regole di inferenza, ognuna delle quali associa a $N$ formule del sistema (premesse) una nuova formula (conseguenza).

In un sistema formale si definisce l'insieme dei teoremi come l'insieme degli assiomi unito a tutte le formule che si possono ottenere dall'applicazione delle regole di inferenza agli assiomi stessi e alle altre formule ottenute, ricorsivamente.

Logica proposizionale

È un linguaggio formale che consente di esprimere proposizioni booleane elementari o composte, basato sui connettivi logici (and, or, not, implica, se e solo se) e su un insieme di simboli.

Possiamo quindi dire che è una logica formale avente per alfabeto le lettere, unite ai connettivi $\neg$ (NOT), $\wedge$ (AND), $\vee$ (OR), $\rightarrow$ (implicazione), $\leftrightarrow$ (doppia implicazione), e le parentesi tonde, usate per evitare ambiguità sull'applicazione dei connettivi.

Per insieme di regole di inferenza abbiamo:

una proposizione è una formula ben formata (fbf);
se $A$ è una fbf, allora anche $\neg A$ è una fbf;
se $A$ e $B$ sono fbf, allora anche $(A \vee B)$, $(A \wedge B)$, $(A \leftrightarrow B)$, $(A \rightarrow B)$ sono fbf;
tutto il resto non è una fbf.

Alle fbf della logica proposizionale è possibile associare una semantica mediante una funzione di valutazione: una funzione che va dall'insieme $L$ delle fbf nell'insieme $\{V, F\}$,

$$v : L \longrightarrow \{\,V,\ F\,\}$$

tale che:

$$\begin{align} v(\neg x) &= V \quad\text{se } v(x) = F \\ v(\neg x) &= F \quad\text{se } v(x) = V \\ v(x \wedge y) &= V \iff v(x) = V \text{ e } v(y) = V \\ v(x \vee y) &= V \iff v(x) = V \text{ oppure } v(y) = V \\ v(x \rightarrow y) &= V \iff v(x) = F \text{ oppure } v(y) = V \\ v(x \leftrightarrow y) &= V \iff v(x) = v(y) \end{align}$$

che attribuiscono ai connettivi logici il significato consueto.

Per attribuire il valore a una fbf in base alla funzione di valutazione, si assegna alle proposizioni elementari un valore di vero/falso e poi, a partire da quelle, si calcolano tutte le altre risalendo le parentesi dalle più interne.

Un limite della logica proposizionale è che, se si vuole esprimere il concetto "ogni $A_i$ è vero per $i$ che va da 1 a $n$", lo si può fare solo scrivendo

$$A_1 \wedge A_2 \wedge A_3 \wedge \cdots \wedge A_n$$

ma se vogliamo esprimere lo stesso concetto per un numero imprecisato o infinito di termini non possiamo farlo: in sostanza mancano i quantificatori. Inoltre nella logica proposizionale non abbiamo la possibilità di riferirci a predicati o funzioni.

Linguaggio del primo ordine

Un linguaggio del primo ordine è una logica formale in cui l'alfabeto è composto da:

simboli per variabili: $x_1, x_2, \ldots$
simboli per costanti: $a_1, a_2, \ldots$
simboli per predicati o relazioni, a ciascuno dei quali è associato il suo numero di argomenti: $P^1, Q^1, P^2, Q^2, \ldots$
simboli per funzioni, a ciascuna delle quali è associato il suo numero di argomenti: $f^1, g^1, f^2, g^2, \ldots$
simboli ausiliari: parentesi tonde e virgola;
simboli per connettivi logici (come per la logica proposizionale);
simboli per quantificatori: $\forall$ (universale) e $\exists$ (esistenziale).

Per le regole di inferenza si rimanda a Wikipedia: in sostanza sono le regole comuni con cui scriviamo in matematica le formule. È bene però osservare che:

costanti e variabili si riferiscono a un "universo del discorso" $U$;
le funzioni $f, g, \ldots$ hanno per dominio $U^n$ e per codominio $U$;
i predicati o relazioni sono sottoinsiemi di $U^n$;
i quantificatori si riferiscono a elementi di $U$.

In sostanza, con un linguaggio del primo ordine possiamo esprimere predicati su $U$ e relazioni di implicazione fra predicati su $U$. In base all'ultimo vincolo non possiamo utilizzare i quantificatori su sottoinsiemi di $U$, cioè su variabili predicative. Si dimostra che una teoria del primo ordine è sufficiente a "contenere" l'aritmetica e la teoria degli insiemi.

Un esempio di linguaggio del primo ordine è l'aritmetica di Peano.

Linguaggi del secondo ordine

Se ammettiamo la possibilità di menzionare, nel linguaggio, anche variabili e costanti che rappresentino funzioni e predicati, otteniamo un linguaggio del secondo ordine. In esso posso quindi esprimere concetti di esistenza o di universalità sui predicati, oltre che sugli elementi di $U$.

Per fare un esempio, si può esprimere che

$$\forall R\, \forall x \big(R(x) \vee \neg R(x)\big)$$

dove $R$ è un predicato generico e $x$ un elemento di $U$. Questa espressione non è ammessa in un linguaggio del primo ordine.

Consideriamo il principio del buon ordinamento dei numeri naturali, secondo il quale ogni sottoinsieme non vuoto dell'insieme dei numeri naturali ammette un minimo: per esprimerlo occorre un quantificatore esistenziale sugli insiemi, ammesso in un linguaggio del secondo ordine ma non del primo.

Se consideriamo il principio di induzione, che afferma che per una generica proprietà, se $P(0)$ è vera e se $P(n) \Rightarrow P(n+1)$, allora $P$ è vera per tutto $\mathbb{N}$, è necessario utilizzare un quantificatore universale sui predicati, e anche questo è possibile solo in una teoria del secondo ordine.

Nel linguaggio del secondo ordine si possono esprimere e generalizzare relazioni (proprietà) su $U$, ma non relazioni tra relazioni: le relazioni hanno sempre per dominio $U$ e non l'insieme delle relazioni stesse. Questo richiederebbe un linguaggio di ordine superiore.

Tra i predicati è possibile esprimere relazioni logiche con connettivi propri del linguaggio del secondo ordine, simili a quelli del primo ordine ma indicati solitamente con termini diversi per non generare confusione:

not per la negazione di un predicato
vel per l'or logico
et per l'and logico
seq per l'implicazione logica
eeq per la doppia implicazione
om per il quantificatore universale
ex per il quantificatore esistenziale

Teoria e metateoria

Si può considerare, in un linguaggio di ordine superiore al primo, "teoria" il sottoinsieme relativo alla logica proposizionale, e "metateoria" le proposizioni che si riferiscono ai predicati stessi.

Intuitivamente, per "parlare" della teoria $U$ abbiamo bisogno di una metateoria $M$, poiché $U$ non contiene in sé i nomi e le proprie regole di inferenza intese in senso astratto. Per parlare di come descriviamo la teoria abbiamo bisogno di una meta-metateoria, e via dicendo.

Completezza di una teoria

In una logica del primo ordine tutto quel che è vero è dimostrabile, e questa proprietà si definisce di completezza. In una logica del secondo ordine o superiore si acquista in espressività ma si perde la proprietà di completezza.

Vale la pena precisare subito in che senso, perché altrimenti questo risultato sembra contraddire il primo teorema di incompletezza che vedremo fra poco. Il teorema di completezza, dimostrato da Gödel nel 1929, riguarda la validità logica: dice che una formula vera in tutti i modelli di una teoria è anche derivabile dai suoi assiomi. Il teorema di incompletezza, del 1931, riguarda invece la verità in un modello particolare — l'aritmetica dei numeri naturali — e dice che esistono enunciati veri lì dentro che non sono derivabili. I due risultati non si contraddicono: il primo afferma che la deduzione del primo ordine cattura tutto ciò che segue necessariamente dagli assiomi; il secondo, che nessun insieme decidibile di assiomi riesce a fissare i naturali in modo tale che ogni verità su di essi ne segua.

Detto più formalmente, una teoria è completa se per una qualsiasi formula ben formata $\varphi$ è possibile dimostrare formalmente $\varphi$ se $\varphi$ è vera, o dimostrare formalmente $\neg\varphi$ se $\varphi$ è falsa.

Si può alternativamente dire che una teoria è completa se non esistono formule indecidibili, ossia di cui non è possibile fornire né una dimostrazione né una confutazione.

Coerenza di una teoria

Una teoria si dice coerente se non esiste alcuna formula ben formata $\varphi$ di cui sia possibile dimostrare formalmente sia $\varphi$ sia $\neg\varphi$.

La coerenza è un concetto importante poiché si può dimostrare che in una teoria incoerente si può dimostrare qualsiasi cosa, e quindi la teoria perde di significato.

ω-coerenza di una teoria

Una teoria si dice ω-coerente se non esiste nessuna formula ben formata $\varphi$ tale che si possa dimostrare al contempo

$$\forall x\, \varphi(x) \qquad\text{e}\qquad \exists x\, \neg\varphi(x)$$

La ω-coerenza è un concetto più forte della semplice coerenza. Una teoria può essere coerente ma non ω-coerente: può cioè dimostrare $\exists x\, \neg\varphi(x)$ e allo stesso tempo dimostrare $\varphi(0), \varphi(1), \varphi(2), \ldots$ per ogni singolo numerale, senza mai contraddirsi in senso stretto. Il testimone la cui esistenza viene asserita non è allora nessuno dei numeri naturali "veri", ma un elemento di un modello non standard.

Questa distinzione ha un ruolo storico preciso. La versione originale del primo teorema, quella pubblicata da Gödel nel 1931, richiede la ω-coerenza: la sola coerenza basta a mostrare che la formula autoreferenziale non è dimostrabile, ma per escludere anche che sia dimostrabile la sua negazione serve l'ipotesi più forte. Fu John Barkley Rosser, nel 1936, a costruire una formula diversa — più elaborata, che parla non solo di dimostrazioni ma anche di confutazioni — per la quale la semplice coerenza è sufficiente. È la ragione per cui oggi il teorema si enuncia quasi sempre nella forma indebolita, e per cui la ω-coerenza compare ormai solo nei testi che seguono la dimostrazione originale.

Nel seguito ricostruiamo l'argomento di Gödel, quindi nella forma che richiede la ω-coerenza.

Primo teorema di incompletezza di Gödel

TeoremaIn una teoria $T$ sufficientemente espressiva da contenere l'aritmetica, effettivamente assiomatizzabile e ω-coerente, esiste almeno una formula $\varphi$ che non può essere né dimostrata né confutata.

Effettivamente assiomatizzabile significa che esiste una procedura meccanica capace di riconoscere se una formula è un assioma di $T$. Senza questa ipotesi il teorema è falso, e il controesempio è immediato: l'insieme di tutti gli enunciati veri sui numeri naturali è per costruzione coerente e completo. Non è però un insieme di assiomi utilizzabile, perché non c'è modo di riconoscerne i membri — ed è esattamente ciò che serve per costruire il predicato $\mathrm{Dim}$ che vedremo fra poco, il quale deve poter verificare meccanicamente se una dimostrazione è corretta.

Dimostrazione

La dimostrazione si basa sulla possibilità di definire una formula logica che neghi la propria dimostrabilità. A tal fine si codifica una formula "autoreferenziale", ossia che parla di sé stessa.

Si associa a ogni simbolo dell'alfabeto della teoria un numero naturale. Quindi a una formula, che è data da un insieme di simboli, possiamo associare un numero di Gödel, pari a

$$p_1^{\,s_1}\, p_2^{\,s_2} \cdots p_n^{\,s_n}$$

ove $p_1, \ldots, p_n$ sono i primi $n$ numeri primi e $s_1, \ldots, s_n$ sono i numeri associati ai simboli della formula considerata. In sostanza abbiamo trasformato una generica formula della teoria in un numero naturale. Chiamiamo $G(\varphi)$ il godeliano della formula ben formata $\varphi$.

Visto che per ipotesi $T$ è abbastanza espressiva da contenere l'aritmetica, può trattare le formule al pari dei numeri stessi. Gli assiomi di $T$ devono essere almeno sufficienti a dimostrare alcuni enunciati fondamentali:

ogni numero naturale ha un numero di Gödel, che si ottiene applicando reiteratamente la funzione successore all'elemento 0;
dato un qualsiasi numero di Gödel di una formula $\varphi(x)$ con variabile libera $x$, e un qualsiasi numero naturale $m$, vi è un numero di Gödel associato alla formula $\varphi(G(m))$, ottenuto sostituendo le occorrenze di $x$ in $\varphi(x)$ con il numero di Gödel associato a $m$.

Dette $D_1, \ldots, D_n$ le regole di deduzione della teoria, supponiamo che $D_1$ consenta di passare dalle formule $a_1$ e $a_2$ di $T$ a una nuova formula $a_3$. Si avrà che il numero di Gödel della sequenza $a_1, a_2$, che chiamiamo $n$, e il numero $m$ associato alla formula $a_3$ saranno in relazione $R_1$ tra loro, ossia $(n,m) \in R_1$. Sarà pertanto possibile verificare meccanicamente se una dimostrazione è corretta, controllando nei vari passaggi se i corrispondenti numeri naturali sono in relazione tra loro.

Definiamo $H$ l'insieme dei numeri di Gödel di tutti gli enunciati dimostrabili. Per quanto detto, $H$ è chiuso relativamente alle relazioni binarie $R_1, \ldots, R_n$ associate alle regole di deduzione $D_1, \ldots, D_n$: se $n$ è nell'insieme $H$ e $(n,m)$ è elemento di $R_i$, allora anche $m$ appartiene ad $H$, ossia è dimostrabile.

Attraverso una serie di passi, Gödel costruisce un predicato metamatematico

$$\mathrm{Dim}(y, x)$$

che rappresenta la relazione "$y$ è il godeliano di una dimostrazione della formula di godeliano $x$", e una formula

$$\mathrm{Teor}(x) \quad\text{della forma}\quad \exists y\, \mathrm{Dim}(y,x)$$

Si noti che $\mathrm{Teor}$ è una formula come tutte le altre. In sostanza $\mathrm{Teor}(x)$ è vera per tutti gli $x$ godeliani di qualche teorema.

Si possono dimostrare tre proprietà di $\mathrm{Teor}$:

$$\begin{align} &1. && \varphi \text{ è dimostrabile} \ \Rightarrow\ \mathrm{Teor}\big(G(\varphi)\big) \text{ è vera} \\ &2. && \mathrm{Teor}\big(G(\varphi \Rightarrow \theta)\big) \ \Rightarrow\ \Big[\mathrm{Teor}\big(G(\varphi)\big) \Rightarrow \mathrm{Teor}\big(G(\theta)\big)\Big] \\ &3. && \mathrm{Teor}\big(G(\varphi)\big) \ \Rightarrow\ \mathrm{Teor}\Big(G\big(\mathrm{Teor}(G(\varphi))\big)\Big) \end{align}$$

Si considera la funzione $\mathbf{sost}(x, y)$, dove $y$ è il godeliano di una formula con variabile libera e $x$ un numero, che restituisce il risultato della sostituzione, nella formula $y$, di $x$ ovunque appaia la variabile libera. In altri termini, sost aritmetizza la sostituzione di un numerale al posto di una variabile libera in una formula.

Si considera poi la funzione $\mathbf{not}(x)$, che al godeliano di una formula $x$ associa il godeliano della negazione di quella formula.

Si considera infine la composizione di sost e not:

$$\mathbf{sostnot}(x) = \mathbf{sost}\big(x,\ \mathbf{not}(x)\big)$$

che, data una formula con una variabile libera il cui godeliano è $x$, fornisce il godeliano della formula ottenuta negando quella formula e sostituendo alla variabile libera il godeliano $x$ stesso.

Queste funzioni sono rappresentabili numericamente secondo lo schema fornito da Gödel.

Fatte tali premesse, consideriamo il numero $n$, godeliano della formula

$$\mathrm{Teor}\big(\mathbf{sostnot}(x)\big) \qquad (2)$$

Questa formula significa, data una formula di godeliano $x$ avente una variabile libera, "$\mathbf{sostnot}(x)$ è dimostrabile".

Se sostituiamo il numerale di $n$ alla variabile $x$ nella negazione di questa formula otteniamo

$$\neg\,\mathrm{Teor}\big(\mathbf{sostnot}(n)\big) \qquad (3)$$

Il godeliano di questa formula, per le premesse fatte, è proprio $\mathbf{sostnot}(n)$. Infatti, sostituendo:

$\mathbf{sostnot}(n)$ = (dobbiamo negare la formula il cui godeliano è $n$, ossia $\mathrm{Teor}(\mathbf{sostnot}(x))$, e sostituire nella sua variabile libera il numerale $n$) = $G\big(\neg\,\mathrm{Teor}(\mathbf{sostnot}(n))\big)$.

Questa formula concettualmente vuol dire "io non sono dimostrabile": infatti $\mathrm{Teor}(x)$ dice che esiste una dimostrazione $y$ di $x$, quindi $\neg\,\mathrm{Teor}$ dice che non esiste una dimostrazione di $\mathbf{sostnot}(n)$.

Primo caso. Vediamo cosa succede se la (3), $\neg\,\mathrm{Teor}(\mathbf{sostnot}(n))$, fosse dimostrabile, e sia $m$ il godeliano della dimostrazione. Allora sarebbe dimostrabile $\mathrm{Dim}(m, \mathbf{sostnot}(n))$, pertanto $\exists y\, \mathrm{Dim}(y, \mathbf{sostnot}(n))$, quindi sarebbe dimostrabile $\mathrm{Teor}(\mathbf{sostnot}(n))$, che è la negazione della (3): avremmo un'incoerenza.

Secondo caso. Supponiamo invece che $\mathrm{Teor}(\mathbf{sostnot}(n))$, cioè la negazione della (3), sia dimostrabile. Se lo fosse, esisterebbe $m$ tale che $\mathrm{Dim}(m, \mathbf{sostnot}(n))$. Avendo già dimostrato che la (3) non è dimostrabile, non esiste $y$ tale che $\mathrm{Dim}(y, \mathbf{sostnot}(n))$; quindi neanche $m$ è tale che $\mathrm{Dim}(m, \mathbf{sostnot}(n))$, ossia si avrebbe $\neg\,\mathrm{Dim}(m, \mathbf{sostnot}(n))$, che contraddice l'assunto. $\blacksquare$

Secondo teorema di incompletezza di Gödel

TeoremaIn una teoria $T$ sufficientemente espressiva da contenere l'aritmetica, ed effettivamente assiomatizzabile e coerente, non è possibile provare la coerenza di $T$ all'interno di $T$.

Il secondo teorema non richiede una costruzione nuova: si ottiene formalizzando dentro $T$ la dimostrazione del primo. È qui che tornano utili le tre proprietà di $\mathrm{Teor}$ elencate poco sopra, che nella letteratura hanno un nome: sono le condizioni di derivabilità di Hilbert-Bernays, introdotte nei Grundlagen der Mathematik del 1939 e poi semplificate da Martin Löb nel 1955. Riscritte con la notazione usata finora:

$$\begin{align} &\text{(D1)} && T \vdash \varphi \quad\Longrightarrow\quad T \vdash \mathrm{Teor}\big(G(\varphi)\big) \\ &\text{(D2)} && T \vdash \mathrm{Teor}\big(G(\varphi \Rightarrow \theta)\big) \Rightarrow \Big[\mathrm{Teor}\big(G(\varphi)\big) \Rightarrow \mathrm{Teor}\big(G(\theta)\big)\Big] \\ &\text{(D3)} && T \vdash \mathrm{Teor}\big(G(\varphi)\big) \Rightarrow \mathrm{Teor}\Big(G\big(\mathrm{Teor}(G(\varphi))\big)\Big) \end{align}$$

La differenza rispetto a come le avevamo enunciate è sottile ma decisiva: la (D1) è una regola che vale a livello metateorico, cioè siamo noi a osservarla dall'esterno; la (D2) e la (D3) sono invece enunciati che $T$ dimostra al proprio interno. È questo che permette di far entrare il ragionamento dentro la teoria invece di lasciarlo fuori.

Denotiamo con $\Gamma$ la formula autoreferenziale costruita nel primo teorema, quella per cui

$$T \vdash \Gamma \leftrightarrow \neg\,\mathrm{Teor}\big(G(\Gamma)\big)$$

e con $\mathrm{Coer}(T)$ l'enunciato che formalizza la coerenza di $T$, per esempio $\neg\,\mathrm{Teor}\big(G(0=1)\big)$: "non è dimostrabile una contraddizione".

Il primo teorema, nella sua prima metà, dice: se $T$ è coerente, allora $\Gamma$ non è dimostrabile. Quel ragionamento — che abbiamo svolto poco fa in italiano — usa soltanto passaggi elementari sulla nozione di dimostrabilità, e con le (D1), (D2) e (D3) si può ripetere dentro $T$, ottenendo

$$T \vdash \mathrm{Coer}(T) \Rightarrow \Gamma$$

A questo punto la conclusione è immediata. Se $T$ dimostrasse la propria coerenza, cioè se $T \vdash \mathrm{Coer}(T)$, allora per modus ponens si avrebbe $T \vdash \Gamma$. Ma il primo teorema ci ha appena detto che $\Gamma$ non è dimostrabile in una teoria coerente. Quindi $T$ non può dimostrare $\mathrm{Coer}(T)$. $\blacksquare$

Il risultato ha una portata che va oltre la logica formale, perché colpisce un programma preciso: quello di Hilbert, che si proponeva di fondare la matematica dimostrandone la coerenza con mezzi finitari, cioè elementari e incontestabili. Il secondo teorema dice che nemmeno un sistema robusto quanto si vuole può fare da garante a sé stesso: per dimostrare la coerenza di $T$ serve sempre una teoria più forte, la cui coerenza a sua volta resta da dimostrare. La sequenza non si chiude mai.

Va notato che il teorema non dice che la coerenza dell'aritmetica sia indimostrabile in assoluto: dice che non è dimostrabile dall'interno. Nel 1936 Gerhard Gentzen ne diede infatti una dimostrazione, usando l'induzione transfinita fino all'ordinale $\varepsilon_0$ — un principio che l'aritmetica di Peano non è in grado di formalizzare, e che quindi non viola nulla, ma che è anche più difficile da accettare come "evidente" di quanto non lo sia la coerenza che si voleva provare.

Considerazioni

Il primo teorema di Gödel stabilisce che in una teoria sufficientemente espressiva ci sono sempre teoremi che non possono essere dimostrati. Si potrebbero aggiungere assiomi per renderli veri, ma si otterrebbe una nuova teoria con gli stessi limiti della precedente, creando spazio per nuovi teoremi indimostrabili, e così via.

La mia perplessità sulla dimostrazione del primo teorema non è di tipo prettamente matematico, ma riguarda l'interpretazione del risultato.

La dimostrazione consiste principalmente nel costruire una formula autoreferenziale, $\neg\,\mathrm{Teor}(\mathbf{sostnot}(n))$, che afferma di non essere dimostrabile. Tuttavia, nel farlo, assimila una dimostrazione alla sua rappresentazione "tipografica" ben precisa.

Una prima perplessità sta proprio in questo, che potrebbe apparire un limite. Tuttavia, anche ammettendo che ci siano altri teoremi, tipograficamente diversi, attestanti lo stesso concetto, questi potrebbero essere usati in una catena di dimostrazioni per ottenere il teorema "indimostrabile", che diverrebbe pertanto dimostrabile. Pertanto la scelta tipografica della dimostrazione — i caratteri usati, l'ordine, o persino una modalità di dimostrazione diversa — non serve ad aggirare il vincolo dato dalla formula $\mathrm{Teor}$.

Bibliografia

Gabriele Lolli, Sotto il segno di Gödel — recensione
Il primo teorema di incompletezza di Gödel
I teoremi di incompletezza di Gödel, Treccani
Francesco Berto, Tutti pazzi per Gödel!
Kurt Gödel, Stanford Encyclopedia of Philosophy
Teoremi di incompletezza di Gödel, Wikibooks

Cerca nel blog

Appunti di informatica