Gödelova věta o úplnosti predikátové logiky

Gödelova věta o úplnosti predikátové logiky (také jen Gödelova věta o úplnosti či věta o úplnosti) je základní větou matematické logiky. Dává do souvislosti syntaktický pojem dokazatelnosti a sémantický pojem pravdivosti v modelu.

Tvrdí, že v každé predikátové teorii prvního řádu je jakákoli formule dokazatelná právě tehdy, když platí v každém modelu této teorie.

Větou o úplnosti se obvykle nazývá následující ekvivalence. Implikace zleva doprava se někdy nazývá věta o korektnosti.

Formule ${\displaystyle \varphi }$ je dokazatelná v teorii T, právě když ${\displaystyle \varphi }$ platí v každém modelu T.

Teorie S je bezesporná, právě když má nějaký model.

Zde S představuje teorii T s přidaným axiomem „neplatí ${\displaystyle \varphi }$“. Ta je sporná, právě když je ${\displaystyle \varphi }$ dokazatelná v T.

Gödelova věta o úplnosti má zásadní význam pro matematickou logiku. Například z ní vyplývá, že

• Každá bezesporná teorie má model.
• Z toho pak věta o kompaktnosti: má-li každá konečná podteorie (tj. podmnožina axiomů) teorie ${\displaystyle \varphi }$ model, pak je teorie ${\displaystyle \varphi }$ je bezesporná (důkaz sporu by využíval jen konečně mnoho axiomů) a tedy má model.
• Z toho dále Löwenheim-Skolemova věta
• A z ní plyne, že má-li teorie s nejvýše spočetně mnoha symboly jakýkoli nekonečný model, pak má model libovolné nekonečné mohutnosti.

Věta o úplnosti říká, že systém dokazování v predikátové logice prvního řádu je

• Korektní, tj. neprokáže žádnou formuli, která neplatí v každém modelu.
• Úplný (odtud název věty), tj. prokáže každou formuli, která platí ve všech modelech.

Tím se dokazatelnost formulí (v libovolné predikátové teorii prvního řádu, která má jen konečně, případně spočetně mnoho symbolů) redukuje na existenci formálního důkazu. Tím je konečná posloupnost znaků z nějaké konečné množiny. Pro počítač je snadné i velmi dlouhou posloupnost znaků ověřit, zda je nebo není důkazem dané formule.

Počítače také mohou odvozovat posloupnosti formulí, a tak hledat důkaz zkoumané formule v určité teorii. Tj. rozhodovat o libovolné matematické hypotéze, zda je dokazatelná v této teorii. Teoreticky by se toho dalo využít i pro hledání neznámých pravdivých formulí ve velkých teoriích typu Peanovy aritmetiky či ZFC, ale toto je v současnosti (2025) výpočetně neúnosně náročné. V praxi se využívá jen ve vybraných vědních oborech jako je algebra a při dokazování jednoduchých tvrzení.

Softwarem pro strojové dokazování formulí a verifikací důkazů je například programovací jazyky Lean, Idris a Mathematica.

Větu o úplnosti dokázal poprvé v roce 1929 Kurt Gödel, v současné době se však častěji uvádí důkaz podaný později Leonem Henkinem.

Použijme název „teorie ekvivalencí“ pro teorii s jedním binárním predikátem ~ a axiomy:

${\displaystyle (\forall x)x\sim x\;\;\;}$ (reflexivita)

${\displaystyle (\forall x,y)x\sim y\implies y\sim x\;\;\;}$ (symetrie)

${\displaystyle (\forall x,y,z)x\sim y\land y\sim z\implies x\sim z\;\;\;}$ (Tranzitivita: pokud ${\displaystyle x}$ je v relaci s ${\displaystyle y}$ a ${\displaystyle y}$ se ${\displaystyle z}$, pak ${\displaystyle x}$ je v relaci se ${\displaystyle z}$.)

Příkladem modelu této teorie je

• Množina všech přímek v rovině, kde ${\displaystyle \sim }$ reprezentuje rovnoběžnost.
• Množina celých čísel, kde ${\displaystyle a\sim b}$ právě když jejich rozdíl je sudý.

Formule ${\displaystyle (\forall x,y,u,v)x\sim y\land y\sim u\land u\sim v\implies x\sim v}$ (tj. jakási „prodloužená tranzitiva“) je z těchto axiomů dokazatelná, a proto platí v každém modelu.

Formule ${\displaystyle (\exists x,y)x\not \sim y}$ není dokazatelná ani vyvratitelná, a proto v některých modelech teorie ekvivalencí neplatí (množina všech přímek v rovině s relací rovnoběžnosti) a v jiných platí (množina všech přímek v rovině rovnoběžných s osou x, opět s relací rovnoběžnosti).

Formule ${\displaystyle (\exists x)x\not \sim x}$ je vyvratitelná (tj. její negace je dokazatelná), a proto neplatí v žádném modelu teorie ekvivalencí.

• Gödelovy věty o neúplnosti
• Věta o kompaktnosti