Dimostrazione originale del teorema di completezza di Gödel

La dimostrazione del teorema di completezza di Gödel, fornita da Kurt Gödel nella sua tesi di dottorato del 1929 (e una versione più breve, pubblicata come articolo nel 1930^[1], intitolata "La completezza degli assiomi del calcolo funzionale della logica" in tedesco) ad oggi non è facile da leggere: utilizza concetti e formalismi in disuso e terminologie spesso oscure. La versione fornita di seguito tenta di rappresentare fedelmente tutti i passaggi della dimostrazione e tutte le idee importanti, pur riformulandola nel linguaggio odierno della logica matematica. Questa traccia non deve essere considerata una prova rigorosa del teorema.

Lavoriamo nel calcolo dei predicati del primo ordine. I linguaggi consentono i simboli di costanti, di funzioni e di predicati. Le strutture sono costituite da un dominio (non vuoto) e da una funzione che interpreta i simboli del relativo linguaggio come elementi, funzioni o relazioni su quel dominio.

Utilizziamo la logica classica (invece che la logica intuizionistica, per esempio).

Fissiamo una qualche assiomatizzazione (cioè un sistema di deduzione attuabile da una macchina) del calcolo dei predicati, formato da assiomi logici e regole di inferenza: uno qualunque dei numerosi sistemi equivalenti andrà bene. La dimostrazione originale di Gödel usava il sistema di Hilbert-Ackermann.

Assumiamo, senza dimostrarli, tutti i ben noti risultati di base sul nostro formalismo di cui abbiamo bisogno, come il teorema della forma normale e il teorema di correttezza.

Usiamo il calcolo dei predicati senza uguaglianza (a volte chiamato erroneamente senza identità), cioè non ci sono assiomi speciali che esprimono le proprietà dell'uguaglianza (tra elementi del dominio) come un simbolo di relazione speciale. Dopo aver dimostrato la forma base del teorema, sarà facile estenderla al caso del calcolo dei predicati con uguaglianza.

Di seguito enunciamo due forme del teorema e ne mostriamo l'equivalenza. Successivamente, dimostriamo il teorema. Ciò viene realizzato attraverso i seguenti passaggi:

1. Riduciamo il teorema ai soli enunciati (formule senza variabili libere) in forma prenessa, cioè con tutti i quantificatori (∀ e ∃) all'inizio. Inoltre, lo riduciamo a formule il cui primo quantificatore è ∀. Questo è possibile perché, per ogni formula chiusa, ne esiste una equivalente in forma prenessa il cui primo quantificatore è ∀.
2. Riduciamo il teorema ai soli enunciati della forma ${\displaystyle \forall x_{1}\dots \forall x_{k}\exists y_{1}\dots \exists y_{m}\phi [x_{1},\dots ,x_{k},y_{1},\dots ,y_{m}]}$. Sebbene non possiamo farlo semplicemente riordinando i quantificatori, mostriamo che è ancora sufficiente provare il teorema per enunciati di questa forma.
3. Infine, dimostriamo il teorema per enunciati della suddetta forma.
   • Ciò viene effettuato notando prima che un enunciato come ${\displaystyle B=\forall x_{1}\dots \forall x_{k}\exists y_{1}\dots \exists y_{m}\phi [x_{1},\dots ,x_{k},y_{1},\dots ,y_{m}]}$ è refutabile (la sua negazione è dimostrabile) oppure soddisfacibile, cioè c'è qualche modello nel quale è vero (potrebbe anche essere sempre vero, cioè una tautologia); questo modello sta semplicemente assegnando valori di verità ai sottoenunciati da cui ${\displaystyle B}$ è formato. La ragione di ciò è la completezza della logica proposizionale, con i quantificatori esistenziali che non giocano alcun ruolo.
   • Estendiamo questo risultato a enunciati sempre più complessi e lunghi ${\displaystyle D_{n}\ (n=1,2,\dots )}$, costruiti a partire da ${\displaystyle B}$, in modo che qualcuno di essi è refutabile e quindi lo è anche ${\displaystyle \phi }$, oppure sono tutti non refutabili e quindi ognuno è vero in qualche modello.
   • Usiamo infine i modelli in cui valgono i ${\displaystyle D_{n}}$ (nel caso siano tutti non refutabili) per costruire un modello in cui vale ${\displaystyle \phi }$.

