{{TIN064 Skripta}}

Gödelovy věty obecně

Viz Wikipedia - wen:Gödel's%20incompleteness%20theorems. Tradiční znění i důkaz je trochu jiný, zde využijeme vyčíslitelnostní mašinerie, kterou jsme si zavedli.

První věta

Věta: Jakákoliv efektivně generovaná (axiomatizovatelná) teorie schopná vyjádřit základní aritmetiku (Robinsonovu aritmetiku) nemůže být zároveň bezesporná (konzistentní) a úplná (každý pravdivý výrok lze dokázat). Tedy pro každou takovou bezespornou teorii existuje výrok (aritmetický výraz), který není dokazatelný ani vyvratitelný.

Teorie je úplná, když je každá formule dokazatelná nebo vyvratitelná (ekvivalentně: když má právě 1 model). Přirozená čísla jsou jedním z modelů Robinsonovy aritmetiky. První Gödelova věta říká, že můžeme mít tvrzení, která platí o přirozených číslech, ale v aritmetice (ani v její rozšířeních) je nelze dokázat ... aritmetiku nelze "zúplnit".

Zamysleme se nad předpoklady:

  • Teorie T je bezesporná, pokud v ní nelze dokázat zároveň formule F a !F. Ve sporných teoriích dokážeme úplně cokoliv.

  • Teorie T je axiomatizovatelná, jestliže množina dokazatelných formulí v T je rekurzivně spočetná. (Tedy dokážeme o každém výroku v T potvrdit jeho dokazatelnost, neboli existuje program, který postupně generuje všechny dokazatelné výroky v T.)

  • Teorie T je schopná vyjádřit základní aritmetiku, disponuje-li základní aritmetickou silou (definice níže). Díky tomu můžeme v teorii vyjádřit Gödelovými čísly logické formule i ČRF (dokazující výroky teorie) a tak si můžeme dovolit použít vyčíslitelnostní mašinerii.

Pěkná jednoduchá teorie vyhovující našim potřebám je např. wen:Peano%20axioms.

(Má sice nekonečně mnoho axiomů, ale její schémata se přesto dají snadno ověřit, je tedy axiomatizovatelná.)

Druhá věta

Věta: Pokud taková teorie umožňuje dokázat tvrzení o vlastní bezespornosti, je sporná (nekonzistentní).

Neboli v teorii T nelze dokázat vlastní bezespornost. (TODO: nepatrně silnější předpoklady.)

Dále se jí zde nebudeme příliš zabývat.

Aritmetika vs. ČRF

Teorie základní aritmetické síly je popsaná jazykem prvního řádu s

  • numerálem pro nulu

  • numerálem pro jedničku

  • funkčními symboly pro sčítání a násobení

Vlastně je to minimum, co nám stačí k popisu přirozených čísel. Excelentním příkladem je Peanova aritmetika.

Ve Strojilovi najdeme ještě požadavek na konečně mnoho axiomů. To však třeba v Peanově aritmetice nejde, tam máme pro sčítání a násobení tzv. axiomová schémata a pro každou dvojici čísel vlastně zvlášť axiom o výsledku násobení a sčítání - jsme totiž v logice prvního řádu. V praxi je ale důležitá axiomatizovatelnost, a ta v případě takového schématu není problém.

ČRF je reprezentovatelná v ZAS teorii T, existuje-li formule, která popisuje ČRF ve smyslu věty o selektoru a zároveň je v T dokazatelná vždy, když ČRF zkonverguje. (Formálně viz Strojil.)

Věta: ČRF je reprezentovatelná v libovolné teorii ZAS. (Pozn. - nejspíše je třeba axiomatizovatelnost?)

Důkaz zhruba: Podle věty o selektoru ČRF odpovídá nějaký RSP. Podle Matisjevičovy věty (!) tomu RSP odpovídá diofantický predikát, tedy existenční predikát o rovnosti dvou polynomů. (Polynom je něco v teorii ZAS jistě vyjádřitelné. Vlastně se na ZAS můžeme dívat jako na jazyk právě tak silný, abychom v něm mohli reprezentovat polynomy.)

Důkaz pořádně: Museli bychom si rozmyslet, jak pouze pomocí přirozených čísel vlastně něco dokazovat (navíc s existenčním kvantifikátorem). Neřešíme...

Gödelovy věty ve vyčíslitelnosti

Naformulujme si věty ještě jednou, tentokrát trochu jiným jazykem:

Nechť T je teorie logiky 1. řádu, má základní aritmetickou sílu a je bezesporná.

Předvěta: Množina formulí dokazatelných v T není rekurzivní.

