Il teorema di completezza di Gödel è un teorema fondamentale della logica matematica ottenuto dal logico Kurt Gödel nel 1929. Esso stabilisce una corrispondenza tra validità logica e dimostrabilità logica nella logica del primo ordine.

Una formula del primo ordine è detta logicamente valida se è vera in ogni struttura del suo linguaggio. Il teorema di completezza mostra come se una formula è valida, allora esiste una prova della formula, ottenibile in numero finito di passi. La deduzione è dunque verificabile a mano o al calcolatore. La relazione tra verità e dimostrabilità stabilisce uno stretto legame tra teoria dei modelli e teoria della dimostrabilità nella logica matematica.

Un'importante conseguenza del teorema di completezza è che è possibile enumerare le conseguenze logiche di ogni teoria del primo ordine, enumerandone tutte le deduzioni corrette usando gli assiomi della teoria.

I teoremi di incompletezza di Gödel, riferendosi ad un differente significato di completezza, mostrano che, se una formalizzazione di sufficiente potenza dell'aritmetica è consistente, allora esiste una formula F, dipendente dalla formalizzazione scelta, di cui non si può dimostrare né la verità, né la verità della sua negazione.

Sono stati proposti numerosi sistemi di deduzione per la logica del primo ordine, come la deduzione naturale o il sistema deduttivo di Hilbert. In comune a tutti questi sistemi c'è la nozione di deduzione formale che può essere, a seconda dei casi, una sequenza o un albero di formule nella quale ogni passaggio da una formula all'altra è giustificata da una regola di deduzione definita nel sistema stesso. L'ultima di queste formule è considerata la conclusione del teorema. La definizione delle regole deduttive e la definizione di deduzione formale è tale che ogni dimostrazione può essere verificata con un algoritmo, e quindi da un computer.

Ogni formula è espressa in un linguaggio specifico ed è definita logicamente valida se è vera in ogni struttura di tale linguaggio. Per enunciare, e quindi dimostrare, il teorema di completezza, è necessario anche scegliere un sistema di deduzione. Quest'ultimo è definito completo se ogni formula logicamente valida è la conclusione di qualche deduzione formale. In altre parole in un sistema deduttivo completo ogni formula vera è dimostrabile. In questo senso ci sono molti teoremi di completezza, uno per ogni sistema deduttivo completo.

Il teorema di completezza di Gödel afferma che un sistema deduttivo per la logica dei predicati del primo ordine è "completo" nel senso che le regole di deduzione permettono di dimostrare tutte le formule logicamente valide. Un altro aspetto dello stesso problema è il teorema di correttezza che afferma che tutte le formule dimostrabili sono logicamente valide. Questi due teoremi, se dimostrati entrambi, implicano che una formula è logicamente valida se e solo se è dimostrabile (cioè è conclusione di una deduzione formale).

In verità si può dimostrare una versione più generale del teorema di completezza. Questa versione afferma che, per ogni teoria del primo ordine T e per ogni formula chiusa S nello stesso linguaggio della teoria, esiste una deduzione formale di S a partire da T se e solo se S è verificata in ogni modello di T. Questa versione più generale è usata implicitamente, ad esempio, quando si dimostra che una affermazione è dimostrabile a partire dagli assiomi della teoria dei gruppi prendendo un gruppo arbitrario e mostrando che tale affermazione è soddisfatta in quel preciso gruppo

La branca della logica matematica che studia proprietà generali dei modelli si chiama teoria dei modelli. La teoria della dimostrazione studia cosa può essere formalmente dimostrato in un particolare sistema formale. Il teorema di completezza stabilisce un collegamento fondamentale tra questi due mondi perché collega la semantica con la sintassi. Il teorema di completezza non deve comunque essere sopravvalutato confondendo i due concetti di completezza: il celeberrimo teorema di incompletezza dello stesso Gödel, mostra che ci sono insormontabili limitazioni a quello che si può raggiungere con una dimostrazione matematica. Il nome del teorema di incompletezza si riferisce infatti ad un altro senso del termine completo: il teorema di completezza dice che tutte le formule che sono conseguenza logica di una teoria sono dimostrabili, il teorema di incompletezza dice che alcune formule non sono dimostrabili né, tantomeno, sono conseguenza logica di una certa teoria.

