I teoremi di Godel
Una teoria (o sistema) formale
S si dice coerente se e solo se dalle sue proposizioni non può
derivare alcuna contraddizione (dal punto di vista sintattico, cioè mediante le
regole di deduzione della teoria).
Si dice che S ha un modello se esiste un universo interpretativo
in cui le proposizioni di S sono tutte vere (si dice anche, in tal caso,
che S è soddisfacibile).
Si dice che
T è un teorema di
S se T è derivabile sintatticamente
dagli assiomi
di
S; si dice
invece che T è conseguenza logica di
S se T è
vera in ogni interpretazione che rende veri gli assiomi di
S (punto di
vista semantico, T risulta vera per ogni modello di
S).
I due teoremi seguenti enunciano due importanti proprietà della logica.
Nel 1930 Godel dimostra, per la logica dei predicati del 1° ordine, il teorema di completezza semantica:
Se T è una
conseguenza logica di S, allora T è un teorema di S
(un sistema coerente ha un modello)
L'inverso di questo teorema stabilisce, invece,
la
correttezza semantica.
Una teoria formale S
si dice invece sintatticamente completa se e solo se, per ogni proposizione T
di S, o T
oppure non T è un
teorema
di S
(aggiungendo al sistema, supposto coerente, una formula non
dimostrabile esso perde la coerenza).
Una teoria S si dice assiomatizzata se e solo se l'insieme dei suoi assiomi è decidibile, nel senso che esiste un algoritmo che consente di determinare se una qualsiasi data proposizione di S è o non è un assioma di S. Si dice invece assiomatizzabile se e solo se è equivalente (ha le stesse proposizioni) a una teoria assiomatizzata.
Nel 1931 Godel dimostra un teorema ancora più importante:
I sistemi formali assiomatizzabili, coerenti e sufficientemente espressivi per includere l'aritmetica, sono sintatticamente incompleti.
Infatti, considerato un sistema
S siffatto, costruisce una
formula G, nell'ambito dell'aritmetica, che asserisce che essa stessa non
è dimostrabile;
dimostra poi le due implicazioni:
vale a dire, se G è
dimostrabile allora lo è anche la sua negazione e viceversa.
Quindi, supponendo gli assiomi coerenti, egli ha costruito una proposizione
indecidibile, nel senso che né G, né la sua negazione possono
ricavarsi formalmente dagli assiomi di S (sono cioè teoremi della
teoria).
In altri termini, il sistema S risulta sintatticamente incompleto.
D'altra parte, G non può essere falsa, altrimenti sarebbe dimostrabile e quindi gli assiomi non coerenti; dunque G è una proposizione vera dell'aritmetica, pur essendo indecidibile, il che prova anche l'incompletezza semantica.
In particolare, se gli assiomi della teoria
S per l'aritmetica sono coerenti, si può dimostrare G (esiste una proposizione aritmetica vera che non è dimostrabile a partire dagli assiomi), per cui la teoria risulta contraddittoria: se l'aritmetica è coerente, questo fatto non può, dunque, essere dimostrato nell'ambito dell'aritmetica stessa.