Questa è la forma più elementare del teorema di completezza. Lo riformuliamo subito in una forma più comoda per i nostri scopi: quando diciamo "tutte le strutture", è importante specificare che le strutture coinvolte sono interpretazioni classiche (tarskiane) ${\displaystyle I=\langle U,F\rangle }$, dove ${\displaystyle U}$ è un insieme di oggetti non vuoto (possibilmente infinito), mentre ${\displaystyle F}$ è una funzione che mappa simboli di costanti, di funzioni e di predicati rispettivamente in elementi di ${\displaystyle U}$, funzioni e relazioni su ${\displaystyle U}$ (al contrario, le cosiddette "logiche libere" accettano anche che il dominio sia vuoto; per saperne di più sulle logiche libere, si veda il lavoro di Karel Lambert).

"${\displaystyle \phi }$ è refutabile" significa per definizione "${\displaystyle \neg \phi }$ è dimostrabile".

Se vale il Teorema 1 e ${\displaystyle \phi }$ non è soddisfacibile, allora ${\displaystyle \neg \phi }$ è valida in tutte le strutture e quindi dimostrabile, dunque ${\displaystyle \phi }$ è refutabile e vale il Teorema 2. Se invece vale il Teorema 2 e ${\displaystyle \phi }$ vale in tutte le strutture, allora ${\displaystyle \neg \phi }$ non è soddisfacibile e quindi refutabile; ma allora ${\displaystyle \neg \neg \phi }$ è dimostrabile e dunque lo è anche ${\displaystyle \phi }$, quindi vale il Teorema 1.

Iniziamo la dimostrazione del Teorema 2 restringendo sequenzialmente la classe di tutte le formule ${\displaystyle \phi }$ per le quali dobbiamo dimostrare che "${\displaystyle \phi }$ è insoddisfacibile solo se è refutabile".

All'inizio dobbiamo dimostrarlo per tutte le possibili formule del linguaggio preso in esame. Tuttavia, supponiamo che per ogni formula ${\displaystyle \phi }$ esista qualche formula ${\displaystyle \psi _{\phi }}$, presa da una classe più ristretta di formule ${\displaystyle \mathrm {C} }$, tale per cui "${\displaystyle \psi _{\phi }}$ è insoddisfacibile solo se è refutabile"${\displaystyle \implies }$"${\displaystyle \phi }$ è insoddisfacibile solo se è refutabile".

Allora, una volta provata questa affermazione (espressa nella frase precedente), basterà dimostrare che "${\displaystyle \phi }$ è insoddisfacibile solo se è refutabile" solo per le ${\displaystyle \phi }$ che stanno nella classe ${\displaystyle \mathrm {C} }$. Se ${\displaystyle \phi }$ e ${\displaystyle \psi _{\phi }}$ sono sintatticamente equivalenti, ovvero ${\displaystyle \phi \equiv \psi _{\phi }}$ (cioè, se la formula ${\displaystyle \phi \leftrightarrow \psi _{\phi }}$ è dimostrabile), allora è vero che "${\displaystyle \psi _{\phi }}$ è insoddisfacibile solo se è refutabile"${\displaystyle \implies }$"${\displaystyle \phi }$ è insoddisfacibile solo se è refutabile" (il teorema di correttezza è necessario per provare ciò).

Esistono tecniche standard per riscrivere una formula arbitraria in un'altra che non utilizzi funzioni e simboli costanti, a costo di introdurre quantificatori aggiuntivi; assumeremo quindi che tutte le formule siano prive di tali simboli. L'articolo di Gödel utilizzava dal principio una versione del calcolo dei predicati che non ha funzioni e costanti.