Una conseguenza importante del teorema di completezza è il fatto che le formule logicamente valide (e quindi dimostrabili) di una teoria sono solo una quantità numerabile. La definizione di formula logicamente valida riguarda contemporaneamente tutte le strutture di un particolare linguaggio, e quindi non fornisce direttamente un algoritmo per verificare la validità di una formula. Inoltre, per via del teorema di incompletezza, l'insieme delle formule logicamente valide non può essere decidibile. Tuttavia il teorema di completezza implica che l'insieme delle formule che sono conseguenze di una teoria consistente è numerabile: l'algoritmo dovrebbe prima, quindi, numerare tutte le deduzioni formali che si possono ottenere dalla teoria, e usare questo per numerare le conclusioni di ogni deduzione. La natura sintattica delle deduzioni formali che sono sequenze o alberi finiti rende possibile la costruzione di questo algoritmo.

Il teorema di completezza e il teorema di compattezza sono due pietre d'angolo per la logica del primo ordine. Anche se nessuno di questi due teoremi viene dimostrato dettagliatamente, ognuno può essere dedotto assumendo l'altro.

Il teorema di compattezza afferma che se una formula φ è conseguenza logica di un insieme di formule Γ (potenzialmente infinito) allora è anche conseguenza di un sottoinsieme finito di Γ. Questa è una conseguenza diretta del teorema di completezza, perché solo un numero finito di ipotesi contenute in Γ può essere utilizzato in una dimostrazione formale di φ, e il teorema di correttezza assicura che φ è quindi conseguenza logica di questo insieme finito di ipotesi. Questa dimostrazione del teorema di compattezza è quella originariamente utilizzata da Gödel.

D'altro canto, in molti sistemi deduttivi, è possibile dimostrare il teorema di completezza a partire dal teorema di compattezza.

Si può misurare l'inefficacia del teorema di completezza in due modi: in teoria degli insiemi e in matematica inversa. In teoria degli insiemi, il lemma dell'ultrafiltro è una versione debole dell'assioma della scelta che non è dimostrabile in ZF, il sistema di assiomi di Zermelo e Fraenkel. In ZF si dimostra che i teoremi di completezza e compattezza sono equivalenti, e che entrambi sono equivalenti al lemma dell'ultrafiltro. In matematica inversa vengono considerate solo strutture e teorie numerabili. In questo contesto i teoremi di completezza e di compattezza sono equivalenti tra loro ed entrambi sono equivalenti al sistema di assiomi WKL₀, con l'equivalenza dimostrabile in RCA₀. In particolare, sebbene ogni teoria del primo ordine consistente e numerabile abbia un modello finito o numerabile, come conseguenza del teorema di completezza e del teorema di Löwenheim-Skolem, si conclude che ci sono effettivamente teorie del primo ordine che non hanno modelli calcolabili.

La completezza è una proprietà fondamentale della logica del primo ordine che non è valida per tutte le logiche. La logica del second'ordine, ad esempio, non ha un teorema di completezza per la semantica standard (ha invece la completezza per la semantica di Henkin), e lo stesso vale per tutte le logiche di ordine superiore. È quindi possibile costruire dei sistemi deduttivi corretti in una logica di ordine superiore, ma tali sistemi non saranno completi. Inoltre l'insieme delle formule logicamente valide in una logica del second'ordine non è ricorsivamente enumerabile.

Un teorema di completezza può essere dimostrato per la logica modale usando la semantica di Kripke.

Lo stesso argomento in dettaglio: Dimostrazione originale del teorema di completezza di Gödel.

La dimostrazione originaria di Gödel riduce il problema generale al caso particolare di formule espresse in una determinata forma sintattica, e poi conclude con un ragionamento ad hoc.

Nei testi di logica contemporanei, il teorema di completezza è piuttosto dimostrato con la dimostrazione di Henkin che costruisce direttamente un modello per ogni teoria consistente del primo ordine a partire dai termini del linguaggio. Nel 2004 James Margetson ha sviluppato una dimostrazione completamente computerizzata usando il programma Isabelle [1], e ulteriori dimostrazioni sono disponibili.

• Teorema di Henkin
• Teoremi di incompletezza di Gödel
• Dimostrazione originale del teorema di completezza di Gödel

• (EN) Gödel’s completeness theorem, su Enciclopedia Britannica, Encyclopædia Britannica, Inc.
• (EN) Eric W. Weisstein, Teorema di completezza di Gödel, su MathWorld, Wolfram Research.

Portale Matematica: accedi alle voci di Teknopedia che trattano di matematica