Student World

 Svůj výsledek o neúplnosti aritmetiky (tzv. první Goedelovu větu) poprvé oznámil na konferenci v Královci 7. října 1930, slavný článek s podrobným důkazem a navíc významným důsledkem (tzv. druhou Goedelovou větou) vyšel na počátku roku 1931.

Obě Goedelovy věty odhalují závažné skutečnosti o formálních systémech, ve kterých se pokoušíme systematizovat způsoby našeho usuzování, například při dokazování vět v matematice. Formální systém aritmetiky sestává z axiomů (např. „Každé přirozené číslo má svého následovníka.“) a logických odvozovacích pravidel (např. modus ponens: „Jestliže z tvrzení A vyplývá tvrzení B a zároveň platí tvrzení A, pak platí i tvrzení B.“). Všechny axiomy formálního systému považujeme za dokázané. Za dokázané dále prohlásíme každé tvrzení, které lze z axiomů odvodit opakovaným použitím odvozovacích pravidel.

První Goedelova věta říká, že jestliže je bezesporný formální systém dostatečně bohatý (zahrnuje alespoň aritmetiku), pak v něm vždy existuje nějaké nerozhodnutelné tvrzení, které nelze ani dokázat, ani vyvrátit (tj. dokázat jeho negaci). Druhá Goedelova věta říká, že v takovém systému se nám nikdy nemůže podařit dokázat jeho vlastní bezespornost.

Počin Kurta Goedela je srovnatelný se zásadními „koperníkovskými obraty“ v jiných oborech lidského bádání, jako byla např. transcendentální reflexe Immanuela Kanta ve filozofii (poznání je významně determinováno subjektem a nikoliv pouze objektivní realitou), Darwinova teorie v biologii (živí tvorové včetně člověka nejsou projektem nějakého tvůrce, nýbrž výsledkem působení evolučních zákonů) či revoluce Alberta Einsteina ve fyzice (prostor a čas nejsou absolutní, ale jsou formovány hmotou a energií). Poselství Kurta Goedela volně řečeno zní: Naše racionální usuzování ztělesněné ve formálních logických systémech bude vždy zaostávat za vyjadřovacími schopnostmi našeho jazyka, přinejmenším v oblasti tak bezprostřední a praktické, jakou je sčítání a násobení přirozených čísel.

Rigorózní důkazy Goedelových vět jsou rozsáhlé a technicky náročné. Zajímavá snad ale může být krátká, neformální verze důkazu první Goedelovy věty, která by mohla být srozumitelná především programátorsky zaměřeným čtenářům:

Předpoklad (základní víra matematika): V matematice nemůžeme formálně dokázat něco, co není pravda.

Zdůvodnění předpokladu: Axiomy formálního systému volíme vždy tak, aby byly evidentně pravdivé. Logická odvozovací pravidla, která při dokazování používáme, očividně odvozují z pravdy vždy jen zase pravdu. Proto jsou všechna dokázaná tvrzení pravdivá.

Očíslování programů: Můžeme si představit, že programujeme v nějakém konkrétním jazyce, např. v jazyce C. Všechny možné programy můžeme pomyslně seřadit (např. podle abecedy), takže každý program má své jednoznačné pořadové číslo.

Očíslování tvrzení: Podobně jako programy, seřadíme a očíslujeme také všechna možná (pravdivá i nepravdivá) tvrzení o konkrétních přirozených číslech, jako např. „Číslo 17 je sudé“, „Existuje prvočíslo větší než 10^1 000”, nebo třeba “291. program někdy vytiskne číslo 13“.

Speciální program: Vytvoříme program P, který pomocí axiomů a odvozovacích pravidel daného formálního systému systematicky sestavuje různé formální důkazy tak, že na každý možný důkaz jednou dojde. Navíc dělá to, že kdykoliv narazí na důkaz tvrzení o nějakém konkrétním čísle n, které říká, že „n-tý program nikdy nevytiskne číslo n“, program P toto číslo n vytiskne.

Řekněme, že program P je podle našeho číslování p-tý v pořadí.

Fakt: Program P nikdy nevytiskne číslo p.

Zdůvodnění faktu: Aby program P vytiskl číslo p, musel by narazit na důkaz tvrzení „p-tý program nikdy nevytiskne číslo p“. Přitom toto tvrzení by bylo nepravdivé. Existoval by tedy důkaz tvrzení, které je nepravdivé, což podle Předpokladu není možné.

Nerozhodnutelné tvrzení: Tvrzení o čísle p, že „p-tý program nikdy nevytiskne číslo p“ je formálně nerozhodnutelné.

Zdůvodnění nerozhodnutelnosti tvrzení:

1. Tvrzení „p-tý program nikdy nevytiskne číslo p“ nelze dokázat, protože kdyby jeho důkaz existoval, program P by ho dříve nebo později našel a vytiskl by číslo p, což by bylo v rozporu s Faktem.

2. Jeho negace, tedy tvrzení „p-tý program někdy vytiskne číslo p“, je podle Faktu nepravdivá, a proto ji v souladu s Předpokladem rovněž nelze dokázat.

autor Otto Huřťák