Gedelova teorema o potpunosti

Gedelova teorema o potpunosti je teorema matematičke logike koju je dokazao Kurt Gedel u svojoj doktorskoj disertaciji 1929. i kasnije u radu objavljenom 1930. U svom najpoznatijem obliku, ona tvrdi da je u predikatskom računu prvog reda svaka logički valjana formula dokaziva. Ovo je jedna od najvažnijih teorema matematičke logike, jer pokazuje da klasičan predikatski račun „sadrži“ sve zakone logike koji se mogu iskazati predikatskim formulama.

U formulaciji Gedelove teoreme o potpunosti, reč dokaziva je sintaktičke prirode: ona označava da postoji formalno izvođenje formule u teoriji u pitanju, u ovom slučaju u predikatskom računu prvog reda. Takvo izvođenje–dokaz je konačan spisak koraka u kojem se svaki korak ili poziva na aksiomu teorije ili se dobija iz prethodnih koraka primenom osnovnih pravila zaključivanja. Kada je takvo izvođenje dato, ispravnost svakog od koraka se može proveriti algoritamski (na primer, pomoću računara, ili ručno). Pojam valjane formule, pak, je semantički: formula je valjana ako je tačna u svakom modelu jezika formule (odnosno svaka takva interpretacija je i jedan njen model).

Gedelova teorema o potpunosti pokazuje da su aksiome i pravila zaključivanja predikatskog računa prvog reda „potpuni“ u smislu da nikakve dodatne aksiome ili pravila zaključivanja nisu potrebni kako bi se izvele sve logički valjane formule. Komplementarno svojstvo je ispravnost (semantička konzistentnost ili neprotivurečnost). Teorema o ispravnosti tvrdi da je predikatski račun prvog reda semantički ispravan, odnosno da se u njemu mogu izvesti jedino logički valjana tvrđenja. Ponekad se teorema o ispravnosti tretira kao deo jednog, sveobuhvatnog iskaza o potpunosti, poput formulacije samog Gedela iz 1929., koja u osnovi glasi:

Postoji račun predikatske logike prvog reda takav da za svaki skup formula Γ i svaku formulu φ važi: φ sledi iz Γ ako i samo ako se φ može izvesti iz Γ u ovom računu.

Teorema o potpunosti ustanovljava temeljnu vezu između semantike (teorije modela, koja izučava šta je tačno u različitim interpretacijama) i sintakse (teorije dokaza, koja izučava šta se može dokazati u pojedinačnim formalnim sistemima). Ako $\vDash$ označava semantičku posledicu i $\vdash$ izvedivost u računu, gornja Gedelova teorema glasi

$\Gamma \vDash \varphi \,\Leftrightarrow \,\Gamma \vdash \varphi$.

Ovde, smer zdesna nalevo odgovara ispravnosti, a sleva nadesno potpunosti računa. Slabiji iskaz Gedelove teoreme o potpunosti citiran na početku članka, odgovara slučaju kada je Γ prazan skup formula (zapravo se može dokazati da su „slabiji“ i „jači“ iskaz ekvivalentni). Ova teorema, međutim, ne ukida niti marginalizuje razliku između ova dva pristupa. U stvari, drugi rezultat koji je proslavio Gedela, njegova teorema o nepotpunosti, pokazuje da postoje suštinska ograničenja u pogledu toga šta se u matematici može postići formalnim dokazima: konkretno, da se unutar dovoljno bogatih teorija ne može svaka dokazati svaki valjan iskaz. (Pažnja: ime Gedelove teoreme o nepotpunosti se odnosi na drugo značenje reči „potpun“. Vidi članak Teorija modela.)

Gedelova teorema o potpunosti uspostavlja teorijsku osnovu automatskih dokazivača, dakle izradi i proveri dokaza pomoću računarskih programa. Prvobitno je činila i prvi korak u okviru Hilbertovog programa (izrada potpunog i neprotivurečnog računa za celu matematiku), sve dok program nije dotučen upravo Gedelovom teoremom o nepotpunosti.

Ideja dokaza

Izvorni Gedelov dokaz se danas uglavnom više ne koristi. Umesto njega, obično se upotrebljava sledeća „Osnovna teorema logike prvog reda“, koju je formulisao Henkin 1949.:

Svaki konzistentan skup formula ima model.

Ovde se konzistentnost odnosi na sintaksni pojam: kažemo da je skup formula Γ konzistentan (neprotivurečan), ako se iz njega u datom računu ne može izvesti kontradikcija, odnosno ne postoji formula φ takva da je $\Gamma \vdash \varphi$ i $\Gamma \vdash \lnot \varphi$.

Teorema o potpunosti se može jednostavno dokazati pretpostavljajući ovu teoremu. I zaista, pretpostavimo da je $\Gamma \vDash \varphi$, ali nije $\Gamma \vdash \varphi$. Račun ima svojstvo da se konzistentnom skupu formula može pridružiti negacija formule koja se iz njega ne može izvesti pri čemu je i novodobijeni (brojniji) skup formula i dalje konzistentan. U našem slučaju, $\Gamma \cup \{\lnot \varphi \}$ je takođe konzistentan skup formula i prema Henkinovoj teoremi ima model. U takvom modelu je, međutim, φ netačna, suprotno pretpostavci da je u pitanju valjana formula.

Uopštenja i veze sa drugim tvrđenjima

Važi i sledeći opštiji oblik Gedelove teoreme o potpunosti:

U svakoj teoriji prvog reda T, za datu rečenicu S u jeziku ove teorije postoji izvođenje S iz T ako i samo ako je S zadovoljena u svakom modelu teorije T.

Teorema o potpunosti je središnje svojstvo logike prvog reda i ne vredi u drugim logikama. Logika drugog reda, na primer, nema svoju teoremu o potpunosti. Takođe, potpunost je svojstvo pojedinačnog računa P (oznaka $\vdash$ za izvedivost zapravo označava $\vdash _{P}$) i dokaz se izvodi za konkretan pojedinačan račun. Gedel je svoju teoremu dokazao u Hilbertovom računu. Takođe potpun je, na primer, Gencenov račun sekvenata, oblika prirodne dedukcije.

Gedelova teorema o potpunosti je ekivivalentna lemi o ultrafiltrima, slabom obliku aksiome izbora, u smislu da se ekvivalencija može dokazati u Zermelo-Frenkel teoriji skupova bez aksiome izbora (ZF).

Izvorni dokazi

• Kurt Gedel, „O potpunosti logičkog računa“ (Kurt Gödel, "Über die Vollständigkeit des Logikkalküls"), doktorska disertacija, Univerzitet u Beču, 1929. Ova disertacija sadrži izvorni dokaz teoreme o potpunosti.
• Kurt Gedel, „Potpunost aksioma logičkog funkcijskog računa“ (Kurt Gödel, "Die Vollständigkeit der Axiome des logischen Funktionen-kalküls"), Monatshefte für Mathematik und Physik 37 (1930), 349-360. Ovaj članak sadrži isti materijal kao disertacija, ali u prerađenom i skraćenom obliku. Dokazi i objašnjenja su kraći i izostavljen je dugačak uvod.