{{TIN064 Skripta}}

## Gödelovy věty obecně ##

Viz Wikipedia - [wen:Gödel's incompleteness theorems](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#Applications_in_mathematical_logic](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 $\varphi(x)$, která bude nabývat 0 pro $x \in A$, 1 pro $x \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 $\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