Gödelova věta: neúplnost formálních systémů

Věta o neúplnosti Gödela: Proč je formální matematika omezená

V roce 1931 dokázal Kurt Gödel zásadní omezení každé dostatečně silné formální aritmetické soustavy. Jeho věty o neúplnosti ukázaly, že není možné vytvořit bezesporný systém, který by dokázal všechna pravdivá tvrzení o přirozených číslech. Tento objev rozptýlil snovou představu o úplné formalizaci celé matematiky.

Trend sjednocování ve vědě a matematice

Na přelomu 19. a 20. století se věda vykazovala silným směrem k unifikaci. Newton spojil pozemskou gravitaci s nebeskou mechanikou. Maxwell sjednotil elektřinu, magnetismus a světlo do jednoho elektromagnetického pole. Darwin vysvětlil rozmanitost života pomocí přirozeného výběru.

Matematici usilovali o podobný syntézis: odvodit aritmetiku, geometrii i matematickou analýzu z jediného souboru axiomů. Gottlob Frege navrhl definici čísel prostřednictvím teorie množin:

• 0 = ∅ (prázdná množina)
• 1 = {∅}
• 2 = {∅, {∅}}

Následník čísla n byl definován jako sjednocení všech předchozích čísel. To umožnilo formální zavedení aritmetiky. Paradox Russella však celý systém zničil: z axiomů vyplývalo rozporové tvrzení „množina všech množin, které sebe sama neobsahují“.

Základní krize a Hilbertův program

Paradox Russella vyvolal krizi základů matematiky. David Hilbert navrhl ambiciózní program formalizace:

• Úplnost (K): systém dokáže všechna pravdivá tvrzení aritmetiky.
• Bezespornost (K): systém nedokáže žádné nepravdivé tvrzení.
• Rozhodnutelnost: existuje algoritmus pro ověření, zda je dané tvrzení dokazatelné.

Hilbert požadoval metamatematický důkaz těchto vlastností pro konečný soubor axiomů.

Principia Mathematica Russella a Whiteheada

Bertrand Russell a Alfred North Whitehead vytvořili Principia Mathematica (PM) — axiomatický logický systém dostatečně silný pro celou matematiku. Formálně odvodili aritmetiku od nuly a dokázali například 1+1=2 až na více než 300 stranách.

Pro svou analýzu Gödel zjednodušil syntaxi PM na jazyk podobný PM-Lisp:

| Symbol | Význam | Příklad |

|--------|--------|---------|

| 0 | nula | 0 |

| next | následník | (next 0) |

| + | sčítání | (+ 0 (next 0)) |

| | násobení | ( 0 (next 0)) |

| = | rovnost | (= 0 (* 0 (next 0))) |

Logické operátory:

| Symbol | Význam | Příklad |

|--------|--------|---------|

| not | negace | (not (= 0 1)) |

| or | disjunkce | (or (= 0 1) (not (= 0 1))) |

| when | implikace | (when 0 (or 0 1)) |

| there-is | existenční kvantifikátor | (there-is x (= 4 (* x 2))) |

Axiomy PM zahrnovaly tautologie:

• (when (or p p) p)
• (when p (or p q))
• Komutativita a asociativita disjunkce
• Pravidlo sylogismu

Z nich se pak odvozovaly rovnost i aritmetické operace.

Gödelovo číslování: kódování syntaxe

Gödel použil Cantorovo kódování k reprezentaci formulí přirozenými čísly. Každému symbolu přiřadil jedinečné číslo (tzv. prvočíselné Gödelovo číslo):

| Symbol | Gödelovo číslo |

|--------|----------------|

| ( | 1 |

| ) | 3 |

| 0 | 5 |

| next | 7 |

| + | 9 |

| * | 11 |

| = | 13 |

| not | 15 |

| or | 17 |

| when | 19 |

| there-is | 21 |

| a,b,c... | 2,4,6... |

Formule (there-is a (= (next 0) a)) se nejprve rozloží na posloupnost tokenů, poté se vypočte Gödelovo číslo G = 2^{g₁} × 3^{g₂} × 5^{g₃} × ..., kde gᵢ jsou čísla jednotlivých tokenů. Toto zobrazení je bijekcí mezi formulemi a přirozenými čísly.

Aritmetika v PM-Lispu je vyjádřitelná uvnitř samotného systému: délka formule, substituce, dokazatelnost — vše se redukuje na primitivně rekurzivní funkce.

Samoreference a věta o neúplnosti

Gödel zkonstruoval formuli G, která tvrdí svou vlastní nedokazatelnost: ∃p Proof(p, ⌜G⌝) — „neexistuje důkaz s číslem p pro mě“.

Podle diagonálního lemmatu (pevný bod):

G ≡ ¬Provable(⌜G⌝)

Věta 1: Pokud je PM bezesporná, pak G je pravdivá, ale v PM nedokazatelná.

Věta 2: Pokud je PM bezesporná, pak Con(PM) (bezespornost PM) je v PM nedokazatelná.

Co je klíčové:

• Každý systém, který interpretuje Peanovu aritmetiku, je neúplný.
• Bezespornost systému nelze dokázat uvnitř tohoto systému.
• Čísla kódují syntaxi, čímž vzniká samoreference.
• Hilbertův program je neuskutečnitelný.
• Pravdivost ≠ dokazatelnost.

Důsledky pro informatiku

Gödelova věta je ekvivalentní problému zastavení (halting problem) podle Turinga. Formální systémy mají „slepá místa“. V programování to znamená:

• Existence nerovnovážných funkcí (např. „orákulum zastavení“).
• Logické „bombičky“ v nástrojích pro verifikaci kódu.
• Omezení formální verifikace softwaru.

Současné systémy (např. Coq, Lean) tyto limity uvědomují a spoléhají na tzv. axiomy důvěry.

— Editorial Team