První věta: Je-li T navíc axiomatizovatelná, existuje uzavřená formule F taková, že F je nerozhodnutelná v T (tj. není dokazatelná ani F ani její negace).

V původní verzi jsme mluvili o pravdivosti a dokazatelnosti; mluvit o rozhodnutelnosti je to samé, stačí se paralelně zajímat opět o F i ¬F.

Důkaz Gödelovy věty

Dříve se Gödelovy věty vyčíslitelností dokazovaly pomocí produktivních množin (wen:Creative_and_productive_sets%23Applications_in_mathematical_logic). To je ale zbytečně složité, my na to půjdeme přes efektivně neoddělitelné množiny.

Neformálně - budeme chtít dokázat, že v rozumných (axiomatizovatelných, ZAS) teoriích je množina dokazatelných a vyvratitelných formulí efektivně neoddělitelná dvojice; přitom přímo z definice efektivně neoddělitelných dvojic pak máme k dispozici efektivní proceduru, jak vygenerovat prvek mimo tyto množiny. Ten bude buď pravdivý, nebo nepravdivý, každopádně nebude dokazatelný ani vyvratitelný, proto (dokonce konstruktivně!) dokážeme Gödelovu větu.

Lemma 1: Příslušnost prvku do disjunktní dvojice rekurzivně spočetných množin A, B můžeme popsat rekurzivně spočetným predikátem:

x ∈ A ⇒ ⊢<sub>T</sub>   G(x)<br/>

x ∈ B ⇒ ⊢<sub>T</sub> ¬G(x)

(Pro prvky mimo A a B je predikát G(x) nerozhodnutelný. G je spíše takové "parametrizovatelné predikátové schéma", ze kterého konkrétní predikát vyrobí až x. Měli-li bychom být formálně přesní, jako parametr bychom místo x mohli předat Gödelovo číslo x.)

Důkaz: Z charakteristických funkcí A a B snadno zkontruujeme ČRF φ(x)\varphi(x), která bude nabývat 0 pro x∈Ax \in A, 1 pro x∈Bx \in B a v ostatních případech nedoběhne. Podle věty o selektoru a věty o reprezentovatelnosti ČRF v ZAS bude tedy existovat i predikát G(x). Není úplně jasné, jak formálně pojmout relaci ⊢<sub>T</sub> — můj osobní dojem je, že úlohu "dokazovače" zastane právě ČRF φ(x), která garantuje, že v takovém případě doběhne. Pravděpodobně to ale není vše. ±QED.

Vezměme libovolnou efektivně neoddělitelnou dvojici rekurzivně spočetných množin A, B (dokázali jsme v minulé kapitole, že nějaká taková existuje, dokonce opět konstruktivně). Množiny A, B jsou z definice disjunktní, tedy dle lemmatu 1 existuje RSP G(x).

Musíme se pojistit proti případu, že by G(x) bylo dokazatelné (třeba jinou metodou než přes φ(x)\varphi(x)?) i pro nečekaná x mimo A, B. Definujme si proto novou dvojici množin A', B':

A' = {x | ⊢<sub>T</sub>   G(x) }<br/> B' = {x | ⊢<sub>T</sub> ¬G(x) }

Snadno si uvědomíme, že tímto "rozšířením přes dokazatelnost" jsme si nepokazili klíčové vlastnosti:

  • A ⊆ A', B ⊆ B'

  • A' ∩ B' = Ø (z bezespornosti T)

  • A' a B' jsou rekurzivně spočetné (z axiomatizovatelnosti)

  • A' a B' jsou efektivně neoddělitelná dvojice (A, B tvoří efektivně neoddělitelnou dvojici; A', B' jsou RSM nadmnožiny, tedy stačí použít stejnou separující funkci, jako používaly A, B)

Důkaz předvěty: Sporem - nechť množina všech dokazatelných formulí je rekurzivní. Pak je rekurzivní i množina vyvratitelných formulí. Nejsou rekurzivně neoddělitelné, anžto jsou samy sobě separujícími množinami. Tedy nejsou ani efektivně neoddělitelné. Jsou to však jistě nadmnožiny A' a B', které efektivně neooddělitelná je, a to je spor s definicí efektivní neoddělitelnosti. QED? (Skrytě předpokládáme axiomatizovatelnost, takže to jde asi i jinudy...)

Důkaz Gödelovy věty: Spusťme separující funkci A', B' s jejich kódy (jsou to RSM). Prvek x, který vyrobíme, je mimo A' i B'. Vyrobme predikát G(x), ten tedy je buď pravdivý, ale nedokazatelný (jinak by byl v A'), nebo nepravdivý, ale nevyvratitelný (jinak by byl v B'). Tedy je nerozhodnutelný. QED