Ora, consideriamo una formula generica ${\displaystyle \phi }$ (che non contiene funzioni o costanti) e applichiamo il teorema della forma prenessa per trovare una formula ${\displaystyle \psi _{\phi }}$ in forma normale tale che ${\displaystyle \phi \equiv \psi _{\phi }}$ (forma normale significa che tutti i quantificatori in ${\displaystyle \psi _{\phi }}$, se ce ne sono, si trovano proprio all'inizio di ${\displaystyle \psi _{\phi }}$). Ne consegue che ora dobbiamo dimostrare il Teorema 2 solo per le formule ${\displaystyle \phi }$ in forma normale.

Adesso, eliminiamo tutte le variabili libere da ${\displaystyle \phi }$ quantificandole esistenzialmente: se poniamo che ${\displaystyle x_{1},\dots ,x_{n}}$ sono libere in ${\displaystyle \phi }$, formiamo ${\displaystyle \psi _{\phi }=\exists x_{1}\dots \exists x_{n}\phi }$. Se ${\displaystyle \psi _{\phi }}$ è vera in qualche struttura ${\displaystyle M}$, allora esiste un'assegnazione su ${\displaystyle M}$ alle variabili ${\displaystyle x_{1},\dots ,x_{n}}$ che verifica ${\displaystyle \phi }$ in ${\displaystyle M}$, quindi ${\displaystyle \phi }$ è soddisfacibile; se invece ${\displaystyle \psi _{\phi }}$ è insoddisfacibile, allora ${\displaystyle \neg \psi _{\phi }\equiv \forall x_{1}\dots \forall x_{n}\neg \phi }$ è sempre vera e quindi, in ogni struttura ${\displaystyle M}$, ogni assegnazione su ${\displaystyle M}$ alle variabili ${\displaystyle x_{1},\dots ,x_{n}}$ verifica ${\displaystyle \neg \phi }$, quindi ${\displaystyle \phi }$ è insoddisfacibile. Possiamo allora restringerci alle sole formule ${\displaystyle \phi }$ che sono enunciati, cioè formule senza variabili libere.

Infine vorremmo, per ragioni di convenienza tecnica, che il prefisso di ${\displaystyle \phi }$ (ovvero la stringa di quantificatori all'inizio di ${\displaystyle \phi }$, che è in forma normale) inizi con un quantificatore universale e finisca con un quantificatore esistenziale. Per ottenere ciò per una generica ${\displaystyle \phi }$ (soggetta alle restrizioni che abbiamo già dimostrato), prendiamo due variabili ${\displaystyle y}$ e ${\displaystyle z}$ che non occorrono in ${\displaystyle \phi }$. Se ${\displaystyle \phi =(P)\Phi }$, dove ${\displaystyle (P)}$ sta per il prefisso di ${\displaystyle \phi }$ e ${\displaystyle \Phi }$ per la matrice (la restante parte di ${\displaystyle \phi }$ priva di quantificatori), formiamo ${\displaystyle \psi _{\phi }=\forall y(P)\exists z\Phi }$, che ovviamente è equivalente a ${\displaystyle \phi }$, dato che ${\displaystyle y}$ e ${\displaystyle z}$ non compaiono in ${\displaystyle \Phi }$.

La nostra formula generica ${\displaystyle \phi }$ ora è un enunciato, in forma normale, e il suo prefisso inizia con un quantificatore universale e termina con un quantificatore esistenziale. Chiamiamo la classe di tutte queste formule ${\displaystyle \mathrm {R} }$. Dobbiamo dimostrare che ogni formula in ${\displaystyle \mathrm {R} }$ è insoddisfacibile solo se è refutabile. Data la nostra formula ${\displaystyle \phi }$, raggruppiamo stringhe di quantificatori dello stesso tipo in blocchi:

${\displaystyle \phi =(\forall x_{1}\dots \forall x_{k_{1}})(\exists x_{k_{1}+1}\dots \exists x_{k_{2}})\dots (\forall x_{k_{n-2}+1}\dots \forall x_{k_{n-1}})(\exists x_{k_{n-1}+1}\dots \exists x_{k_{n}})\Phi }$

Definiamo il grado di ${\displaystyle \phi }$ come il numero di blocchi di quantificatori universali separati da blocchi di quantificatori esistenziali nel prefisso di ${\displaystyle \phi }$, come mostrato sopra. Il seguente lemma, che Gödel ha adattato dalla dimostrazione di Skolem del teorema di Löwenheim-Skolem, ci permette di ridurre nettamente la complessità delle formule ${\displaystyle \phi }$ per cui dobbiamo dimostrare il teorema:

Lemma. Sia ${\displaystyle k\geq 1}$. Se ogni formula in ${\displaystyle \mathrm {R} }$ di grado ${\displaystyle k}$ è soddisfacibile o refutabile, allora lo è anche ogni formula in ${\displaystyle \mathrm {R} }$ di grado ${\displaystyle k+1}$.

Commento: Si prenda una formula ${\displaystyle \phi }$ di grado ${\displaystyle k+1}$ della forma ${\displaystyle \phi =\forall x\exists y\forall u\exists v(P)\psi }$, dove ${\displaystyle (P)\psi }$ è il resto di ${\displaystyle \phi }$ (quindi è di grado ${\displaystyle k-1}$). ${\displaystyle \phi }$ afferma che per ogni ${\displaystyle x}$ esiste ${\displaystyle y}$ tale che... (qualcosa). Sarebbe stato bello avere un predicato ${\displaystyle Q}$ in modo che per ogni ${\displaystyle x}$, ${\displaystyle Q(x,y)}$ fosse vero se e solo se il valore di ${\displaystyle y}$ è quello richiesto per rendere (qualcosa) vero. Allora avremmo potuto scrivere una formula di grado ${\displaystyle k}$, equivalente a ${\displaystyle \phi }$, vale a dire ${\displaystyle \forall x'\forall x\forall y\forall u\exists v\exists y'(P)Q(x',y')\land (Q(x,y)\rightarrow \psi )}$ . Questa formula è infatti equivalente a ${\displaystyle \phi }$, perché afferma che per ogni ${\displaystyle x}$, se c'è un ${\displaystyle y}$ che soddisfa ${\displaystyle Q(x,y)}$, allora (qualcosa) vale, e inoltre sappiamo che c'è tale ${\displaystyle y}$, perché per ogni ${\displaystyle x'}$ c'è un ${\displaystyle y'}$ che soddisfa ${\displaystyle Q(x',y')}$. Quindi ${\displaystyle \phi }$ segue da questa formula. È facile anche dimostrare che se la formula è falsa, lo è anche ${\displaystyle \phi }$. Sfortunatamente, in generale non esiste un tale predicato. Tuttavia, questa idea può essere intesa come base per la seguente dimostrazione del lemma.

Dimostrazione. Sia ${\displaystyle \phi }$ una formula di grado ${\displaystyle k+1}$. Allora, possiamo scriverla come:

${\displaystyle \phi =(\forall x)(\exists y)(\forall u)(\exists v)(P)\psi }$

dove ${\displaystyle (P)}$ è il resto del prefisso di ${\displaystyle \phi }$ (quindi è di grado ${\displaystyle k-1}$) e ${\displaystyle \psi }$ è la matrice priva di quantificatori di ${\displaystyle \phi }$. ${\displaystyle x,y,u,v}$ denotano qui ennuple di variabili invece che singole variabili; per esempio, ${\displaystyle (\forall x)}$ in realtà sta per ${\displaystyle \forall x_{1}\forall x_{2}\dots \forall x_{n}}$, dove ${\displaystyle (x_{1},\dots ,x_{n})}$ sono variabili distinte.

Siano ora ${\displaystyle x'}$e ${\displaystyle y'}$ennuple di variabili precedentemente inutilizzate, rispettivamente della stessa lunghezza di ${\displaystyle x}$ e ${\displaystyle y}$, e sia ${\displaystyle Q}$ un simbolo di relazione precedentemente inutilizzato, che accetta un numero di argomenti pari alla somma delle lunghezze di ${\displaystyle x}$ e ${\displaystyle y}$; consideriamo la formula

${\displaystyle \Phi =(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )}$

Chiaramente, ${\displaystyle \Phi \implies \phi }$.

Ora, poiché la stringa di quantificatori ${\displaystyle (\forall u)(\exists v)(P)}$ non contiene variabili di ${\displaystyle x}$ e ${\displaystyle y}$, la seguente equivalenza è facilmente dimostrabile con l'aiuto del formalismo che stiamo usando:

${\displaystyle (Q(x,y)\rightarrow (\forall u)(\exists v)(P)\psi )\equiv (\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )}$

E poiché queste due formule sono equivalenti, se sostituiamo la prima con la seconda dentro ${\displaystyle \Phi }$, otteniamo la formula ${\displaystyle \Phi '}$ tale che ${\displaystyle \Phi \equiv \Phi '}$:

${\displaystyle \Phi '=(\forall x')(\exists y')Q(x',y')\wedge (\forall x)(\forall y)(\forall u)(\exists v)(P)(Q(x,y)\rightarrow \psi )}$

Ora ${\displaystyle \Phi '}$ ha la forma ${\displaystyle (S)\rho \wedge (S')\rho '}$, dove ${\displaystyle (S)}$ e ${\displaystyle (S')}$ sono stringhe di quantificatori, ${\displaystyle \rho }$ e ${\displaystyle \rho '}$ sono prive di quantificatori e, inoltre, nessuna variabile di ${\displaystyle (S)}$ occorre in ${\displaystyle \rho '}$ e nessuna variabile di ${\displaystyle (S')}$ occorre in ${\displaystyle \rho }$. In tali condizioni, ogni formula della forma ${\displaystyle (T)(\rho \wedge \rho ')}$, dove ${\displaystyle (T)}$ è una stringa di quantificatori contenente tutti i quelli in ${\displaystyle (S)}$ e ${\displaystyle (S')}$ inseriti in qualsiasi ordine, ma mantenendo l'ordine relativo all'interno di ${\displaystyle (S)}$ e ${\displaystyle (S')}$, sarà equivalente alla formula originale ${\displaystyle \Phi '}$ (questo è un altro risultato fondamentale del calcolo dei predicati su cui ci basiamo). Dunque, formiamo ${\displaystyle \Psi }$ come segue:

${\displaystyle \Psi =(\forall x')(\forall x)(\forall y)(\forall u)(\exists y')(\exists v)(P)Q(x',y')\wedge (Q(x,y)\rightarrow \psi )}$

e abbiamo ${\displaystyle \Phi '\equiv \Psi }$.

Ora ${\displaystyle \Psi }$ è una formula di grado ${\displaystyle k}$ e quindi, per ipotesi induttiva, soddisfacibile o refutabile. Se ${\displaystyle \Psi }$ è soddisfacibile, allora, considerando ${\displaystyle \Psi \equiv \Phi '\equiv \Phi }$ e ${\displaystyle \Phi \implies \phi }$, vediamo che anche ${\displaystyle \phi }$ è soddisfacibile. Se ${\displaystyle \Psi }$ è refutabile, allora lo è anche ${\displaystyle \Phi }$, che è equivalente ad esso; dunque ${\displaystyle \neg \Phi }$ è dimostrabile. Ora possiamo sostituire tutte le occorrenze di ${\displaystyle Q}$ all'interno della formula dimostrabile ${\displaystyle \neg \Phi }$ da qualche altra formula dipendente dalle stesse variabili, e otterremo comunque una formula dimostrabile. (Questo è ancora un altro risultato fondamentale del calcolo dei predicati. A seconda del particolare formalismo adottato per il calcolo, esso può essere visto come una semplice applicazione della regola di inferenza di "sostituzione funzionale", come nell'articolo di Gödel, oppure può essere dimostrato considerando la dimostrazione formale di ${\displaystyle \neg \Phi }$, sostituendo in essa tutte le occorrenze di ${\displaystyle Q}$ con qualche altra formula con le stesse variabili libere, e notando che tutti gli assiomi logici nella dimostrazione formale rimangono tali dopo la sostituzione, e tutte le regole di inferenza si applicano ancora allo stesso modo.)

In questo caso particolare, sostituiamo ${\displaystyle Q(x',y')}$ in ${\displaystyle \neg \Phi }$ con la formula ${\displaystyle (\forall u)(\exists v)(P)\psi [x,y/x',y']}$. Qui ${\displaystyle [x,y/x',y']}$ significa che invece di ${\displaystyle \psi }$ stiamo scrivendo una formula diversa, in cui ${\displaystyle x}$ e ${\displaystyle y}$ sono sostituiti con ${\displaystyle x'}$ e ${\displaystyle y'}$. ${\displaystyle Q(x,y)}$ è semplicemente sostituito da ${\displaystyle (\forall u)(\exists v)(P)\psi }$.

${\displaystyle \neg \Phi }$ diventa

${\displaystyle \neg ((\forall x')(\exists y')(\forall u)(\exists v)(P)\psi [x,y/x',y']\wedge (\forall x)(\forall y)((\forall u)(\exists v)(P)\psi \rightarrow (\forall u)(\exists v)(P)\psi ))}$

e questa formula è dimostrabile; poiché la parte dopo il segno ${\displaystyle \wedge }$ è ovviamente dimostrabile, e la parte sotto negazione e prima del segno ${\displaystyle \wedge }$ è ovviamente ${\displaystyle \phi }$, ma con ${\displaystyle x}$ e ${\displaystyle y}$ sono sostituiti da ${\displaystyle x'}$ e ${\displaystyle y'}$, segue che ${\displaystyle \neg \phi }$ è dimostrabile e ${\displaystyle \phi }$ è refutabile. Abbiamo dimostrato che ${\displaystyle \phi }$ è soddisfacibile o refutabile, e questo conclude la dimostrazione del Lemma.

Si noti che non possiamo utilizzare ${\displaystyle (\forall u)(\exists v)(P)\psi [x,y/x',y']}$ invece di ${\displaystyle Q(x',y')}$ dall'inizio, perché in quel caso ${\displaystyle \Psi }$ non sarebbe stata una formula in ${\displaystyle \mathrm {R} }$, e quindi non avremmo potuto usare l'induzione. Ecco perché non possiamo usare ingenuamente l'argomento che compare al commento che precede la dimostrazione.

Come mostrato nel precedente Lemma, dobbiamo dimostrare il teorema solo per le formule ${\displaystyle \phi }$ in ${\displaystyle \mathrm {R} }$ di grado 1. ${\displaystyle \phi }$ non può essere di grado 0, poiché le formule in ${\displaystyle \mathrm {R} }$ non hanno variabili libere e non usano costanti. Quindi la formula ${\displaystyle \phi }$ ha la forma generale:

${\displaystyle (\forall x_{1}\dots \forall x_{k})(\exists y_{1}\dots \exists y_{m})\phi [x_{1},\dots ,x_{k},y_{1},\dots ,y_{m}]}$

Ora, definiamo un ordinamento delle k-uple di numeri naturali come segue: ${\displaystyle (x_{1},\dots ,x_{k})<(y_{1},\dots ,y_{k})}$ se e solo se vale almeno una delle seguenti:

• ${\displaystyle \sum _{i=1}^{k}x_{i}<\sum _{i=1}^{k}y_{i}}$;
• ${\displaystyle \sum _{i=1}^{k}x_{i}=\sum _{i=1}^{k}y_{i}}$ e ${\displaystyle (x_{1},\dots ,x_{k})}$ precede ${\displaystyle (y_{1},\dots ,y_{k})}$ in ordine lessicografico.

Denotiamo l'ennesima k-upla nell'ordine appena definito con ${\displaystyle (a_{1}^{n},\dots ,a_{k}^{n})}$.

Poniamo:

• ${\displaystyle B_{n}:=\phi [z_{a_{1}^{n}},\dots ,z_{a_{k}^{n}},z_{(n-1)m+2},z_{(n-1)m+3},\dots ,z_{nm+1}]}$;
• ${\displaystyle D_{n}:=\exists z_{1}\dots \exists z_{nm+1}(B_{1}\land \dots \land B_{n})}$.

Lemma: Per ogni intero ${\displaystyle n\geq 1}$, ${\displaystyle \phi \implies D_{n}}$.

Dimostrazione: Per induzione su ${\displaystyle n}$.

Abbiamo:

${\displaystyle {\begin{aligned}D_{n}&\Longleftarrow D_{n-1}\wedge (\forall z_{1}\dots \forall z_{(n-1)m+1})(\exists z_{(n-1)m+2}\dots \exists z_{nm+1})B_{n}\\&\Longleftarrow D_{n-1}\wedge (\forall z_{a_{1}^{n}}\dots \forall z_{a_{k}^{n}})(\exists y_{1}\dots \exists y_{m})\phi [z_{a_{1}^{n}},\dots ,z_{a_{k}^{n}},y_{1},\dots ,y_{m}]\end{aligned}}}$

dove quest'ultima implicazione vale per sostituzione di variabili, poiché l'ordinamento delle k-uple è tale che, per ogni ${\displaystyle k\geq 1}$ e per ogni ${\displaystyle i\in \{1,\dots ,k\}}$, vale ${\displaystyle {a_{i}^{n}}\leq n<(n-1)m+2}$. Ma l'ultima formula è equivalente a ${\displaystyle D_{n-1}\land \phi }$.

Per il caso base, ${\displaystyle D_{1}=\exists z_{1}\dots \exists z_{m+1}\phi [z_{a_{1}^{1}},\dots ,z_{a_{k}^{1}},z_{2},z_{3},\dots ,z_{m+1}]\equiv \exists z_{1}\dots \exists z_{m+1}\phi [z_{1},\dots ,z_{1},z_{2},z_{3},\dots ,z_{m+1}]}$ è ovviamente un corollario di ${\displaystyle \phi }$. Quindi il Lemma è dimostrato.

Ora, se ${\displaystyle D_{n}}$ è refutabile per qualche ${\displaystyle n\geq 1}$, segue che ${\displaystyle \phi }$ è refutabile. D'altra parte, supponiamo che, per ogni ${\displaystyle n\geq 1}$, ${\displaystyle D_{n}}$ sia non refutabile. Allora, per ogni ${\displaystyle n\geq 1}$, la formula ${\displaystyle D'_{n}:=B_{1}\land \dots \land B_{n}}$ non è refutabile. Questa proprietà dev'essere una conseguenza diretta delle regole di deduzione, altrimenti il sistema non potrebbe garantire la propria completezza.

Dunque, per ogni ${\displaystyle n\geq 1}$, esiste un'assegnazione di verità alle distinte sottoformule ${\displaystyle E_{h}}$ (ordinate secondo la loro prima occorrenza in ${\displaystyle D_{n}'}$; "distinto" qui è inteso in senso sintattico, ovvero sia predicati distinti, sia variabili distinte) nelle ${\displaystyle B_{i}}$, che rende vera ${\displaystyle D_{n}'}$. Ciò deriva dalla completezza della logica proposizionale sottostante.

Ora, mostreremo che esiste un'assegnazione di verità alle ${\displaystyle E_{h}}$ che rende vere tutte le ${\displaystyle D_{n}'}$: le ${\displaystyle E_{h}}$ appaiono nello stesso ordine in ogni ${\displaystyle D_{n}'}$; definiremo induttivamente un'assegnazione generale mediante una sorta di "voto di maggioranza": poiché vi sono infinite assegnazioni per ${\displaystyle E_{1}}$ (una per ogni ${\displaystyle D_{n}'}$), allora o infinite assegnazioni rendono ${\displaystyle E_{1}}$ vera, o solo un numero finito di assegnazioni la rende vera e infinite la rendono falsa. Nel primo caso, ${\displaystyle E_{1}}$ sarà vera nell'assegnazione generale, altrimenti sarà falsa. Nell'induzione, rendiamo ${\displaystyle E_{h}}$ vera se ci sono infinite assegnazioni che rendono ${\displaystyle E_{h}}$ vera, ma solo tra le infinite assegnazioni per le ${\displaystyle D_{n}'}$ che coincidono con l'assegnazione generale da ${\displaystyle E_{1}}$ a ${\displaystyle E_{h-1}}$.

Questa assegnazione generale deve rendere vere ciascuna delle ${\displaystyle B_{i}}$ e ${\displaystyle D_{n}'}$, poiché se l'assegnazione falsificasse una delle ${\displaystyle B_{i}}$, anche le ${\displaystyle D'_{j}}$ sarebbero false per ogni ${\displaystyle j>n}$. Ma questo contraddice il fatto che, per costruzione dell'assegnazione generale fino alle ${\displaystyle E_{h}}$ che compaiono in ${\displaystyle D_{n}'}$, ci sono infiniti ${\displaystyle j}$ tali per cui l'assegnazione che avvera ${\displaystyle D'_{j}}$ coincide con l'assegnazione generale.

Da questa assegnazione, che rende tutte le ${\displaystyle D_{n}'}$ vere, costruiamo un'interpretazione dei predicati del linguaggio che rende vera ${\displaystyle \phi }$. Il dominio del modello saranno i numeri naturali. Ogni predicato ${\displaystyle p}$-ario ${\displaystyle \Psi }$ è vero su ${\displaystyle (u_{1},\dots ,u_{p})}$ precisamente quando la formula atomica ${\displaystyle \Psi (z_{u_{1}},\dots ,z_{u_{p}})}$ è vera nell'assegnazione generale, oppure non ha valore di verità (se non compare mai in nessuno dei ${\displaystyle D_{n}'}$).

In questo modello, ciascuna delle formule ${\displaystyle \exists y_{1}\dots \exists y_{m}\phi [x_{1},\dots ,x_{k},y_{1},\dots ,y_{m}]}$ è vera per costruzione su ogni assegnazione ${\displaystyle \eta }$ tale per cui ${\displaystyle \eta (x_{1})=a_{1}^{n},\dots ,\eta (x_{k})=a_{k}^{n}}$. Ma questo implica che ${\displaystyle \phi }$ stessa è vera nel modello, poiché ${\displaystyle (a_{1}^{n},\dots ,a_{k}^{n})}$ può essere qualunque k-upla di numeri naturali. Quindi ${\displaystyle \phi }$ è soddisfacibile, e abbiamo finito.

Possiamo scrivere ogni ${\displaystyle B_{i}}$ come ${\displaystyle \phi [x_{1},\dots ,x_{k},y_{1},\dots ,y_{m}]}$ per qualche ${\displaystyle x_{1},\dots ,x_{k}}$, che possiamo chiamare "primi argomenti", e ${\displaystyle y_{1},\dots ,y_{m}}$, che possiamo chiamare "ultimi argomenti".

Prendiamo ${\displaystyle B_{1}}$, per esempio. I suoi "ultimi argomenti" sono ${\displaystyle z_{2},z_{3},\dots ,z_{m+1}}$, e per ogni possibile combinazione di ${\displaystyle k}$ di queste variabili c'è un qualche ${\displaystyle j}$ tale per cui esse appaiono come "primi argomenti" in ${\displaystyle B_{j}}$. Quindi per ${\displaystyle n_{1}}$ sufficientemente grande, ${\displaystyle D_{n_{1}}'}$ ha la proprietà che gli "ultimi argomenti" di ${\displaystyle B_{1}}$ appaiono, in ogni possibile combinazione di ${\displaystyle k}$ di essi, come "primi argomenti" in altri ${\displaystyle B_{j}}$ all'interno di ${\displaystyle D_{n_{1}}'}$. Per ogni ${\displaystyle B_{i}}$ c'è un ${\displaystyle D_{n_{i}}'}$ con la proprietà corrispondente.

Quindi, in un modello che soddisfa tutti i ${\displaystyle D_{n}'}$, ci sono oggetti corrispondenti a ${\displaystyle z_{1},z_{2},\dots }$ e ogni combinazione di ${\displaystyle k}$ di questi appare come "primo argomento" in qualche ${\displaystyle B_{j}}$, nel senso che per ogni ${\displaystyle k}$ di questi oggetti ${\displaystyle z_{p_{1}},\dots ,z_{p_{k}}}$ ci sono ${\displaystyle z_{q_{1}},\dots ,z_{q_{m}}}$ che rendono ${\displaystyle \phi [z_{p_{1}},\dots ,z_{p_{k}},z_{q_{1}},\dots ,z_{q_{m}}]}$ vera. Prendendo un sottomodello con solo questi ${\displaystyle z_{1},z_{2},\dots }$ oggetti, abbiamo un modello che soddisfa ${\displaystyle \phi }$.

Gödel ha ridotto ogni formula in cui occorre il predicato di uguaglianza ad una che definisce l'uguaglianza su di essa. Il suo metodo prevede la sostituzione di una formula ${\displaystyle \phi }$ contenente uguaglianze con la formula

${\displaystyle \forall x(x=x)\wedge \forall x\forall y\forall z[x=y\rightarrow (x=z\rightarrow y=z)]}$ ${\displaystyle \wedge \forall x\forall y\forall z[x=y\rightarrow (z=x\rightarrow z=y)]}$

${\displaystyle \wedge }$

${\displaystyle \forall x_{1}\dots \forall x_{k}\forall y_{1}\dots \forall x_{k}[(x_{1}=y_{1}\wedge \dots \wedge x_{k}=y_{k})\rightarrow (P_{1}(x_{1},\dots ,x_{k})\leftrightarrow P_{1}(y_{1},\dots ,y_{k}))]}$

${\displaystyle \wedge ...\wedge }$

${\displaystyle \forall x_{1}\dots \forall x_{m}\forall y_{1}\dots \forall x_{m}[(x_{1}=y_{1}\wedge \dots \wedge x_{m}=y_{m})\rightarrow (P_{n}(x_{1},\dots ,x_{m})\leftrightarrow P_{n}(y_{1},\dots ,y_{m}))]}$

${\displaystyle \wedge \phi }$

Qui ${\displaystyle P_{1},\dots ,P_{n}}$ denotano i predicati che compaiono in ${\displaystyle \phi }$ (con ${\displaystyle k,\dots ,m}$ le loro rispettive arità). Se questa nuova formula è refutabile, lo è anche l'originale ${\displaystyle \phi }$; lo stesso vale per la soddisfacibilità, poiché possiamo prendere l'insieme quoziente del dominio del modello che soddisfa la nuova formula, usando la relazione di equivalenza che rappresenta l'uguaglianza. Questo quoziente è ben definito rispetto agli altri predicati, e quindi soddisferà la formula originaria ${\displaystyle \phi }$.

Gödel ha anche considerato il caso di insiemi numerabili di formule. Usando le stesse riduzioni di cui sopra, ha potuto considerare solo quei casi in cui ogni formula è di grado 1 e non contiene simboli di uguaglianza. Per un insieme numerabile di formule ${\displaystyle \phi ^{i}}$ di grado 1, possiamo definire ${\displaystyle B_{k}^{i}}$ come sopra; quindi definire ${\displaystyle D_{k}}$ come l'unione di ${\displaystyle B_{1}^{1},\dots ,B_{k}^{1},\dots ,B_{1}^{k},\dots ,B_{k}^{k}}$ . Il resto della prova prosegue come prima.

Nel caso di insiemi non numerabili di formule, è necessario l'assioma della scelta (o almeno una sua forma debole). Usando l'AC completo, si possono ben ordinare le formule e dimostrare il caso non numerabile con lo stesso argomento di quello numerabile, ma con l'induzione transfinita. Altri approcci possono essere usati per dimostrare che il teorema di completezza in questo caso è equivalente al teorema dell'ideale booleano primo, una forma debole di AC.

• K Gödel, Über die Vollständigkeit des Logikkalküls, University Of Vienna., 1929. La prima dimostrazione del teorema di completezza.

• Kurt Gödel
• Prova ontologica di Gödel
• Teoremi di incompletezza di Gödel
• Teorema di completezza di Gödel

• Stanford Encyclopedia of Philosophy: "Kurt Gödel" — di Juliette Kennedy.
• Biografia di MacTutor: Kurt Gödel.