Visualizza wikitesto di Dimostrazione originale del teorema di completezza di Gödel

[[File:1925_kurt_gödel_(cropped).png|destra|thumb| Kurt Gödel (1925)]]
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<ref name="nota1"/>, 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.

== Presupposti ==
Lavoriamo nel [[Teoria del primo ordine|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 [[Forma prenessa#Forma normale prenessa|teorema della forma normale]] e il [[Correttezza (logica matematica)|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''.

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

# Riduciamo il teorema ai soli enunciati (formule senza variabili libere) in [[forma prenessa]], cioè con tutti i [[Quantificatore|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 è ∀.
# Riduciamo il teorema ai soli enunciati della forma <math>\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]</math>. Sebbene non possiamo farlo semplicemente riordinando i quantificatori, mostriamo che è ancora sufficiente provare il teorema per enunciati di questa forma.
# Infine, dimostriamo il teorema per enunciati della suddetta forma.
#* Ciò viene effettuato notando prima che un enunciato come <math>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]</math> è 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 [[Valore di verità|valori di verità]] ai sottoenunciati da cui <math>B</math> è formato. La ragione di ciò è la [[Completezza (logica matematica)|completezza]] della [[logica proposizionale]], con i quantificatori esistenziali che non giocano alcun ruolo.
#* Estendiamo questo risultato a enunciati sempre più complessi e lunghi <math>D_n\ (n = 1, 2, \dots) </math>, costruiti a partire da <math>B</math>, in modo che qualcuno di essi è refutabile e quindi lo è anche <math>\phi</math>, oppure sono tutti non refutabili e quindi ognuno è vero in qualche modello.
#* Usiamo infine i modelli in cui valgono i <math>D_n </math> (nel caso siano tutti non refutabili) per costruire un modello in cui vale <math>\phi</math>.

=== Teorema 1. Ogni enunciato valido (vero in tutte le strutture) è dimostrabile. ===
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) <math>I = \langle U, F\rangle</math>, dove <math>U</math> è un insieme di oggetti non vuoto (possibilmente infinito), mentre <math>F</math> è una funzione che mappa simboli di costanti, di funzioni e di predicati rispettivamente in elementi di <math>U</math>, funzioni e relazioni su <math>U</math> (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).

=== Teorema 2. Ogni formula non soddisfacibile è refutabile. ===
"<math>\phi</math> è refutabile" significa ''per definizione'' "<math>\neg\phi</math> è dimostrabile".

=== Equivalenza dei due teoremi ===
Se vale il '''Teorema 1''' e <math>\phi</math> non è soddisfacibile, allora <math>\neg\phi</math> è valida in tutte le strutture e quindi dimostrabile, dunque <math>\phi</math> è refutabile e vale il '''Teorema 2'''. Se invece vale il '''Teorema 2''' e <math>\phi</math> vale in tutte le strutture, allora <math>\neg\phi</math> non è soddisfacibile e quindi refutabile; ma allora <math>\neg\neg\phi</math> è dimostrabile e dunque lo è anche <math>\phi</math>, quindi vale il '''Teorema 1'''.

=== Dimostrazione del teorema 2: primo passo ===
Iniziamo la dimostrazione del '''Teorema 2''' restringendo sequenzialmente la classe di tutte le formule <math>\phi</math> per le quali dobbiamo dimostrare che "<math>\phi</math> è insoddisfacibile solo se è refutabile".

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

Allora, una volta provata questa affermazione (espressa nella frase precedente), basterà dimostrare che "<math>\phi</math> è insoddisfacibile solo se è refutabile" solo per le <math>\phi</math> che stanno nella classe <math>\mathrm C</math>. Se <math>\phi</math> e <math>\psi_\phi</math> sono sintatticamente equivalenti, ovvero <math>\phi \equiv \psi_\phi</math> (''cioè'', se la formula <math>\phi \leftrightarrow \psi_\phi</math> è dimostrabile), allora è vero che "<math>\psi_\phi</math> è insoddisfacibile solo se è refutabile"<math>\implies</math>"<math>\phi</math> è insoddisfacibile solo se è refutabile" (il [[Correttezza (logica matematica)|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 <math>\phi</math> (che non contiene funzioni o costanti) e applichiamo il teorema della [[forma prenessa]] per trovare una formula <math>\psi_\phi</math> in ''forma normale'' tale che <math>\phi \equiv \psi_\phi</math> (''forma normale'' significa che tutti i quantificatori in <math>\psi_\phi</math>, se ce ne sono, si trovano proprio all'inizio di <math>\psi_\phi</math>). Ne consegue che ora dobbiamo dimostrare il '''Teorema 2''' solo per le formule <math>\phi</math> in forma normale.

Adesso, eliminiamo tutte le variabili libere da <math>\phi</math> quantificandole esistenzialmente: se poniamo che <math>x_1, \dots, x_n</math> sono libere in <math>\phi</math>, formiamo <math>\psi_\phi = \exists x_1 \dots \exists x_n \phi</math>. Se <math>\psi_\phi</math> è vera in qualche struttura <math>M</math>, allora esiste un'assegnazione su <math>M</math> alle variabili <math>x_1, \dots, x_n</math> che verifica <math>\phi</math> in <math>M</math>, quindi <math>\phi</math> è soddisfacibile; se invece <math>\psi_\phi</math> è insoddisfacibile, allora <math>\neg\psi_\phi \equiv \forall x_1 \dots \forall x_n \neg \phi</math> è sempre vera e quindi, in ogni struttura <math>M</math>, ogni assegnazione su <math>M</math> alle variabili <math>x_1, \dots, x_n</math> verifica <math>\neg\phi</math>, quindi <math>\phi</math> è insoddisfacibile. Possiamo allora restringerci alle sole formule <math>\phi</math> che sono ''enunciati'', cioè formule senza variabili libere.

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

=== Ridurre il teorema a formule di grado 1 ===
La nostra formula generica <math>\phi</math> 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 <math>\mathrm R</math>. Dobbiamo dimostrare che ogni formula in <math>\mathrm R</math> è insoddisfacibile solo se è refutabile. Data la nostra formula <math>\phi</math>, raggruppiamo stringhe di quantificatori dello stesso tipo in blocchi:

: <math>\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 </math>

Definiamo il '''grado''' di <math>\phi</math> come il numero di blocchi di quantificatori universali separati da blocchi di quantificatori esistenziali nel prefisso di <math>\phi</math>, 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 <math>\phi</math> per cui dobbiamo dimostrare il teorema:

'''Lemma'''. Sia <math>k \ge 1</math>. Se ogni formula in <math>\mathrm R</math> di grado <math>k</math> è soddisfacibile o refutabile, allora lo è anche ogni formula in <math>\mathrm R</math> di grado <math>k + 1</math>.

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

'''Dimostrazione.''' Sia <math>\phi</math> una formula di grado <math>k + 1</math>. Allora, possiamo scriverla come:

: <math>\phi = (\forall x)(\exists y)(\forall u)(\exist v) (P) \psi</math>

dove '''<math>(P)</math>''' è il resto del prefisso di <math>\phi</math> (quindi è di grado <math>k - 1</math>) e <math>\psi</math> è la matrice priva di quantificatori di <math>\phi</math>. <math>x, y, u, v</math> denotano qui ''ennuple'' di variabili invece che singole variabili; per esempio, <math>(\forall x)</math> in realtà sta per <math>\forall x_1 \forall x_2 \dots \forall x_n</math>, dove <math>(x_1, \dots, x_n)</math> sono variabili distinte.

Siano ora <math>x'</math>e <math>y'</math>ennuple di variabili precedentemente inutilizzate, rispettivamente della stessa lunghezza di <math>x</math> e <math>y</math>, e sia <math>Q</math> un simbolo di relazione precedentemente inutilizzato, che accetta un numero di argomenti pari alla somma delle lunghezze di <math>x</math> e <math>y</math>; consideriamo la formula

: <math>\Phi = (\forall x')(\exists y') Q(x',y') \wedge (\forall x)(\forall y)( Q(x,y) \rightarrow (\forall u)(\exist v)(P)\psi )</math>

Chiaramente, <math>\Phi \implies \phi</math>.

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

: <math>( Q(x,y) \rightarrow (\forall u )(\exists v)(P) \psi) \equiv (\forall u)(\exists v)(P) ( Q(x,y) \rightarrow \psi )</math>

E poiché queste due formule sono equivalenti, se sostituiamo la prima con la seconda dentro <math>\Phi</math>, otteniamo la formula <math>\Phi'</math> tale che <math>\Phi \equiv \Phi'</math>:

: <math>\Phi' = (\forall x')(\exist y') Q(x',y') \wedge (\forall x)(\forall y) (\forall u)(\exists v)(P) ( Q(x,y) \rightarrow \psi )</math>

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

: <math>\Psi = (\forall x')(\forall x)(\forall y) (\forall u)(\exists y')(\exists v)(P)Q(x',y') \wedge (Q(x,y) \rightarrow \psi )</math>

e abbiamo <math>\Phi' \equiv \Psi</math>.

Ora <math>\Psi</math> è una formula di grado <math>k</math> e quindi, per ipotesi induttiva, soddisfacibile o refutabile. Se <math>\Psi</math> è soddisfacibile, allora, considerando <math>\Psi \equiv \Phi' \equiv \Phi</math> e <math>\Phi \implies \phi</math>, vediamo che anche <math>\phi</math> è soddisfacibile. Se <math>\Psi</math> è refutabile, allora lo è anche <math>\Phi</math>, che è equivalente ad esso; dunque <math>\neg \Phi</math> è dimostrabile. Ora possiamo sostituire tutte le occorrenze di <math>Q</math> all'interno della formula dimostrabile <math>\neg \Phi</math> 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 <math>\neg \Phi</math>, sostituendo in essa tutte le occorrenze di <math>Q</math> 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 ''<math>Q(x', y')</math>'' in <math>\neg \Phi</math> con la formula <math>(\forall u)(\exists v)(P)\psi[x,y/x',y']</math>. Qui <math>[x,y/x',y']</math> significa che invece di <math>\psi</math> stiamo scrivendo una formula diversa, in cui <math>x</math> e <math>y</math> sono sostituiti con <math>x'</math> e <math>y'</math>. ''<math>Q(x, y)</math>'' è semplicemente sostituito da <math>(\forall u)(\exists v)(P)\psi</math>.

<math>\neg \Phi</math> diventa

: <math>\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 ) )</math>

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

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

=== Dimostrazione del teorema per enunciati di grado 1 ===
Come mostrato nel precedente '''Lemma''', dobbiamo dimostrare il teorema solo per le formule <math>\phi</math> in <math>\mathrm R</math> di grado 1. <math>\phi</math> non può essere di grado 0, poiché le formule in <math>\mathrm R</math> non hanno variabili libere e non usano costanti. Quindi la formula <math>\phi</math> ha la forma generale:

: <math> (\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]</math>

Ora, definiamo un ordinamento delle k-[[Ennupla|uple]] di [[Numero naturale|numeri naturali]] come segue: <math> (x_1, \dots, x_k) < (y_1, \dots, y_k) </math> se e solo se vale almeno una delle seguenti:

* <math> \sum_{i = 1}^k x_i < \sum_{i = 1}^k y_i </math>;
* <math> \sum_{i = 1}^k x_i = \sum_{i = 1}^k y_i </math> e <math> (x_1, \dots, x_k) </math> precede <math> (y_1, \dots, y_k) </math> in [[ordine lessicografico]].

Denotiamo l'ennesima k-upla nell'ordine appena definito con <math> (a^n_1, \dots, a^n_k) </math>.

Poniamo:

* <math> B_n := \phi[z_{a^n_1}, \dots, z_{a^n_k}, z_{(n-1)m+2}, z_{(n-1)m+3}, \dots, z_{nm+1}] </math>;
* <math>D_n := \exists z_1 \dots \exists z_{nm+1} (B_1 \land \dots \land B_n) </math>.

'''Lemma''': Per ogni intero <math>n \ge 1</math>, <math> \phi \implies D_n</math>.

'''Dimostrazione''': Per induzione su <math>n</math>.

Abbiamo:

:<math> \begin{align}
    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^n_1} \dots \forall z_{a^n_k})(\exists y_1 \dots \exists y_m) \phi[z_{a^n_1}, \dots, z_{a^n_k}, y_1, \dots, y_m]
\end{align} </math>

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

Per il caso base, <math> D_1 = \exists z_1 \dots \exists z_{m+1} \phi[z_{a^1_1}, \dots, z_{a^1_k}, 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}] </math> è ovviamente un corollario di <math>\phi</math>. Quindi il '''Lemma''' è dimostrato.

Ora, se <math> D_n </math> è refutabile per qualche <math>n \ge 1</math>, segue che <math>\phi</math> è refutabile. D'altra parte, supponiamo che, per ogni <math>n \ge 1</math>, <math> D_n </math> sia non refutabile. Allora, per ogni <math>n \ge 1</math>, la formula <math>D'_n := B_1 \land \dots \land B_n</math> 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 <math>n \ge 1</math>, esiste un'assegnazione di verità alle distinte sottoformule <math>E_h</math> (ordinate secondo la loro prima occorrenza in <math>D_n'</math>; "distinto" qui è inteso in senso sintattico, ovvero sia predicati distinti, sia variabili distinte) nelle <math> B_i </math>, che rende vera <math>D_n'</math>. Ciò deriva dalla completezza della [[logica proposizionale]] sottostante.

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

Questa assegnazione generale deve rendere vere ciascuna delle <math> B_i </math> e <math>D_n'</math>, poiché se l'assegnazione falsificasse una delle <math> B_i </math>, anche le <math>D'_j</math> sarebbero false per ogni <math> j > n </math>. Ma questo contraddice il fatto che, per costruzione dell'assegnazione generale fino alle <math>E_h</math> che compaiono in <math>D_n'</math>, ci sono infiniti <math> j </math> tali per cui l'assegnazione che avvera <math>D'_j</math> coincide con l'assegnazione generale.

Da questa assegnazione, che rende tutte le <math>D_n'</math> vere, costruiamo un'interpretazione dei predicati del linguaggio che rende vera <math>\phi</math>. Il dominio del modello saranno i [[Numero naturale|numeri naturali]]. Ogni predicato <math>p</math>-ario <math>\Psi</math> è vero su <math>(u_1, \dots, u_p)</math> precisamente quando la formula atomica <math>\Psi(z_{u_1}, \dots, z_{u_p})</math> è vera nell'assegnazione generale, oppure non ha valore di verità (se non compare mai in nessuno dei <math>D_n'</math>).

In questo modello, ciascuna delle formule <math> \exists y_1 \dots \exists y_m \phi[x_1, \dots, x_k, y_1, \dots, y_m] </math> è vera per costruzione su ogni assegnazione <math>\eta</math> tale per cui <math>\eta(x_1) = a_1^n, \dots, \eta(x_k) = a_k^n</math>. Ma questo implica che <math>\phi</math> stessa è vera nel modello, poiché <math>(a^n_1, \dots, a^n_k)</math> può essere qualunque k-upla di numeri naturali. Quindi <math>\phi</math> è soddisfacibile, e abbiamo finito.

==== Spiegazione intuitiva ====
Possiamo scrivere ogni <math> B_i </math> come <math> \phi[x_1, \dots, x_k, y_1, \dots, y_m] </math> per qualche <math>x_1, \dots, x_k</math>, che possiamo chiamare "primi argomenti", e <math>y_1, \dots, y_m</math>, che possiamo chiamare "ultimi argomenti".

Prendiamo <math> B_1 </math>, per esempio. I suoi "ultimi argomenti" sono <math>z_2, z_3, \dots, z_{m + 1}</math>, e per ogni possibile combinazione di <math> k </math> di queste variabili c'è un qualche <math> j </math> tale per cui esse appaiono come "primi argomenti" in <math> B_j </math>. Quindi per <math> n_1 </math> sufficientemente grande, <math> D_{n_1}' </math> ha la proprietà che gli "ultimi argomenti" di <math> B_1 </math> appaiono, in ogni possibile combinazione di <math> k </math> di essi, come "primi argomenti" in altri <math> B_j </math> all'interno di <math> D_{n_1}' </math>. Per ogni <math> B_i </math> c'è un <math> D_{n_i}' </math> con la proprietà corrispondente.

Quindi, in un modello che soddisfa tutti i <math> D_n' </math>, ci sono oggetti corrispondenti a <math>z_1, z_2, \dots</math> e ogni combinazione di <math> k </math> di questi appare come "primo argomento" in qualche <math> B_j </math>, nel senso che per ogni <math> k </math> di questi oggetti <math>z_{p_1}, \dots, z_{p_k}</math> ci sono <math>z_{q_1}, \dots, z_{q_m}</math> che rendono <math> \phi[z_{p_1}, \dots, z_{p_k}, z_{q_1}, \dots, z_{q_m}] </math> vera. Prendendo un sottomodello con solo questi <math>z_1, z_2, \dots</math> oggetti, abbiamo un modello che soddisfa <math>\phi</math>.

== Estensioni ==

=== Estensione al calcolo dei predicati del primo ordine con uguaglianza ===
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 <math>\phi</math> contenente uguaglianze con la formula

: <math> \forall x (x = x) \wedge \forall x \forall y \forall z [x = y \rightarrow (x = z \rightarrow y = z)] </math> <math> \wedge \forall x \forall y \forall z [x = y \rightarrow (z = x \rightarrow z = y)] </math> 
: <br /> <math> \wedge </math> 
: <br /> <math> \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))] </math> 
: <br /> <math> \wedge ... \wedge </math> 
: <br /> <math> \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))] </math> 
: <br /> <math> \wedge \phi </math>

Qui <math>P_1, \dots, P_n</math> denotano i predicati che compaiono in <math>\phi</math> (con <math>k, \dots, m</math> le loro rispettive arità). Se questa nuova formula è refutabile, lo è anche l'originale <math>\phi</math>; 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 <math>\phi</math>.

=== Estensione a insiemi numerabili di formule ===
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 <math> \phi^i </math> di grado 1, possiamo definire <math> B^i_k </math> come sopra; quindi definire <math> D_k </math> come l'unione di <math> B^1_1, \dots, B^1_k, \dots, B^k_1, \dots, B^k_k </math> . Il resto della prova prosegue come prima.

=== Estensione a insiemi arbitrari di formule ===
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 [[Buon ordine|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.

== Note ==

<references>
<ref name = "nota1">{{Cita pubblicazione|cognome=Gödel|nome=K|autore6=Kurt Gödel|titolo=Die Vollständigkeit der Axiome des logischen Funktionenkalküls|lingua=de|volume=37|anno=1930|doi=10.1007/BF01696781}} Lo stesso materiale della tesi, ma con dimostrazioni più brevi, spiegazioni più succinte e senza la lunga introduzione.</ref>
</references>

== Bibliografia ==

* {{Cita pubblicazione|cognome=Gödel|nome=K|autore6=Kurt Gödel|anno=1929|titolo=Über die Vollständigkeit des Logikkalküls|editore=University Of Vienna.}} La prima dimostrazione del teorema di completezza.

== Voci correlate ==
* [[Kurt Gödel]]
* [[Prova ontologica di Gödel]]
* [[Teoremi di incompletezza di Gödel]]
* [[Teorema di completezza di Gödel]]

== Collegamenti esterni ==

* [[Stanford Encyclopedia of Philosophy]]: "[http://plato.stanford.edu/entries/goedel/ Kurt Gödel]" — di Juliette Kennedy.
* Biografia di MacTutor: [http://www-groups.dcs.st-and.ac.uk/~history/Mathematicians/Godel.html Kurt Gödel.]

{{Portale|matematica|filosofia}}

[[Categoria:Logica matematica]]
[[Categoria:Dimostrazioni matematiche]]
[[Categoria:Logica]]
[[Categoria:Kurt Gödel]]
[[Categoria:Teoria dei modelli]]