UNIVERZITA KARLOVA V PRAZE FILOZOFICKÁ FAKULTA, KATEDRA LOGIKY
DIPLOMOVÁ PRÁCE
2005
Jaroslav Zouhar
UNIVERZITA KARLOVA V PRAZE FILOZOFICKÁ FAKULTA, KATEDRA LOGIKY Obor logika
Interpretace Gödelovy věty o neúplnosti
Vypracoval: Vedoucí diplomové práce: Rok odevzdání:
Jaroslav Zouhar Prof. RNDr. Jaroslav Peregrin, CSc. 2005
Prohlašuji, že jsem tuto práci vypracoval samostatně v tom smyslu, že se mi od nikoho nedostalo větší pomoci než od pana prof. Peregrina, a využil jsem výhradně citované literatury.
V Praze, 31.7.2005
Jaroslav Zouhar
Zásady pro vypracování: Gödel dokázal, že ke každé dané axiomatizaci aritmetiky bude existovat výrok, který nebude ani dokazatelný, ani vyvratitelný. Bude totiž vždy existovat výrok, říkejme mu G, který v přesně definovaném smyslu říká sám o sobě, že je nedokazatelný – a z toho vyplývá, že jak dokazatelnost, tak vyvratitelnost G by vedla ke sporu. Avšak jestliže G říká, že G není dokazatelný a G skutečně dokazatelný není, pak je to, co G říká, pravda – G je tedy pravdivý. Z toho se zdá vyplývat, že Gödel dokázal, že nikdy nelze dokázat všechny pravdivé výroky. Jak však víme, že G je pravdivý? Jistě ne v důsledku nějaké neexplikovatelné intuice, ale díky tomu, že nám to Gödel ukázal. G tedy v jistém smyslu dokazatelný je – Gödelův důkaz je totiž mimo jiné jasnou demonstrací, a v tomto smyslu důkazem, pravdivosti G. Cílem práce by nyní mělo být prozkoumání toho, jak by bylo možné tento ‘důkaz’ formalizovat a zjistit, v čem je podstatný rozdíl mezi Gödelovým ukázáním pravdivosti G a důkazem v tom smyslu, ve kterém je G nedokazatelný.
O OBBSSAAH H OBSAH .................................................................................................................................... 5 ÚVOD ...................................................................................................................................... 7 KAPITOLA 1: GÖDELOVA VĚTA ................................................................................................ 9 O ČEM MLUVÍ ............................................................................................................................................... 9 PŘEDBĚŽNÁ POZOROVÁNÍ ...................................................................................................................... 14 MIMO-MATEMATICKÝ DOSAH VĚTY ....................................................................................................... 15 HLAVNÍ MYŠLENKA .................................................................................................................................. 15 NELZE NA GÖDELOVU VĚTU VYZRÁT? ................................................................................................. 17 CO FORMÁLNÍMU SYSTÉMU CHYBÍ? ........................................................................................................ 18 KAPITOLA 2: DŮKAZ GÖDELOVY VĚTY .................................................................................. 19 ARITMETIZACE JAZYKA ARITMETIKY..................................................................................................... 19 ZACHYCENÍ DOKAZATELNOSTI UVNITŘ TEORIE ARITMETIKY .......................................................... 20 SESTROJENÍ AUTOREFERENČNÍ FOMULE............................................................................................... 24 KAPITOLA 3: FORMALIZACE DŮKAZU .................................................................................... 27 O ČEM SE V DŮKAZE MLUVÍ .................................................................................................................... 27 ELEMENTÁRNÍ KROKY V DŮKAZU ......................................................................................................... 27 PRVNÍ POKUS O FORMALIZACI ................................................................................................................ 28 FORMALIZACE PODRUHÉ ......................................................................................................................... 43 KAPITOLA 4: INTERPRETOVÁNÍ GÖDELOVY VĚTY ................................................................ 49 MYSL JAKO FORMÁLNÍ SYSTÉM (BOBŮV PŘÍPAD) ................................................................................. 49 SEBEREFLEXE: CELEK V SOBĚ SAMÉM ................................................................................................... 52 (PO)ZNÁME PŘIROZENÁ ČÍSLA? .............................................................................................................. 54 SHRNUTÍ ..................................................................................................................................................... 55 POUŽITÁ LITERATURA .......................................................................................................... 56
..... „There really is one?“ breathed Phouchg. „There really is one,“ confirmed Deep Thought. „To Everything? To the great Question of Life, the Universe and Everything?“ „Yes.“ Both of the men had been trained for this moment, their lives had been a preparation for it, they had been selected at birth as those who would witness the answer, but even so they found themselves gasping and squirming like excited children. „And you’re ready to give it to us?“ urged Loonquawl. „I am.“ „Now?“ „Now,“ said Deep Thought. They both licked their dry lips. „Though I don’t think,“ added Deep Thought, „that you’re going to like it.“ „Doesn’t matter!“ said Phouchg. „We must know it! Now!“ „Now?“ inquired Deep Thought. „Yes! Now...“ „All right,“ said the computer, and settled into silence again. The two men fidgeted. The tension was unbearable. „You’re really not going o like it,“ observed Deep Thought. „Tell us!“ „All right,“ said Deep Thought. „The Answer to the Great Question...“ „Yes...!“ „Of Life, the Universe and Everything...“ said Deep Thought. „Yes...!“ „Is...“ said Deep Thought, and paused. „Yes...!“ „Is...“ „Yes...!...?“ „Forty-two,“ said Deep Thought, with infinite majesty and calm. - Douglas Adams, The Hitchhiker’s Guide to the Galaxy
Úvod
Ú ÚVVO OD D Snažíme-li se dokázat matematické tvrzení, bývá nějtěžší uvědomit si, proč je pravdivé. Dát tomuto zdůvodnění správnou logickou formu – provést důkaz – už bývá to jednodušší. Základní důkazové prostředky používané v matematice se totiž zdají být v podstatě prosté. Vypadá to, že každý matematický důkaz jde složit z jednoduchých elementárních kroků, jejichž správnost lze snadno ověřovat. Nabízí se myšlenka, že bychom k matematickému dokazování našli několik jeho jasných výchozích principů, takže by správnost podrobně popsaných matematických důkazů šlo ověřovat automaticky. Výsledkem snahy teoreticky vymezit pojem důkazu jsou tzv. kalkuly – nástroje k vytváření matematických důkazů. Účelem kalkulu je, umožnit vytvářet jen zápisy vyjadřující korektní matematické důkazy. Těmto zápisům se říká formální důkazy. K formalizaci matematické teorie je potřeba vtisknout veškerým tvrzením v ní využívaným nějakou jednotnou formu. Pro to se osvědčil jazyk predikátové logiky. Formální dokazování je pak postup od některých takto formalizovaných tvrzení – formulí – k jiným podle dokazovacích pravidel kalkulu. Tvrzení, která se v dané teorii považují za pravdivá bez potřeby dalšího zdůvodnění, jsou vyjádřena axiomy. Množina axiomů pak tvoří formální teorii, z níž se v kalkulu dokazují teorémy dané teorie. Ve čtvrtině dvacátého století se zdálo všechno nasvědčovat tomu, že pro každé odvětví matematického myšlení půjde najít adekvátní množinu axiomů a ke každé matematické větě pak dodat odpovídající formální důkaz v příslušné formální teorii. Potom se v časopise Monatshefte für Mathematik und Physik objevil Gödelův článek. V roce 1930 německý logik a brněnský rodák Kurt Gödel ve slavném článku Über formal unentscheidbare Sätze der Principia Mathematica und verwandte Systeme (O formálně nerozhodnutelných větách Principia Mathematica a příbuzných systémů) ukázal, že ke každé použitelné axiomatické teorii obsahující některá evidentně pravdivá tvrzení o přirozených číslech dokážeme najít takový pravdivý výrok, že ani on ani jeho negace nebudou z této teorie v adekvátním kalkulu predikátové logiky dokazatelné. Tento výsledek je známý jako Gödelova věta o neaxiomatizovatelnosti aritmetiky či jako první Gödelova věta o neúplnosti (neúplnosti proto, že žádná použitelná axiomatizace aritmetiky nestačí k dokázání všech pravdivých výroků o přirozených číslech). Dále jí budu říkat jen Gödelova věta, protože s jinými jeho větami tu nebudeme mít co do činění. Jestliže nás ale Gödel dokázal přesvědčit o pravdivosti výroku, který není formálně dokazatelný (a o jeho pravdivosti není zvykem pochybovat), nějak ho přece dokázal. Zdá se proto, že musel využít buď nějakých důkazových prostředků, které kalkul není s to postihnout, nebo jakési znalosti o přirozených číslech, která není v axiomatice zachycena – a protože nedokazatelný pravdivý výrok lze najít ke každé použitelné axiomatice, lze říci, že ani axiomaticky zachytitelná. Přestože z tohoto hlediska působí Gödelův důkaz poněkud tajemně, když ho čtete, nic tajemného na něm není – jednotlivé kroky jsou stejně zřejmé jako v kterémkoli jiném matematickém důkaze. Podivíte se až tehdy, když si zjistíte, co se vlastně dokázalo. Gödelova věta má tendenci svádět různé myslitele k různým filosofickým interpretacím. Někteří si myslí, že dává definitivní odpověď na významné otázky týkající se schopností lidské mysli. Mezi vyvozovanými závěry jsou: ◦ Žádný formální systém není s to zachytit naše usuzování. ◦ Lidské myšlení přesahuje schopnosti jakéhokoli stroje. ◦ Nemůžeme poznat, jak funguje naše mysl.
7
Úvod
To mi připadá jako malé kouzlo – od tvrzení o kalkulu, axiomatických teoriích a odvozování formulí predikátové logiky se dospíváme k závěrům o povaze lidského myšlení a hranici schopností počítačů. Výchozí tvrzení lze navíc matematicky rigorózně dokázat na přibližně dvaceti stránkách za využití pouze základních znalostí o přirozených číslech! Pokusím se nejdřív vyjasnit, jak spolu tyto věci souvisejí, co přesněji Gödelova věta říká a v čem spočívá její schopnost vypovídat o věcech, které na první pohled zdaleka přesahují její rajón. Pak zkusím zjistit, v čem se důkaz Gödelovy věty tak podstatně liší od formálního důkazu v kalkulu predikátové logiky, že jej nelze v tomto kalkulu formalizovat, a to tím, že se o jeho formalizaci pokusím.
8
Gödelova věta
K KAAPPIITTO OLLA A 11::
G GÖ ÖD DE ELLO OV VA AV VĚ ĚT TA A
Originál Gödelovy věty hovoří o -konzistentních rozšířeních určité části systému v Principia Mathematica Bertranda Russella a Alfreda Northa Whiteheada. Místo něj ale uvedu trošku jednodušší větu, v níž je to, co je z Gödelova výsledku pro tuto práci klíčové, obsaženo a kterou jde dokázat přepsáním Gödelova originálního důkazu do moderního žargonu: Ke každé rekurzívní množině aritmetických formulí, která je formálně bezesporná a z níž jsou formálně dokazatelné všechny axiomy Peanovy aritmetiky, existuje pravdivá aritmetická formule, která není z této množiny axiomů formálně dokazatelná. Gödelův důkaz je navíc konstruktivní: obsahuje návod, jak ke každé teorii (splňující předpoklady věty) tuto formuli sestrojit. Formální dokazatelností se tu myslí dokazatelnost v nějakém adekvátním kalkulu predikátové logiky 1. řádu. Později uvedu trochu obecnější formu Gödelovy věty, hovořící o formálních systémech, které mohou disponovat i jinými důkazovými prostředky.
O ČEM MLUVÍ Nejdřív se pokusím přiblížit, co přesněji věta říká, objasněním klíčových pojmů v ní použitých. Mluví se tu o formálně dokazatelných formulích, o Peanově aritmetice a o rekurzívních teoriích (množinách axiomů), které jsou formálně bezesporné.
Formule predikátové logiky 1. řádu Formule jsou konečné posloupnosti symbolů. V případě formulí klasické predikátové logiky prvního řádu, o které se v Gödelově větě jedná, mohou těmito symboly být: 1. logické spojky: , , →. 2. kvantifikátor: . 3. proměnné: x, y, z ... 4. interpunkční znaménka: (, ). 5. jmenné konstanty, např. 0. 6. funkční symboly, např. +, ∙, S. 7. predikátové symboly, např. =, >, ≥. Symboly v prvních dvou bodech a symbol rovnosti (,=’) jsou tzv. logické konstanty, ostatní symboly v posledních třech bodech jsou tzv. mimologické konstanty. Formule v jazyce nějaké teorie jsou takové, v nichž se vyskytují jen ty mimologické symboly, které se vyskytují v některém z axiomů dané teorie. Formule v jazyce aritmetiky, kterým budu říkat aritmetické formule, jsou takové, které neobsahují jiné mimologické symboly než 0, S, +, ∙, >, ≥. Někdy budu formule zapisovat ve zkrácené podobě tak, že využiji nových symbolů jako zkratek. Například formuli ,(x=y)’ budu zapisovat ,x≠y’, formuli tvaru ,(φ ψ)’ budu zapisovat ,φ ψ’, formuli tvaru ,x(φ)’ budu zapisovat ,x φ’ apod. Závorky budu často vynechávat pro lepší srozumitelnost zápisu. Název čísla n se v aritmetické formuli zapíše ,S(S(...S(0)...))’, přičemž symbol S se tu vyskytuje nkrát. Zkráceně jej budu zapisovat n.
9
Gödelova věta
Formule v jazyce aritmetiky Vypovídáme-li něco o přirozených číslech, činíme tak větami nějakého jazyka. Přitom to, kolik toho o přirozených číslech umíme říct, je omezeno bohatostí použitého jazyka. Podle všeho je docela dobře možné, že některé zajímavé věci o číslech zatím neumíme vyjádřit kvůli omezením našeho jazyka. Například před vynalezením teorie množin, zavádějící pojem spočetných množin, nebylo možné říct, že přirozených čísel je jen spočetně mnoho. Uzavřené formule v jazyce aritmetiky vyjadřují tvrzení o přirozených číslech. Například formule ,x(x>1)‘ vyjadřuje tvrzení, že existuje číslo větší než jedna. Jsou tvrzení, která aritmetickými formulemi vyjádřit nejde, třeba, že ke každému číslu existuje jen konečný počet menších. Z toho pohledu se může zdát jazyk aritmetiky dost chudý. Mohli bychom proto nabýt přesvědčení, že formální nedokazatelnost pravdivého výroku, jehož existenci tvrdí Gödelova věta, je dána prostě omezeností jazyka teorií, o nichž se mluví – že k tomu, abychom mohli toto tvrzení dokázat, musíme mluvit o něčem, o čem formule v jazyce daných teorií mluvit nemohou. Ukazuje se ale – jak popíšu dále – že Gödelovu větu lze zcela obdobně dokázat i pro teorie s mnohem bohatším jazykem: že i k teoriím s obohaceným jazykem bude existovat už formule v chudičkém jazyce aritmetiky, která, ač pravdivá, z ní bude formálně nedokazatelná, bude-li teorie splňovat určité předpoklady. Tím, že se omezíme na formule jazyka aritmetiky, se proto dosah dosažených výsledků nijak nesníží. Dá se říct, že na formule se díváme dvojím způsobem: jednak z hlediska toho, jak jsou utvořeny (kterou posloupností symbolů jsou), a jednak z hlediska toho, co říkají – jaká tvrzení vyjadřují. Díky tomu můžeme o formulích mluvit zároveň jako o formálně dokazatelných (jakožto posloupnostech symbolů) i jako o pravdivých – vyjadřujících pravdivé tvrzení.
Symbolický zápis matematických tvrzení Matematikové mají ve zvyku zapisovat tvrzení symbolicky kvůli srozumitelnosti. Aby se takto vyjádřená tvrzení nepletla s formulemi (posloupnostmi symbolů), budu je psát kurzívou. Například tvrzení, že existuje číslo větší než jedna, vyjádřené formulí ,x(x>1)’, zapíšu symbolicky ,x(x>1)’, nebo třeba ,Existuje x takové, že x>1.’.
Formální dokazatelnost Formální dokazatelností formule se myslí její dokazatelnost v určitém kalkulu. Přitom některé kalkuly jsou považovány za standardní kalkuly predikátové logiky 1. řádu a umožňují dokázat tytéž formule. Když se mluví o formální dokazatelnosti bez dalšího upřesnění, myslí se tím dokazatelnost v některém (libovolném) ze standardních kalkulů. Dokazování formulí v kalkulu má odpovídat neformálnímu, avšak matematicky rigoróznímu dokazování jim odpovídajících tvrzení. Například neformálnímu důkazu tvrzení, že existuje číslo větší než jedna, by měl odpovídat důkaz formule ,x(x>1)’. Od dobrého kalkulu by se dalo očekávat, že formule v něm dokazatelné budou odpovídat právě všem neformálně, avšak matematicky rigorózně dokazatelným tvrzením (tedy alespoň z těch, které je jazyk formulí schopen vyjádřit), jestliže dále nezdůvodňovaným tvrzením neformálního důkazu bude odpovídat množina formulí, z níž se v kalkulu dokazuje.
Odvození a formální důkaz Dokazování formulí v kalkulu se provádí odvozováním formulí, případně nějakých sekventů, v souladu s odvozovacími pravidly kalkulu. Formálním důkazem formule se ale nemyslí jen provedení tohoto odvození, nýbrž i vyjádření postupu odvození v nějakém předepsaném tvaru (je to podobné, jako když se neformální důkaz matematického tvrzení popíše slovy v knize). U
10
Gödelova věta
Gödela je formální důkaz posloupnost formulí, z nichž každou lze získat použitím některého pravidla kalkulu z formulí jí v posloupnosti předcházejících, není-li sama axiom. Poslední formule posloupnosti je pak dokázaná formule. Důležité je, že o každém zápisu v předepsaném tvaru (např. o každé posloupnosti formulí) se dá rozhodnout, zda se jedná o důkaz té které formule, pouhým ověřením, zda splňuje nějaké formální podmínky. Vzhledem k tomu, že formule, jejichž formální dokazatelností se budeme zabývat, vyjadřují tvrzení o číslech, budu někdy místo o formální dokazatelnosti formulí mluvit o formální dokazatelnosti tvrzení, čímž budu myslet formální dokazatelnost formule, která je vyjadřuje. Přitom by mohl nastat jeden problém: některá tvrzení je totiž možné vyjádřit různými formulemi, např. tvrzení ,Existuje číslo větší než 1.’ lze vyjádřit jednak formulí ,x(x>1)’ a jednak formulí ,y(y>1)’. Co kdyby jedna byla dokazatelná a druhá ne? Bylo by pak třeba říct, formální dokazatelnost které formule se má na mysli, když se mluví o formální dokazatelnosti tohoto tvrzení. Naštěstí se ukazuje, že u standardních kalkulů se formální dokazatelnost formulí, o nichž jsme připraveni prohlásit, že vyjadřují totéž tvrzení, shoduje, takže to potřeba není.
Adekvátnost kalkulu To, že formule v jazyce predikátové logiky 1. řádu je logickým důsledkem jiných, lze přesněji formulovat alespoň dvěma způsoby: ◦ popsat logický důsledek s pomocí formální dokazatelnosti (čili odvoditelnosti v kalkulu), ◦ popsat logický důsledek jako sémantické vyplývání. Sémantické vyplývání se definuje s pomocí pojmu splnění formule nějakou interpretací. Interpretace je v podstatě určité formální vyjádření toho, co jména, funktory, predikáty a proměnné ve formulích označují. Formule je pak splněná nějakou interpretací, jestliže je při příslušném udělení významu symbolům v ní obsaženým pravdivá. Formule vyplývá z množiny formulí, jestliže je splněná každou interpretací, jíž jsou splněné všechny formule z dané množiny. Formule je logická tautologie, jestliže je splněna každou interpretací, neboli, jestliže vyplývá z prázdné množiny formulí. Na interpretaci je dobré to, že jasně popisuje množinu objektů, o nichž formule mluví. V přirozené interpretaci aritmetických formulí je to množina všech přirozených čísel. Za standardní kalkul predikátové logiky je považován takový, který je adekvátní vůči její sémantice. To znamená, že formule vyplývá z nějaké množiny formulí právě tehdy, když je z této množiny v daném kalkulu dokazatelná. Z Gödelovy věty pak plyne, že ke každé rekurzívní množině aritmetických formulí existuje i jejich nestandardní interpretace, která splňuje všechny formule z této množiny, za předpokladu, že je vůbec nějakou interpretací splnit lze.
Peanova aritmetika Jazyk Peanovy aritmetiky obsahuje jednu jmennou konstantu 0, jeden jednoargumentový funktor S, dva dvouargumentové funktory + a ∙ a dva dvoumístné relační symboly > a ≥, tedy tytéž mimologické symboly, jaké mohou obsahovat aritmetické formule. Peanovu aritmetiku tvoří osm axiomů a jedno schéma (dodávající nekonečnou množinu axiomů):
11
Gödelova věta
PA1:
x (S(x) ≠ 0)
PA2:
x y (S(x) = S(y) → x = y)
PA3:
x (x+0 = x)
PA4:
x y (x+S(y) = S(x+y))
PA5:
x (x∙0 = 0)
PA6:
x y (x∙S(y) = (x∙y)+x)
PA7:
x y (x ≥ y ↔ z (x+z = y))
PA8:
x y (x > y ↔ z (x+S(z) = y))
Schéma indukce:
(φ(x › 0) (φ → φ(x › S(x))) → x φ pro každou formuli φ(x)1
Axiomy PA1 až PA8 popisují vlastnosti přirozených čísel, o nichž snad nepochybuje nikdo, kdo umí počítat s přirozenými čísly. Jak je to ale s axiomy indukce (tj. axiomy, které vzniknou ze schématu indukce dosazením konkrétních formulí za φ(0), φ(x) a φ(S(x)) – mají rozumné opodstatnění? Přirozená čísla jsou taková, k nimž lze dospět přičítáním jedničky, začneme-li od nuly. Jestliže má tedy nula nějakou vlastnost (zde vyjádřenou formulí φ) a s každým číslem, které ji má, ji má i číslo o 1 větší, nemůžeme přičítáním jedničky dospět k číslu, které by ji nemělo, a tedy ji mají všechna čísla.2 Má se tedy za to, že axiomy Peanovy aritmetiky vyjadřují jen tvrzení pravdivá o přirozených číslech. Proto se požadavek, aby z teorie, která má axiomatizovat aritmetiku, byly tyto axiomy dokazatelné, nepovažuje za nijak omezující. Jestliže jsou z jedné z teorie formálně dokazatelné všechny axiomy druhé teorie, jsou z ní formálně dokazatelné všechny formule, které jsou formálně dokazatelné z druhé. Říká se pak, že první teorie je alespoň tak silná jako druhá. Teorie, o nichž hovoří Gödelova věta, jsou tedy alespoň tak silné jako Peanova aritmetika, a cokoli je formálně dokazatelné v Peanově aritmetice, je formálně dokazatelné v každé z těchto teorií.
Rekurzívnost teorie Požadavek, aby teorie (tedy množina axiomů) byla rekurzívní, staví na pojmu rekurzívní funkce. Co je rekurzívní funkce a rekurzívní množina, popíšu podrobněji dále. Podstatné je, že pojem rekurzívní množiny má vystihnout intuitivní představu algoritmu: množina objektů nějakého druhu má být rekurzívní tehdy, když existuje algoritmus, pomocí něhož lze o jakémkoli objektu daného druhu rozhodnout, zda je nebo není jejím prvkem, v nějakém konečném (ačkoli třeba předem neznámo jakém) čase. Přijmeme-li tento (mezi matematiky obecně přijímaný) názor, můžeme říct, že požadavek, aby teorie byla rekurzívní, znamená, aby bylo možné v konečném čase zjistit, zda něco je či není její axiom. Takový požadavek se možná zdá být u axiomatické teorie zcela samozřejmý, ale není zanedbatelný: Předpokládejme, že z množiny pravdivých formulí nelze formálně dokázat nepravdivý výrok (což by pro dokazování ve standardním kalkulu mělo platit). Pak množina všech formulí, které vyjadřují pravdivá tvrzení o přirozených číslech, je teorie, z níž jsou dokazatelné právě všechny Myslí se formule v jazyce Peanovy aritmetiky. Zápis ,φ(x)’ značí, že formule φ má volnou proměnnou x, ,φ(x › 0)’ označuje formuli, která vznikne z φ dosazením konstanty 0 za proměnnou x tam, kde x není vázaná kvantifikátorem, a ,φ(x › S(x))’ označuje formuli, která vznikne z φ dosazením termu S(x) za proměnnou x tam, kde x není vázaná kvantifikátorem. Jestliže φ je formule s jedinou volnou proměnnou, budu zápis tvaru ,φ(x › t)’ pro libovolný term t zkracovat na ,φ(t)’. 2 Ovšem ne všechny vlastnosti přirozených čísel lze vyjádřit formulí v jazyce aritmetiky (např. „být takovým číslem, že jen konečně mnoho je menších“). 1
12
Gödelova věta
pravdivé výroky o přirozených číslech (z množiny formulí je totiž dokazatelná každá z těchto formulí). Potíž je v tom, že tato teorie nemusí být (a Gödelova věta prokáže, že není) rekurzívní.3
Bezespornost Bezesporná teorie je taková, že pro žádnou formuli φ neplatí, že by v ní byla dokazatelná jak φ, tak i formule tvaru ,φ’. Ze sporné teorie jde formálně dokázat spor, tedy formuli tvaru ,φ φ’, a dokonce úplně každou formuli. Díky tomu můžeme bezespornou teorii charakterizovat také tím, že v ní není formálně dokazatelná např. formule ,0≠0’ (formule ,0=0’ je totiž formálně dokazatelná v každé teorii). Mohli bychom se ptát, zda už požadavek, aby kalkul neumožňoval odvodit spor bez jakýchkoli předpokladů, jej nečiní podstatně odlišným od lidského usuzování – zdá se totiž, jako by naše usuzování někdy (bez jakýchkoli chybných předpokladů) vedlo ke sporu. Případy, kdy logicky (alespoň na první pohled) korektní úvaha vede ke sporu, jsou známy jako paradoxy. Například, označme následující větu A: Věta A je nepravdivá. Pak věta A je pravdivá právě tehdy, když věta A – tedy ona sama – je nepravdivá. Za předpokladu, že je pravdivá, je zároveň nepravdivá, a za předpokladu, že je nepravdivá, je současně pravdivá – v každém případě je tedy zároveň pravdivá i nepravdivá (takový úsudek možná neodpovídá tomu, jak běžně přemýšlíme – větu A bychom možná neoznačili ani za pravdivou, ani za nepravdivou – ale svou logickou formou se neliší od úsudků, které se provádějí v matematice, a jimž odpovídající odvození lze provést v kalkulu). Matematik sice takto umí dokázat sporné tvrzení, ale nevyvozuje z toho například, že jedna se nerovná jedna (čemuž odpovídající odvození lze v kalkulu provést), protože to, zda je nějaká podivná o sobě vypovídající věta pravdivá, nemá co dělat s aritmetikou přirozených čísel. Na druhou stranu, můžeme najít paradoxy, které se přirozených čísel týkají: Princip indukce, vyjádřený v Peanově aritmetice schématem indukce, říká, že má-li nula určitou vlastnost a s každým číslem, které má tuto vlastnost, má onu vlastnost i číslo o 1 větší, pak tuto vlastnost mají všechna čísla, symbolicky: pro každou vlastnost V, [V(0) x(V(x) → V(x+1))] → yV(y). Nazvěme vlastnost čísel nahoru přenosnou, jestliže s každým číslem, které ji má, ji má i každé číslo větší, symbolicky: vlastnost V je nahoru přenosná, jestliže x y [(V(x) y≥x) → V(y)] Dá se dokázat, že princip indukce je ekvivalentní tvrzení, že ke každé nahoru přenosné vlastnosti existuje nejmenší číslo, které ji má – symbolicky: pro každou vlastnost V: xy[(V(x) y≥x) → V(y)] → z[V(z) w(z≥w → V(w))], za (slaboučkého) předpokladu, že ke každé vlastnosti čísel existuje vlastnost k ní opačná, tj. taková, kterou mají právě ta čísla, jež nemají tu první. Označme P vlastnost, kterou má číslo tehdy, když je větší nebo rovné nějakému číslu, které nelze definovat méně než deseti slovy. Pak vlastnost P je nahoru přenosná: jestliže nějaké číslo n je větší nebo rovné nějakému číslu nedefinovatelnému méně než deseti slovy, platí to i pro číslo větší. Za předpokladu, že platí princip indukce, tedy existuje nejmenší číslo, které má vlastnost P, označme jej č. Číslo č musí být zároveň nejmenším číslem, které nelze definovat méně než deseti
3
Někteří by ale měli námitky už proti způsobu definování takové množiny axiomů.
13
Gödelova věta
slovy – kdyby totiž ne, bylo by tu nějaké menší, které má vlastnost P. Pak ale můžeme číslo č definovat: nejmenší číslo, které nelze definovat méně než deseti slovy, což je méně než deseti slovy. Pak ale není možné, aby č mělo vlastnost P: aby ji mělo, muselo by tu být číslo menší než č, které nelze definovat méně než deseti slovy, ale ukázali jsme, že žádné takové není. Celkově jsme tedy dokázali, že číslo č vlastnost P zároveň má i nemá, symbolicky: P(č) P(č). Takže z principu indukce, vztahujeme-li jej i na takové vlastnosti jako P, lze dokázat spor. Přesto se princip indukce v matematické praxi běžně používá – je na něm založen důkaz indukcí. Jak je to možné? Vlastnosti jako „nebýt definovatelné méně než deseti slovy“ se prostě při matematickém usuzování neberou v úvahu: říkají něco o našem jazyce, nikoli o přirozených číslech samotných: z toho, že náš jazyk umožňuje vytvořit paradoxní tvrzení (jako větu „Já jsem nepravdivá“) či paradoxní číselné vlastnosti (jako „být číslem nedefinovatelným méně než deseti slovy“), se nesoudí, že by sama přirozená čísla byla něčím paradoxním. Dokud formule v kalkulu dokazované mluví jen o číslech (přesněji řečeno, v oboru jejích proměnných jsou jen objekty, které můžeme sčítat, násobit apod.), zdá se, že nebezpečí dospět k paradoxu podobnému těm předchozím nehrozí. Kdybychom ale chtěli použít standardní kalkul na formule, které by měly vyjadřovat třeba tvrzení o sobě samých (například „tvrdit“ svoji nepravdivost), mohli bychom očekávat, že se tu paradox objeví a kalkul tedy umožní dokázat kontradikce. Potom by ale umožnil dokázat i tvrzení, která bychom za (neformálně) dokazatelná nemuseli považovat, umožnil by totiž dokázat všechna.
Shrnutí Gödelova věta říká, že ke každé „algoritmicky rozpoznatelné“ množině formulí, z níž jsou formálně dokazatelné některé pravdivé aritmetické formule, existuje pravdivá aritmetická formule, která není z této množiny formálně dokazatelná, za předpokladu, že není z dané množiny formálně dokazatelná zcela libovolná formule. Jestliže formální dokazatelnost z množiny formulí je s to vystihnout neformální dokazování z množiny předpokladů (tedy že z pravdivých tvrzení o přirozených číslech dokážeme neformálně dokázat právě to, co je formálně dokazatelné z příslušné množiny formulí), dá se říct, že každá použitelná množina axiomů je příliš malá.
PŘEDBĚŽNÁ POZOROVÁNÍ Gödelova věta říká, že ke každé axiomatické teorii splňující určité předpoklady, jejichž splnění bychom od teorie aritmetiky přirozených čísel jistě očekávali, existuje pravdivý výrok, který v ní není formálně dokazatelný. Vypadá to tedy, že se říká, že z každé axiomatické teorie aritmetiky je toho dokazatelného příliš málo. Dá se na to ale dívat i obráceně, Gödelovu větu lze totiž přeformulovat: Ke každé rekurzívní množině aritmetických formulí, z níž jsou formálně dokazatelné všechny axiomy Peanovy aritmetiky, existuje pravdivá aritmetická formule, o které platí: jestliže je z dané množiny axiomů formálně dokazatelná tato formule, je z ní formálně dokazatelná i formule ,0≠0’. Teď ji naopak můžeme číst tak, že z každé dostatečně silné axiomatické teorie aritmetiky (totiž takové, z níž jsou dokazatelné Peanovy axiomy a jistá pravdivá formule) už je dokazatelného příliš mnoho, totiž i to, že nula se nerovná nule. Gödelova věta bývá nazývána větou o neaxiomatizovatelnosti aritmetiky přirozených čísel. Přitom se ale zdá, že podoba axiomů i dokazatelnost, o níž mluví, je jen specifického druhu – jedná se tu o formule predikátové logiky 1. řádu a k ní adekvátní kalkul. Lze si představit, že by 14
Gödelova věta
aritmetika přirozených čísel byla axiomatizovatelná množinou axiomů s lepšími vyjadřovacími schopnostmi (třeba schopnými říct, že ke každému číslu existuje jen konečně mnoho menších) nebo s jiným, rafinovanějším kalkulem. Podrobnější popis Gödelova důkazu ale ukáže, že to tak není – že už důkazové prostředky, které máme v Peanově aritmetice, umožňují rozšířit důkaz jisté pravdivé aritmetické formule na důkaz sporu i v mnohem bohatších systémech.
MIMO-MATEMATICKÝ DOSAH VĚTY Lidská mysl se zdá být něco tak složitého, že pustit se do jejího matematického popisu může působit jako přinejlepším velice odvážný počin. Gödel ale provedl nečekaný kousek: vzal jednu z jejích zdánlivě nejnepozoruhodnějších schopností, totiž schopnost usuzovat o přirozených číslech, a ukázal, že tato schopnost v něčem přesahuje schopnosti každé použitelné axiomatiky, kterou dokážeme najít. A ukázal to tak, že nám dal návod, jak k takovému systému najít výrok, jehož pravdivost tento systém není s to odhalit, a dokázal jeho pravdivost.4 Spojitost mezi Gödelovou větou a počítači se zdá být asi taková: pokud by libovolný počítač vypisoval jedině pravdivá tvrzení o přirozených číslech, existoval by formální systém, na nějž by se vztahoval Gödelův výsledek a v němž by byla dokazatelná všechna tvrzení, která počítač kdy vypíše. Pravdivé tvrzení, které není v tomto formálním systému dokazatelné, by pak počítač nemohl vypsat. Jestliže žádný formální systém, na nějž se vztahuje Gödelův výsledek, nedokáže všechno to co matematik, nedokáže to pak ani žádný počítač. Zdá se však, že proti takovému „převedení“ otázky schopností počítače na otázku dokazatelnosti ve formálním systému lze mít námitky. V této práci se vztahem mezi formálními systémy a počítači nebudu příliš zabývat: zaměřím se spíš na možnost postihnout naše usuzování s pomocí formálního systému.
HLAVNÍ MYŠLENKA Cílem Gödelova důkazu je sestrojení takové formule, která nemůže být v dostatečně silné bezesporné teorii dokazatelná. Myšlenkový postup k nalezení této formule lze rozdělit na tři části: aritmetizaci jazyka aritmetiky, zachycení formální dokazatelnosti uvnitř aritmetiky a sestrojení autoreferenčního výroku. Než se pustím do jejich popisu, předvedu úvahu, která by měla přiblížit stěžejní myšlenku Gödelova důkazu. Předpokládejme, že: ◦ výroky v jazyce nějaké teorie Θ dokážou mluvit o výrocích této teorie (tedy o sobě navzájem). ◦ jazyk teorie Θ je natolik bohatý, aby umožnil vytvořit výrok, který nazveme A: „Výrok A není v teorii Θ dokazatelný“. ◦ v teorii Θ není možné dokázat nepravdivé výroky. Pak výrok A nemůže být v teorii Θ dokazatelný: kdyby totiž byl dokazatelný, byl by nepravdivý, ale v teorii Θ podle předpokladu nelze dokázat nepravdivé výroky. V tom případě je ale výrok A pravdivý, a existuje tedy pravdivý výrok, který není v teorii Θ dokazatelný. Teorie, o jakých mluví Gödelova věta, nemusejí (alespoň při standardním způsobu čtení jejich výrazů) splňovat žádný z výše uvedených předpokladů. Ukáže se ale, že k nalezení formálně nedokazatelného pravdivého výroku stačí podstatně slabší předpoklady, které už ony teorie splňují. Přitom konstrukce takového výroku a ukázání jeho pravdivosti a nedokazatelnosti se v něčem dost podobají těm výroku A, jsou ale mnohem rafinovanější.
4
Zajímavé je, že důsledky Gödelovy věty tu neplynou z její formulace, ale z toho, že ji umíme dokázat.
15
Gödelova věta
Aritmetizace jazyka aritmetiky Formule predikátové logiky jsou posloupnosti symbolů. Vlastnosti formulí, například „být axiomem Peanovy aritmetiky“, jsou tedy vlastnosti posloupností symbolů, a vztahy mezi formulemi, např. kdy jedna je podformulí druhé nebo kdy jedna je dokazatelná z jiných v nějakém kalkulu, jsou pak vztahy mezi posloupnostmi symbolů. Gödel vymyslel, jak formule i posloupnosti formulí kódovat přirozenými čísly tak, aby každé přirozené číslo bylo kódem nejvýše jedné formule nebo posloupnosti formulí. Vlastnostem formulí a posloupností formulí pak odpovídají určité číselné vlastnosti, například vlastnosti „být axiomem Peanovy aritmetiky“ takto odpovídá vlastnost „být kódem axiomu Peanovy aritmetiky“, a vlastnosti „být v teorii Θ formálně dokazatelná“ číselná vlastnost „být kódem formule formálně dokazatelné v teorii Θ“. Podobně vztahům mezi formulemi či jejich posloupnostmi odpovídají vztahy mezi čísly. Gödelovo kódování je navíc zvoleno tak, že zajímavým vlastnostem formulí a důkazů či vztahům mezi nimi odpovídají číselné vlastnosti, které jde v jazyce aritmetiky snadno popsat.5 Číslům, které jsou kódy formulí, budu říkat Gödelova čísla formulí. Jazyk teorie aritmetiky nedokáže vyjádřit tvrzení přímo o svých formulích – jedinými termy (jmény), které obsahuje, jsou jména čísel. Ale díky tomu, že formulím lze přiřadit Gödelova čísla, můžeme ukázat, že tvrzení vyjádřená některými formulemi v jazyce aritmetiky jsou ekvivalentní jistým tvrzením o dokazatelnosti formulí. Kdyby se nám pak podařilo k teorii Θ vytvořit aritmetickou formuli, která by: ◦ vyjadřovala tvrzení ekvivalentní tomu, že číslo n je kód formule formálně nedokazatelné v teorii Θ ◦ sama měla kód n ◦ jestliže by byla v teorii Θ formálně dokazatelná, byla by pravdivá měli bychom formuli, která je pravdivá, ale není v teorii Θ dokazatelná. Kdyby totiž pravdivá nebyla, byla by v teorii Θ dokazatelná, ale to je vyloučeno, protože z její dokazatelnosti v teorii Θ plyne podle našeho předpokladu její pravdivost. V jazyce teorií, o nichž hovoří Gödelova věta, skutečně existují formule s Gödelovým číslem n, které vyjadřují tvrzení ekvivalentní: číslo n je kód formule, která není v této teorii formálně dokazatelná. Ovšem v těchto teoriích nemusejí být formálně dokazatelné jen pravdivé formule: některé teorie – jak se dále ukáže – jsou bezesporné, jsou v nich formálně dokazatelné všechny axiomy Peanovy aritmetiky, a přece i některé nepravdivé formule. Tyto formule pak nesplňují třetí z výše popsaných podmínek. Naštěstí se ukazuje, že formule určitého druhu jsou v dotyčných teoriích formálně dokazatelné právě tehdy, jsou-li pravdivé. Lze k tomu dospět s využitím pojmu rekurzívní relace.
Rekurzívní relace Ukazuje se, že některé číselné vlastnosti a vztahy jde v jazyce aritmetiky popsat tak, že je toho o nich v teoriích splňujících předpoklady Gödelovy věty dokazatelného dostatečně mnoho. Konkrétně, ke každé takové k-místné relaci R existuje formule φ(x1,..xk) taková, že pro všechna čísla n1, ...nk platí: Formule bychom mohli očíslovat třeba tak, že bychom je seřadili lexikograficky a každé pak přiřadili číslo podle jejího pořadí (kdybychom chtěli takto kódovat i posloupnosti formulí, mohli bychom formulím přiřadit jen lichá čísla a posloupnostem formulí pak podobným způsobem sudá). Pak bychom ale možná měli potíže popsat i vlastnosti čísel odpovídající dost jednoduchým vlastnostem formulí. Jak bychom třeba v jazyce aritmetiky popsali vlastnost „být kódem formule začínající kvantifikátorem“? 5
16
Gödelova věta
◦ formule φ(n1,...nk) je pravdivá právě tehdy, když R(n1,...nk), a ◦ formule φ(n1,...nk) je v příslušné teorii dokazatelná právě tehdy, když R(n1,...nk). Gödel ukázal, že taková formule existuje (v případě teorií, o nichž je řeč) ke každé tzv. rekurzívní relaci, a že relace „... je kód důkazu formule s kódem ... v té a té teorii“ je pro teorie splňující předpoklady věty rekurzívní. Proto existuje aritmetická formule φ(x,y) taková, že formule φ(m,n) je pravdivá i dokazatelná právě pro taková čísla m a n, že m je kód důkazu formule s kódem n v dané teorii. Formule ,x φ(n)’ je potom pravdivá právě tehdy, když neexistuje číslo, které by bylo kód důkazu formule s kódem n v dané teorii, neboli, když formule s kódem n není v dané teorii dokazatelná. Jestliže je formule ,x φ(n)’ v dané teorii dokazatelná, je tu pro jakékoli číslo m dokazatelná i formule φ(m,n). Kdyby pak formule ,x φ(n)’ nebyla pravdivá, byla by formule s kódem n dokazatelná, a tedy pro číslo m, které by bylo kódem jejího důkazu, by byla pravdivá formule φ(m,n). Pak by ale byla φ(m,n) v dané teorii i dokazatelná a tato teorie by byla sporná, což je v rozporu s předpoklady Gödelovy věty. Proto z dokazatelnosti formule ,x φ(n)’ plyne její pravdivost. K příslušné teorii máme tedy formuli (totiž ,x φ(n)’), která ◦ je pravdivá, jestliže číslo n je kód formule formálně nedokazatelné v této teorii ◦ pokud je v této teorii formálně dokazatelná, je pravdivá. Kdyby navíc platilo, že ◦ její kód je n, měli bychom formuli, která v naší teorii není formálně dokazatelná: kdyby v ní totiž byla formálně dokazatelná, byla by pravdivá, a číslo n by tedy bylo kódem formule, která v dané teorii není formálně dokazatelná, a proto by ona formule v dané teorii nejen byla, ale současně nebyla formálně dokazatelná. Otázka je, zda existuje formule, která současně s prvními dvěma splňuje i třetí podmínku.
Autoreferenční formule Gödel ukázal, jak k aritmetické formuli ψ(y) sestrojit takovou aritmetickou formuli γ s kódem n, že formule γ je pravdivá právě tehdy, když je pravdivá ψ(n), a v každé teorii splňující předpoklady Gödelovy věty je navíc dokazatelná ekvivalence ψ(n) ↔ γ. K výše popsané formuli ,x φ(y)’ se tedy dá sestrojit taková formule γ s kódem n, která je pravdivá právě tehdy, když je pravdivá formule ,x φ(n)’, tedy když formule s kódem n (tj. ona sama) není v příslušné teorii dokazatelná, a navíc z dokazatelnosti γ plyne dokazatelnost formule ,x φ(n)’, o níž víme, že je za předpokladu své dokazatelnosti i pravdivá, a tedy je pak pravdivá i γ. Formule γ tedy splňuje všechny výše popsané požadavky, a je proto pravdivá, aniž by byla v příslušné teorii dokazatelná.
NELZE NA GÖDELOVU VĚTU VYZRÁT? Důkaz Gödelovy věty ukazuje, jak k nějaké dostatečně silné rekurzivní teorii Θ sestrojit takovou formuli, že pokud je teorie Θ bezesporná, vyjadřuje tato formule pravdivé tvrzení a není v Θ dokazatelná. Takovou formuli budu značit γΘ a budu jí říkat Gödelova formule pro teorii Θ. Mohlo by nás napadnout, vyzrát na Gödelovu větu tak, že bychom přidali formuli γΘ k teorii Θ jako axiom, čímž by se stala v nové teorii dokazatelnou. Tím bychom ale situaci nezachránili, protože přidáním axiomu k dostatečně silné rekurzívní teorii vzniká opět dostatečně silná 17
Gödelova věta
rekurzívní teorie, ke které, je-li bezesporná, existuje podle Gödelovy věty zase jiný pravdivý a nedokazatelný výrok. Když to znázorníme symbolicky, přidáním formule γΘ k teorii Θ vznikne teorie Θ {γΘ}, k níž existuje nějaká jiná formule, γ(Θ {γΘ}), která v ní – za předpokladu bezespornosti – není dokazatelná a vyjadřuje pravdivé tvrzení. Jedna potíž je v tom, že formule, již přidáváme, není Gödelovou formulí pro nově vzniklou teorii Θ {γΘ}, ale pro tu původní, Θ. Mohli bychom tedy zkusit k teorii Θ najít takovou formuli φ, která by (náhodou) byla Gödelovou formulí pro teorii vzniklou jejím přidáním k Θ, symbolicky φ = γ(Θ {φ}), jinak řečeno, takovou formuli φ, že kdybychom k teorii Θ {φ}, která je taky rekurzívní, sestrojili Gödelovu formuli, dostali bychom formuli φ. Pak by ale formule φ byla v dané teorii dokazatelná – byla by přímo jedním z axiomů. Znamená to tedy, že k žádné teorii Θ, splňující předpoklady Gödelovy věty, taková formule neexistuje? Podle dosavadního zkoumání to tak být nemusí, znamená to ale, že teorie vzniklá přidáním této formule (zde teorie Θ {φ}) by byla sporná.
CO FORMÁLNÍMU SYSTÉMU CHYBÍ? Gödel ukázal, jak sestrojit takovou formuli, z jejíž dokazatelnosti z určité teorie plyne její spornost a z nedokazatelnosti z ní pravdivost, a o níž tedy víme, že není z bezesporné teorie dokazatelná a že je pravdivá. Můžeme se na to ale podívat z druhé stránky a ptát se, co nám „po technické stránce“ brání tuto formuli formálně dokázat. Vidím v podstatě tři možnosti: 1. Množina axiomů o přirozených číslech je příliš malá – obsahuje příliš málo axiomů na to, aby z nich byla dokazatelná všechna pravdivá tvrzení o přirozených číslech (z těch, která jsou v jazyce aritmetiky vyjádřitelná). Při důkazu pravdivosti tvrzení z nich nedokazatelného, které Gödel našel, bychom pak měli využít nějaké znalosti o číslech, kterou axiomy z nějakého důvodu nevyjadřují. 2. Kalkul neumožňuje provést odvození odpovídající neformálnímu důkazu daného tvrzení. V tom případě bychom se mohli ptát, ke kterým krokům neformálního důkazu se nedaří provést odpovídající formální odvození, případně proč by nešlo kalkul rozšířit tak, abychom odpovídající formální odvození provést mohli. 3. K důkazu výroku je potřeba využít i jiných pravdivých tvrzení než jsou tvrzení o přirozených číslech (a logické tautologie), ačkoli výrok mluví jen o přirozených číslech. Pak bychom se mohli ptát, o čem všem potřebujeme v důkazech tvrzení o přirozených číslech mluvit, případně proč by nešlo obohatit jazyk a množinu axiomů tak, abychom potřebná tvrzení dokázat mohli. Ke zjištění, která z možností nastává, může pomoci prozkoumání Gödelova důkazu.
18
Důkaz Gödelovy věty
K KAAPPIITTO OLLA A 22::
D DŮŮKKAAZZ G GÖ ÖD DE ELLO OV VY YV VĚ ĚT TY Y
Thit sentence is not self-referential because "thit" is not a word. This is not a complete. Sentence. This either. Hofstdter's Law: It always takes longer than you expect, even when you take into account Hofstadter's Law. - Douglas R. Hofstadter Úplně na konci této práce využiji ještě jeden Douglasův nápad, o kterém už nenapíšu, že je jeho, protože to bude na konci.
Pokusím se načrtnout, jak probíhá Gödelův důkaz, a všímat si zajímavých kroků, které se tu provádějí a nad možností jejichž formalizace se budu později zamýšlet. Důkaz se dá rozdělit na tři hlavní části. První by šlo nazvat aritmetizací jazyka aritmetiky, druhou zachycením dokazatelnosti uvnitř aritmetiky a třetí sestrojením autoreferenční formule.
ARITMETIZACE JAZYKA ARITMETIKY Nejprve přiřadíme čísla symbolům, které tvoří formule Peanovy aritmetiky (to ještě nebudou gödelovská čísla):6 symbol → ( ) = 0 S + ∙ > ≥ xi
číslo 1 2 3 4 5 6 7 8 9 10 11 12 13 i-té prvočíslo větší než 13
Formulím jsou takto přiřazeny posloupnosti čísel.7 Posloupnostem čísel můžeme nyní přiřadit čísla tak, že posloupnosti čísel n1, n2, ...nk přiřadíme číslo p1n ∙ p2n2 ∙ ... pknk,
Gödel pracoval s trochu jiným jazykem, a proto bylo odlišné i jeho kódování. Rozdíl ale není nijak podstatný. Gödel ve svém článku nejprve říká, že formule můžeme považovat za posloupnosti čísel, a později je dokonce ztotožňuje s čísly, které jsou jejich kódy, takže podstatná tvrzení místo o formulích vyslovuje o číslech. Gödelova věta pak v originále přímo netvrdí existenci formálně nedokazatelné formule, ale existenci čísla s určitou (v jazyce aritmetiky popsatelnou) vlastností. 6 7
19
Důkaz Gödelovy věty
kde pi je i-té prvočíslo. Tak dostaneme Gödelovo číslo formule, které byla přiřazena ta která posloupnost čísel. Například formule ,0=0’, které bude nejprve přiřazena posloupnost [8,7,8], bude mít Gödelovo číslo 28 ∙ 37 ∙ 58 = 218 700 000 000. Někdy se říká, že díky aritmetizaci jazyka aritmetiky si můžeme představit, že aritmetické formule mluví o formulích. Tím se ale ještě nic nevysvětluje – podobně si můžeme představit, že aritmetické formule mluví o tom, co budeme mít dnes k večeři: pokud třeba jednotlivým ingrediencím přiřadíme čísla (např. soli jedničku, bramborám dvojku apod.), můžeme si představit, že formule říká, že večeře bude obsahovat přesně ty ingredience, jimž přiřazená čísla jsou ve formuli pojmenována (ať už o nich formule říká cokoli). Rozdíl je ale v tom, že mezi pravdivostí tvrzení o přirozených číslech a pravdivostí tvrzení o formulích nacházíme spojitost. Například, tvrzení Formule ,0=0’ začíná negací je ekvivalentní tvrzení číslo 218 700 000 000 je dělitelné číslem 21, ale ne číslem 22, které můžeme vyjádřit aritmetickou formulí, jež se nevejde do žádné svázatelné diplomové práce: x(S(S(S(...S(0)...))) = x ∙ S(S(0))) x(S(S(S(...S(0)...))) = x ∙ (S(S(0)) ∙ S(S(0)))).8 218 700 000 000-krát ,S’
218 700 000 000-krát ,S’
Přitom zdůvodnit podrobně tuto souvislost není úplně nejjednodušší. Například tu využíváme toho, že číslo má jediný prvočíselný rozklad – což se nám sice může zdát jasné, víme-li, co jsou prvočísla, nicméně je to tvrzení, jehož pravdivost můžeme dál zdůvodňovat. Ve svém důkaze Gödel ukázal, jak ke každé rekurzívní teorii Θ sestrojit takovou aritmetickou formuli φ(x,y), že pro každá čísla m a n, formule φ(m,n) vyjadřuje tvrzení ekvivalentní tomu, že číslo m je kód důkazu formule s kódem n. Jinými slovy, že vztah „... je kódem důkazu formule s kódem ...“ jde popsat jistou aritmetickou formulí. K dosažení výsledku (nalezení pravdivé a nedokazatelné formule) je ale potřeba vědět něco nejen o pravdivosti, ale i dokazatelnosti takové formule. K obojímu lze dospět s využitím pojmu rekurzívní funkce.
ZACHYCENÍ DOKAZATELNOSTI UVNITŘ TEORIE ARITMETIKY Klíčovou myšlenkou Gödelovy věty je zachycení formální dokazatelnosti uvnitř axiomatické teorie aritmetiky – ukázání, že formální teorie aritmetiky umí v jistém smyslu mluvit o dokazatelnosti v sobě samé. K tomu je potřeba ukázat dvě věci: jednak, že některé formule vyjadřují tvrzení ekvivalentní tvrzením o dokazatelnosti formulí, a jednak, že pravdivost některých takových formulí je ekvivalentní jejich dokazatelnosti. Gödelův postup byl takový, nejdřív ukázat spojitost mezi některými číselnými vlastnostmi, resp. relacemi, a vlastnostmi formulí a formálních důkazů, resp. vztahy mezi nimi, a zároveň ukázat, že příslušné číselné vlastnosti, resp. relace, jsou rekurzívní; potom ukázat, že ke každé rekurzívní vlastnosti nebo relaci existuje aritmetická formule, která ji popisuje a která je po dosazení jmen čísel za volné proměnné v dané teorii dokazatelná právě tehdy, je-li pravdivá. Tak dospějeme k formulím, o nichž můžeme tvrdit, že zachycují metamatematické pojmy (pojem důkazu formule, formální dokazatelnosti apod.) uvnitř axiomatické teorie aritmetiky.
8
Příklad s touhle formulí jsem si vypůjčil z knihy Ernesta Nagela a Jamese R. Newmana: Gödelův důkaz.
20
Důkaz Gödelovy věty
Rekurzívní funkce, vlastnosti a relace Rekurzívní funkce mohou sloužit k matematickému vymezení intuitivního pojmu algoritmu: má se za to, že rekurzívní funkce jsou takové funkce na přirozených číslech,9 k nimž existuje algoritmus, který je v konečném čase počítá. Pro lepší představu uvedu jejich definici. Gödel původně definuje rekurzívní funkce takto: Funkce f je rekurzívní, jestliže existuje posloupnost funkcí na přirozených číslech f1,...fn taková, která končí f a má tu vlastnost, že každá funkce fk z této posloupnosti je z některých dvou předcházejících definována rekurzí nebo vzniká z některých předcházejících substitucí nebo je to konstantní funkce nebo funkce přičítání jedničky. Takovým funkcím se později začalo říkat primitivně rekurzívní. Obecné rekurzívní funkce lze narozdíl od primitivně rekurzívních odvozovat kromě rekurze a substituce i tzv. minimalizací. Dají se definovat jako speciální případ tzv. částečně rekurzívních funkcí: 1. funkce f taková, že pro všechna přirozená čísla n je f(n)=c, kde c je nějaké přirozené číslo, je částečně rekurzívní. 2. funkce f taková, že pro všechna přirozená čísla n je f(n)=n+1, je částečně rekurzívní. 3. jsou-li funkce g a h částečně rekurzívní, pak funkce f taková, že pro všechna přirozená čísla n1,... nk je f(0,n2,...nk)=g(n2,...nk) a f(n1+1,n2,...nk)=h(f(n1,n2,...nk),n1,...nk), je částečně rekurzívní (f je z g a h definována rekurzí). 4. jsou-li funkce h a g1, ... gm částečně rekurzívní, pak funkce f taková, že pro všechna přirozená čísla n1, ... nk je f(n1,...nk)=h(g1(n1,...nk),...,gm(n1,...nk)), je částečně rekurzívní (f vzniká z g1, ... gm a h substitucí). 5. je-li funkce g částečně rekurzívní, pak funkce f taková, že pro všechna přirozená čísla n1, ... nk: f(n1,...nk)=m, jestliže m je nejmenší číslo, pro něž je g(m,n1,...nk)=0, a f není pro hodnoty argumentů n1, ... nk definována, jestliže takové číslo neexistuje, je částečně rekurzívní (f je z g odvozena minimalizací). 6. žádné jiné funkce částečně rekurzívní nejsou.10 Rekurzívní funkce je taková, která je částečně rekurzívní a totální, tj. má hodnotu pro všechny hodnoty argumentů. Délce nejkratší posloupnosti funkcí takové, že každá je buď funkce z bodu 1. nebo 2. anebo je odvozena z funkcí jí v posloupnosti předcházejících podle bodů 3., 4. nebo 5., a poslední funkcí je funkce f, se říká délka odvození funkce f.
Tedy takové, hodnoty jejichž argumentů i jejichž hodnoty jsou přirozená čísla. Definice primitivně rekurzívní funkce vznikne z předchozí vynecháním bodu 5. a záměnnou slova „částečně“ za slovo „primitivně“.
9
10
21
Důkaz Gödelovy věty
Rekurzívní relace11 se definují s pomocí rekurzívních funkcí: Relace R je rekurzívní, jestliže existuje rekurzívní funkce f taková, že R(n1,...nk) f(n1,...nk)=0 platí pro všechna n1, ... nk. Funkci f se říká charakteristická funkce relace R. Jestliže definice rekurzívní funkce dobře vymezuje intuitivní pojem algoritmu, lze soudit, že rekurzívní relace budou všechny takové, u nichž dokážeme snadno vymyslet postup (algoritmus) pro rozhodnutí, zda nějaká čísla jsou nebo nejsou v této relaci. Další postup v důkazu nyní je, dokázat, že každou rekurzívní relaci lze popsat takovou aritmetickou formulí, která je po dosazení jmen čísel za volné proměnné pravdivá právě tehdy, jeli formálně dokazatelná v libovolné bezesporné teorii, v níž jsou dokazatelné Peanovy axiomy. To je známo jako korespondenční lemma.
Korespondenční lemma Ke každé rekurzívní relaci R existuje taková formule φ(x1,...xk), že pro každá přirozená čísla n1,...nk, ◦ formule φ(n1,...nk) je pravdivá právě tehdy, když R(n1,...nk), a pro každou teorii Θ splňující předpoklady Gödelovy věty, ◦ formule φ(n1,...nk) je dokazatelná v teorii Φ právě tehdy, když R(n1,...nk).12 O formuli splňující první podmínku budu říkat, že popisuje relaci R. O formuli splňující druhou budu říkat, že relaci R v teorii Θ vystihuje. Důkaz lemmatu se provádí indukcí podle délky odvození charakteristické funkce: postupujeme od jednoduchých rekurzívních funkcí ke složitějším a ukazujeme, jak sestrojit aritmetickou formuli, řekněme φ(y,x1, ...xn), která říká, že hodnota dané funkce pro hodnoty argumentů x1, ...xn je y, a z níž dosazením jmen čísel za volné proměnné vznikne formule, která je v příslušné teorii dokazatelná právě tehdy, je-li pravdivá.13 K důkazu Gödelovy věty tu potřebujeme dokázat určité obecné tvrzení o relacích mezi čísly. Kdybychom ale chtěli dokázat existenci nedokazatelné a pravdivé formule pro jednu konkrétní teorii (třeba pro Peanovu aritmetiku), stačilo by dokázat takové tvrzení o jediné relaci, jak se ukáže později. V tom případě bychom ani nemuseli mluvit o tom, že daná relace je rekurzívní, díky tomu, že bychom ji mohli přímo popsat.14 To bude podstatné pro formalizaci důkazu pravdivosti Gödelovy formule pro konkrétní teorii.
Pro jednodušší vyjadřování budu dále předstírat, že vlastnosti jsou jednomístné relace. To pro všechny formule splňující první podmínku neplatí: Gödel ukázal, že existuje pravdivá formule φ(n), která není z dané teorie dokazatelná, přestože číslo n má vlastnost popsanou formulí φ(x). 13 Gödel ve skutečnosti o pravdivosti nalezené formule vůbec nemluví – mluví jen o její dokazatelnosti. Vědět, kdy je taková formule pravdivá, budeme potřebovat k tomu, abychom mohli v závěru důkazu tvrdit pravdivost formule, jež je v dané teorii nedokazatelná. Gödel ovšem v originálním důkazu netvrdí pravdivost této formule, ale to, že není (u teorií, které splňují maličko silnější požadavky než ty, které jsme vyslovili my) dokazatelná ani ona, ani její negace. 14 Požadavek rekurzívnosti relace nám zaručí, že k ní (ať už je to kterákoli) dokážeme najít příslušnou formuli. 11 12
22
Důkaz Gödelovy věty
Problém dokazatelnosti formule
????
Korespondenční lemma
Problém pravdivosti aritmetické formule
Problém nácházení se v rekurzívní relaci
(dokonce je to ta samá formule)
Korespondenční lemma
Problém dokazatelnosti aritmetické formule
Obrázek 2.1: Korespondenční lemma
Rekurzívní teorie Pojem rekurzívnosti se kromě u číselných funkcí a relací vyskytuje taky v požadavku, aby teorie, o kterých Gödelova věta mluví, byly rekurzívní (díky tomu bude rekurzívní i relace „... je kód důkazu formule s kódem ...“). Je ale potřeba vyjasnit, jak souvisí rekurzívnost teorie s rekurzívností funkcí na přirozených číslech. Pomocí pojmu rekurzívní funkce můžeme definovat pojem rekurzívní množiny přirozených čísel: Množina A je rekurzívní, jestliže existuje rekurzívní funkce f taková, že pro každé přirozené číslo n nA f(n)=0. Teorie je ale množina axiomů (tedy formulí), nikoli přirozených čísel. Můžeme ovšem definici rekurzívních množin rozšířit i na množiny formulí díky tomu, že formule umíme kódovat přirozenými čísly: Množina formulí Φ je rekurzívní, jestliže existuje rekurzívní funkce f taková, že pro každou formuli φ a číslo n, které je jejím kódem, platí: φΦ nA. Důležité je, že ke každé formuli lze v konečném čase algoritmicky vypočítat její kód, a proto lzeli algoritmicky zjistit, zda f(n)=0 pro jakékoli číslo n, lze i algoritmicky zjistit, zda libovolná formule náleží do množiny Φ. Jestliže tedy rekurzívní množiny čísel jsou takové, o nichž můžeme algoritmicky rozhodnout, zda do nich libovolné číslo patří, jsou rekurzívní množiny formulí
23
Důkaz Gödelovy věty
takové, o nichž lze algoritmicky rozhodnout, zda do nich libovolná formule patří. Gödelova věta potom hovoří o teoriích, u nichž jde algoritmicky rozhodnout, co je a co není jejich axiom.
Relace „... je důkaz ...“ Gödel ve svém důkaze ukázal, že vztah „... je kód důkazu formule s kódem ... v teorii Θ“ je rekurzívní, jestliže teorie Θ splňuje předpoklady věty. Aby k tomu dospěl, postupoval v přibližně 45 krocích od jednodušších číselných relací ke složitějším a ukazoval, že jsou rekurzívní. Přitom se tu počítá s tím, že u relací, které odpovídají určitým vlastnostem formulí a formálních důkazů a vztahům mezi nimi, jde zřejmé z jejich definice, jak jim odpovídají.15 Binární relaci mezi čísly „... je kód důkazu formule s kódem ... v teorii Θ“ budu dál někdy značit ,DůkΘ’ a místo tvrzení: Číslo m je kód důkazu formule s kódem n v teorii Θ. budu psát DůkΘ(m,n). Aritmetickou formuli, jejíž existenci zaručuje korespondenční lemma a která popisuje a v teorii Θ vystihuje relaci DůkΘ, budu dále značit ,DůkΘ(x,y)’. Formule ,x DůkΘ(n)’ nyní vyjadřuje tvrzení Žádné číslo není kódem formálního důkazu formule s kódem n v teorii Θ, které je ekvivalentní: Číslo n je kód formule, která není v teorii Θ formálně dokazatelná, díky tomu, že každý důkaz má nějaký kód. Z dokazatelnosti této formule v teorii Θ navíc plyne její pravdivost. Předpokládejme totiž, že formule ,x DůkΘ(n)’ je nepravdivá. Pak existuje nějaké číslo m takové, že m je kódem formálního důkazu formule s kódem n v teorii Θ, neboli DůkΘ(m,n), a protože DůkΘ je rekurzívní relace, je formule ,DůkΘ(m,n)’ formálně dokazatelná v teorii Θ, a proto je formálně dokazatelná i formule ,x DůkΘ(n)’. Protože ale u teorie Φ předpokládáme její bezespornost, není v ní dokazatelná současně formule ,x (DůkΘ(x,n))’. Ukázali jsme tedy, že pokud není formule ,x DůkΘ(n)’ pravdivá, není ani v teorii Φ formálně dokazatelná, a tedy z její dokazatelnosti plyne její pravdivost.
SESTROJENÍ AUTOREFERENČNÍ FOMULE Nejjednodušší případ formule, která by vyjadřovala tvrzení ekvivalentní své vlastní nedokazatelnosti, by byla formule tvaru ,x DůkΘ(x,n))’, jejíž kód by byl n. Protože ale kód formule je (dramaticky) větší než délka této formule a délka jména n je o něco větší než toto číslo, je kód formule obsahující jméno čísla n (dramaticky) větší než toto číslo. Proto taková formule nemůže existovat. Formuli vyjadřující tvrzení ekvivalentní své vlastní bezespornosti bude proto potřeba najít rafinovaněji. Nejdřív ukážu obecný způsob, jak pro každou teorii, která splňuje předpoklady Gödelovy věty, a k libovolné aritmetické formuli φ(x) sestrojit jinou aritmetickou formuli ψ s kódem n, která je pravdivá právě tehdy, když je pravdivá φ(n) a v dané teorii je dokazatelná implikace φ(n) ↔ ψ. A taky to jde poznat z toho, jak Gödel tyto vlastnosti a vztahy pojmenovává. Například vlastnost čísla „být kódem elementární formule“ zapíše ,... ist ein Elementarformel’, případně ,Elf(...)’, vlastnost „být kódem některého z axiomů“ zapíše ,... ist ein Axiom’, případně ,Ax(...)’, vztah „... je kódem důkazu formule s kódem ...“ zapíše ,... ist ein Beweis für die Formel ...’, případně ,...B...’, apod. 15
24
Důkaz Gödelovy věty
Větě, která tvrdí existence takové formule, se říká věta o pevném bodu. Dá se ukázat, že (rekurzívní) relaci „... je kód formule, která vznikne z formule s kódem ... dosazením jména čísla ... za proměnnou y“ jde popsat aritmetickou formulí, nazvěme ji Subst, která ji v dané teorii vystihuje a pro každá čísla n a k je tu dokazatelná formule x y ((Subst(x,n,k) Subst(y,n,k)) → x=y). Pro všechna čísla n, m a k je pak formule Subst(m,n,k) pravdivá právě tehdy, když formule s kódem m vznikne dosazením termu k za proměnnou y ve formuli s kódem n. Označme χ(x,y) formuli Subst(x,y,y) φ. Pak pro všechna čísla m a n je formule χ(m,n) pravdivá právě tehdy, když m je kód formule, která vznikne z formule s kódem n dosazením termu n za proměnnou y a φ(m) je pravdivá. Formule x χ(n) je potom pro libovolné číslo n pravdivá právě tehdy, když formule, která vznikne z formule φ dosazením jména toho čísla, které je kódem formule, jež vznikne dosazením termu n za proměnnou y do formule s kódem n, je pravdivá, jinými slovy, když φ je pravda o kódu formule vzniklé z formule s kódem n dosazením termu n za y. Kód formule x χ(y) označím k a formuli, která vznikne dosazením termu k za proměnnou y v předchozí formuli, označím ψ. Formule ψ, x χ(k), je tedy pravdivá, jestliže formule, která vznikne z formule φ dosazením jména toho čísla, které je kódem formule, jež vznikne dosazením termu k za proměnnou x do formule s kódem k, je pravdivá, jinými slovy, když φ je pravda o kódu formule vzniklé z formule s kódem k dosazením termu k za y. Ovšem formule, která vznikne z formule s kódem k dosazením termu k za proměnnou y je právě ψ! Formule ψ je tedy pravdivá, jestliže formule, která vznikne z formule φ(x) dosazením jména kódu ψ, je pravdivá. Jestliže tedy kód formule ψ je n, je ψ pravdivá právě tehdy, když je pravdivá φ(n). Protože formule Subst v dané teorii vystihuje relaci, kterou popisuje, je tu dokazatelná formule Subst(n,k,k), a proto i x(Subst(x,k,k) → x=n). Díky tomu jsou tu dokazatelné i ekvivalence x(Subst(x,k,k) φ(x)) ↔ (Subst(n,k,k) φ(n)) ↔ φ(n), přičemž formule vlevo je ψ. Teď můžeme sestrojit formuli, jejíž pravdivost je ekvivalentní její nedokazatelnosti v dané teorii. K formuli y Důk(y,x)
25
Důkaz Gödelovy věty
umíme výše popsaným postupem sestrojit takovou formuli ψ s kódem k, která je pravdivá právě tehdy, když je pravdivá formule y Důk(y,k), neboli, když formule s kódem k není v dané teorii dokazatelná. Pravdivost aritmetické formule ψ je tedy ekvivalentní její nedokazatelnosti v dané teorii. Abychom ukázali, že sestrojená formule je pravdivá a není v dané teorii dokazatelná, je potřeba ještě ověřit, že pokud je v ní dokazatelná, je pravdivá. Jestliže ψ je tu dokazatelná, je tu dokazatelná i formule y Důk(y,k). Protože ta je tvaru ,y φ’, kde formule φ(y) vystihuje rekurzívní vlastnost, je za předpokladu, že je tu dokazatelná, taky pravdivá, díky čemuž je pak pravdivá i ψ. Formuli takto sestrojenou k teorii Θ označím γΘ a budu jí říkat Gödelova formule pro teorii Θ. Gödelovu formuli umíme sestrojit k jakékoliv rekurzívní teorii v jazyce aritmetiky, protože k takovým víme, jak sestrojit aritmetické formule Subst a Důk s požadovanými vlastnostmi.
26
Formalizace důkazu
K KAAPPIITTO OLLA A 33::
FFO OR RM MA ALLIIZ ZA AC CE ED DŮ ŮK KAAZ ZU U
Je načase, pokusit se Gödelův důkaz formalizovat, aby se ukázalo, kde nemůžeme uspět. K tomu bude potřeba, uvědomit si, o čem se v důkaze mluví (veškerá podstatná tvrzení, která se v důkazu objevují, bychom totiž měli být schopni vyjádřit nějakou formulí, jež bude součástí formálního důkazu) a jaké myšlenkové postupy se tu uplatňují (jim odpovídající odvození bude totiž potřeba ve formálním důkaze provést). Místo o formálních teoriích budu dál mluvit o formálních systémech, tvořených množinou axiomů a odvozovacími pravidly, protože připadá v úvahu, že bychom k formalizování Gödelova důkazu potřebovali dodat i nová odvozovací pravidla a tedy rozšířit kalkul. U formálních systémů budu ve stejném smyslu jako u formálních teorií mluvit o jejich bezespornosti, nepůjde už ale ve stejném smyslu jako u teorií mluvit o tom, že jsou rekurzívní – dalo by se nanejvýš říct, že je rekurzívní množina jejich axiomů. Důležitější tu ale bude, zda je rekurzívní relace „... je kód důkazu formule s kódem ... v tomto formálním systému“ při nějakém vhodném kódování. Jazykem formálního systému budu rozumět jazyk určovaný množinou formulí v něm dokazatelných. Je potřeba upozornit na to, že Gödelova věta v té podobě, v jaké jsem ji uvedl v minulé kapitole, se vztahuje jen na formální systémy tvořené standardním kalkulem a axiomy v jazyce aritmetiky. Později v této kapitole uvedu její zobecněnou verzi, která se bude vztahovat i na mnohem bohatší formální systémy.
O ČEM SE V DŮKAZE MLUVÍ V důkaze Gödelovy věty se mluví: ◦ o přirozených číslech, o rekurzívních funkcích, vlastnostech a relacích, o posloupnostech (kterými jsou formule a důkazy) a provádíme-li důkaz důsledně, tak taky třeba o prvočíselných rozkladech čísel. Přitom pro důkaz pravdivosti a nedokazatelnosti Gödelovy formule pro konkrétní teorii není potřeba mluvit o rekurzívních funkcích atd., stačí jen popsat jednu konkrétní rekurzívní relaci. ◦ o formulích (posloupnostech symbolů) a o jejich pravdivosti a o formálních důkazech v určité teorii. Jazyk formálního systému, v němž bychom mohli Gödelův důkaz formalizovat, by měl umožnit vyjádřit příslušná tvrzení.
ELEMENTÁRNÍ KROKY V DŮKAZU V Gödelově důkazu se (stejně jako v každém jiném) počítá s tím, že některé kroky není potřeba dál zdůvodňovat – jsou evidentně správné. K zachycení některých takových kroků slouží kalkul predikátové logiky (který určuje, jaké kroky jsou logicky správné) a axiomy aritmetiky (vyjadřující evidentně pravdivá tvrzení o přirozených číslech). Pokusím se popsat, co z toho, co je pro nás zřejmé, využíváme v důkazu Gödelovy věty k učinění elementárních, dále nezdůvodňovaných kroků: 1. Umíme provést (alespoň některé) logicky správné úsudky – takové, s nimiž nemůžeme od pravdivých tvrzení dospět k nepravdivým. To nám umožňuje přecházet od jednoho pravdivého tvrzení k jinému. - logické usuzování v matematice má formálně zachytit kalkul predikátové logiky.
27
Formalizace důkazu
2. Víme leccos o přirozených číslech. Díky tomu můžeme usuzováním dospívat k dalším poznatkům o přirozených číslech. - podstatné poznatky o přirozených číslech mají vyjadřovat Peanovy axiomy. 3. Víme, co která aritmetická formule říká, např. že formule ,x(x+1≠x)’ říká, že z každého čísla dostaneme přičtením jedničky jiné, neboli, že pro každé číslo x je x+1 různé od x.16 Díky tomu můžeme o některých aritmetických formulích – třeba o Peanových axiomech – tvrdit, že jsou pravdivé. 4. Víme, že formule určitého tvaru jsou obecně pravdivé a že některá odvozovací pravidla vystihují obecně logicky správné úsudky. Díky tomu víme, že axiomy vzniklé dosazením formulí do schémat kalkulu i Peanovy aritmetiky jsou pravdivé a že z pravdivých formulí není možné v kalkulu odvodit nepravdivé. 5. Víme, že můžeme ztotožnit formule (posloupnosti symbolů) s posloupnostmi čísel. Přesněji řečeno, že pokud nahradíme běžné symboly, které se vyskytují ve formulích, čísly (a náležitě pozměníme schémata kalkulu a Peanovy aritmetiky a odvozovací pravidla), budou v nové teorii a v novém kalkulu dokazatelné právě ty posloupnosti čísel, které vzniknou nahrazením symbolů v dokazatelných formulích. K podrobné formalizaci Gödelova důkazu bychom potřebovali formální systém, který by umožnil ke každému z takto intuitivně správných kroků provést formální odvození.
PRVNÍ POKUS O FORMALIZACI Nejdřív zkusím najít systém, v němž by bylo možné zachytit hrubou strukturu důkazu pravdivosti Gödelovy formule pro Peanovu aritmetiku, přičemž důkaz některých tvrzení vynechám s tím, že tato tvrzení učiním přímo axiomy daného systému. Potom prozkoumám, zda se na takový systém vztahuje Gödelova věta.
Co je potřeba formální systém „naučit“ K tomu, aby jednotlivé kroky neformálního důkazu Gödelova výroku šlo v novém systému formalizovat, by mělo stačit, vyjádřit to, co je nám zřejmé a co jsem se dříve pokusil shrnout v bodech 1. - 5., axiomy a odvozovacími pravidly: 1. Axiomy standardního kalkulu a jeho odvozovací pravidla, ovšem nyní zahrnující a aplikovatelná na formule v bohatším jazyce – viz. dále. 2. Axiomy Peanovy aritmetiky. 3. Axiomy, které říkají, co která formule vyjadřuje, neboli že každá formule, která říká, že A, je pravdivá právě tehdy, když A. To vyžaduje, aby v novém systému bylo možné vyjádřit tvrzení o formulích a jejich pravdivosti. Jedna možnost je (vzhledem k tomu, že jména v jazyce Peanovy aritmetiky označují – při jejich standardním čtení – jen přirozená čísla) obohatit jazyk nového systému: ◦ o nový druh proměnných, které budu značit velkými písmeny. Za obor proměnnosti těchto proměnných se budou považovat výrazy jazyka aritmetiky. ◦ o několik predikátových symbolů, sloužících k popisu aritmetických formulí a vyjádření jejich pravdivosti: Přesněji řečeno, poznáme to potom, co nám někdo vysvětlí, co symboly použité ve formulích znamenají. Co která formule vyjadřuje, je určeno tím, jaký význam kterému symbolu přiřadíme – mohli bychom například symbol ,0’ považovat za označení jedničky, v kterémžto případě by formule vyjadřovaly jiná tvrzení. 16
28
Formalizace důkazu
Predikátový symbol ve formuli Prom(X,y) Konst(X) Fun1(X,Y) Fun2(X,Y,Z) Fun3(X,Y,Z) Elem1(X,Y,Z) Elem2(X,Y,Z) Elem3(X,Y,Z) Neg(X,Y) Impl(X,Y,Z) Disj(X,Y,Z) Kvant(X,y,Z) JePravdiváPA(X)
Standardní čtení X je proměnná y X je konstanta 0 X je term tvaru ,S(Y)’ X je term tvaru ,(Y)+(Z)’ X je term tvaru ,(Y)∙(Z)’ X je elementární formule tvaru ,X=Y’ X je elementární formule tvaru ,Y>Z’ X je formule tvaru ,Y≥Z’ X je formule tvaru ,(Y)’ X je formule tvaru ,(Y)→(Z)’ X je formule tvaru ,(Y)(Z)’ X je formule tvaru ,y(Z)’ X je pravdivá aritmetická formule
Ke každému aritmetickému termu t pak definujeme formuli ψt(X), která říká, že X je term t, a ke každé aritmetické formuli φ definujeme formuli ψφ(X), která říká, že X je formule φ:17 ◦ Jestliže term t je proměnná y, pak ψt je formule Prom(X,y). Podobně pro konstantu. ◦ Jestliže t je term tvaru ,S(t1)’, pak ψt je formule ,Y(Fun1(X,Y) ψt1(Y))’. ◦ Jestliže t je term tvaru ,t1+t2’, pak ψt je formule ,Y Z (Fun2(X,Y,Z) ψt1(Y) ψt2(Z))’. Podobně pro funktor násobení. ◦ Jestliže φ je formule ,t1=t2’, pak ψφ je formule ,Y Z (Elem1(X,Y,Z) ψt1(Y) ψt2(Z))’. Podobně pro ostatní atomické formule. ◦ Jestliže φ je tvaru ,φ1’, pak ψφ je formule ,Y (Neg(X,Y) ψφ1(Y))’. ◦ Jestliže φ je tvaru ,φ1 → φ2’, pak ψφ je formule ,Y Z (Impl(X,Y,Z) ψφ1(Y) ψφ2(Z))’. Podobně pro disjunkci. ◦ Jestliže φ je tvaru ,y φ1’, pak ψφ je formule ,Z (Kvant(X,y,Z) ψφ1(Z))’. Nový formální systém pak bude pro každou aritmetickou formuli φ obsahovat axiom X (ψφ(X) → PravdiváPA(X)) ↔ φ, který říká, že formule φ je pravdivá právě tehdy, když φ. 4. Nejjednodušší je, zavést axiom, který tvrdí pravdivost všech formulí dokazatelných v Peanově aritmetice: X (JeDokazatelnáPA(X) → JePravdiváPA(X)). Tvrzení, které formule vyjadřuje, pro nás asi není zřejmé – je nejspíš potřeba dokázat ho indukcí podle délky důkazu. Formalizací takového důkazu se budu zabývat později – prozatím učiním formuli axiomem. 5. Axiom popisující vztah mezi číselnými relacemi a odvoditelností v kalkulu Peanovy aritmetiky. Gödel ve svém důkaze využije asi tak 45 jednodušších kroků, aby nás přesvědčil, že číselná relace „... je kód důkazu formule s kódem ... v Peanově aritmetice“, zkráceně DůkPA, je 17 To, že formule ψ (X), resp. ψ (X), říká, že X je term t, resp. formule φ, je dáno tím, jaký význam jsme přidělili φ t predikátům Fun1, Elem1, Neg atd.
29
Formalizace důkazu
rekurzívní. Mohli bychom se pokusit dodat axiomy, které by umožnily formalizovat všech 45 kroků, prozatím však postačí, když bude náš formální systém obsahovat axiom: y (x DůkPA(x,y) ↔ X (JeKódPA(y,X) JeDokazatelnáPA(X))), vyjadřující tvrzení, ke shledání jehož pravdivosti potřebuje běžný smrtelník kolem 45 kroků, totiž že existuje číslo, které je ve vztahu DůkPA k číslu m, právě tehdy, když formule s kódem m je formálně dokazatelná. Přitom se tu myslí kódování aritmetických formulí, jaké jsme popsali výše. Pro jednoduchost budu to, které číslo je kódem které formule, popisovat axiomy: X (ψφ(X) ↔ JeKódPA(n,X)) pro každou formuli φ a její kód n (kdybychom měli formalizovat důkaz tvrzení vyjádřeného předchozím axiomem, potřebovali bychom, aby formální systém „věděl“, jak se kódují formule, takhle to ale není nutné). Formuli ,y DůkPA(y,x)’ budu zapisovat ještě zkráceněji ,DokPA(x)’. Formální systém tvořený výše popsanými axiomy a standardním kalkulem predikátové logiky nazvu ZS1. ZS1 tedy obsahuje: ◦ axiomy standardního kalkulu predikátové logiky a jeho pravidla, aplikovatelná na formule se dvěma druhy proměnných ◦ axiomy Peanovy aritmetiky ◦ axiomy: X (ψφ(X) → JePravdiváPA(X)) ↔ φ pro každou aritmetickou formuli φ, X (JeDokazatelnáPA(X) → JePravdiváPA(X)), X (ψφ(X) ↔ JeKódPA(n,X)) pro každou aritmetickou formuli φ a její kód n, x (DokPA(x) ↔ Y (JeKódPA(x,Y) JeDokazatelnáPA(Y)))
Důkaz γPA v ZS1 Jestliže n je kód Gödelovy formule pro Peanovu aritmetiku a m je kód formule ,0≠0’, pak formuli DokPA(n) → DokPA(m) 18
jde dokázat v Peanově aritmetice, a proto i v ZS1. Protože v ZS1 jde dokázat formuli 0≠0, jde tu dokázat i X (ψ,0≠0’(X) → JePravdiváPA(X)), X (ψ,0≠0’(X) → JeDokazatelnáPA(X)), X (JeKódPA(m,X) → JeDokazatelnáPA(X)) (díky tomu, že formule ,X (ψ,0≠0’(X) ↔ JeKódPA(m,X))’ je axiom) a DokPA(m). Tohle tvrzení nemá být nijak samozřejmé. Podstatnou část důkazu tvoří důkaz korespondenčního lemmatu pro relaci DůkPA, který se od neformálního důkazu pro tuto konkrétní relaci liší – mimo to, že je formální – v tom, že místo odpovídající formule se „sestrojuje“ číslo (její kód) a místo o její dokazatelnosti se mluví o vlastnosti DokPA. To samé pak platí o celé Gödelově formuli. Přitom že to lze provést, je možné díky tomu, že Peanova aritmetika toho „ví dost“ o rekurzívních relacích. 18
30
Formalizace důkazu
Proto je dokazatelná formule DokPA(n), což je v Peanově aritmetice nedokazatelná aritmetická formule, kterou jsme chtěli dokázat.
Co chybí systému ZS1 Systém ZS1 neobsahuje axiomy, které by popisovaly pojmy dokazatelnosti formule a kódování tak, jak je definujeme my. Dalo by se říct, že systém ZS1 „neví“, co to znamená být formálně dokazatelný, „ví“ jen, že některé formule tuto vlastnost mají,19 a taky „neví“, jak se kódují formule, „ví“ jen, které číslo je kódem které formule. K formalizaci podrobného důkazu Gödelova výroku by bylo potřeba najít axiomy, které by odpovídaly našim definicím pojmů dokazatelnosti a kódování formulí a axiomy ZS1, které popisují neformálně dokazovaná tvrzení, formálně dokázat. Poznámka: stejně jako bychom mohli říct, že významy predikátů JeDokazatelnáPA a JeKódPA nejsou v axiomech systému ZS1 dobře zachyceny, dá se nejspíš tvrdit, že významy predikátů Prom, Konst, Fun1, Fun2, Fun3, Elem1, Elem2, Elem3, Neg, Impl, Disj, Gen a JePravdiváPA dobře zachyceny jsou, a to axiomy tvaru X (ψφ(X) → JePravdiváPA(X)) ↔ φ. V systému ZS1 nejde formalizovat důkaz pravdivosti dokazatelných formulí už z těchto důvodů: ◦ ZS1 „neví“, co je to formální dokazatelnost ◦ schéma indukce, které obsahuje ZS1, se vztahuje jen na formule v jazyce aritmetiky, nikoli na formule v jazyce ZS1, které mluví o dokazatelnosti a pravdivosti formulí. Ani jedno se ovšem nezdá být nepřekonatelnou překážkou. Otázku, jestli to jsou jediné překážky, odložím na později. V systému ZS1 je dokazatelná aritmetická formule, která není dokazatelná v Peanově aritmetice. Dá se o něm navíc soudit, že je bezesporný, díky tomu, že všechny jeho axiomy vyjadřují pravdivá tvrzení o přirozených číslech a formálních důkazech v Peanově aritmetice. Zdá se tedy, že přirozená čísla popisuje (za cenu obohacení jazyka a přidání axiomů) o něco lépe než Peanova aritmetika. Můžeme se ptát, zda jsme (čirou náhodou) nezískali formální systém, v němž by byly formálně dokazatelné všechny aritmetické formule vyjadřující tvrzení, která umíme (neformálně) dokázat my. Umíme najít pravdivou aritmetickou formuli, která by nebyla v ZS1 dokazatelná? Především je třeba říct, že na formální systém se Gödelova věta v té podobě, v jaké je uvedena na začátku předminulé kapitoly a jaké důkaz tu byl načrtnut, nevztahuje. Ta totiž mluví o formálním dokazování v teoriích s jazykem Peanovy aritmetiky. Není ale těžké dokázat Gödelovu větu i pro formální systém, jakým je ZS1: stačí ◦ zvolit vhodné kódování formulí rozšířeného jazyka a ◦ sestrojit formuli DůkZS1 obdobně jako formuli DůkPA. To je možné díky tomu, že množina axiomů ZS1 je pořád rekurzívní a odvozovací pravidla jsou stejná. Zbytek důkazu pak proběhne stejně jako u teorií s jazykem Peanovy aritmetiky. Díky tomu, že víme o pravdivosti axiomů ZS1, umíme dokázat i pravdivost Gödelovy formule pro něj. Jestliže příčinou nedokazatelnosti Gödelovy formule pro Peanovu aritmetiku v ní samé byla nemožnost mluvit v jejím jazyce o formálních důkazech v ní – čehož k neformálnímu důkazu využíváme – není divu, že v ZS1 je nedokazatelná Gödelova formule pro něj: formule ZS1 umějí mluvit o aritmetických formulích a formálních důkazech v Peanově aritmetice, ale ne (alespoň při
19
Totiž ty, k nimž existuje číslo, jež je v relaci DůkPA k jejich kódu.
31
Formalizace důkazu
jejich standardním čtení) o formulích ZS1 a formálních důkazech v něm.20 Můžeme se proto pokusit sestrojit formální systém, který by o formálních důkazech v sobě samém mluvit dokázal. Než se do toho pustím, vyslovím ještě obecnější verzi Gödelovy věty, než je ta uvedená v předminulé kapitole, která bude mluvit o formálních systémech s různými jazyky.
Obecnější verze Gödelovy věty Nechť formální systém T je takový, že existuje prosté zobrazení f, které každé formuli z jazyka tohoto systému a každé posloupnosti takových formulí přiřadí přirozené číslo, a navíc takové, že platí: ◦ k relaci Subst takové, že každá čísla m, n a k jsou v této relaci právě tehdy, když existují formule φ a ψ v jazyce systému T, pro něž je f(φ)=m a f(ψ)=n a formule φ vznikne z formule ψ dosazením termu ,k’ za proměnnou y, existuje taková aritmetická formule χ, že χ popisuje relaci Subst a navíc je pro všechna m, n a k, která jsou v této relaci, v systému T dokazatelná formule tvaru x(χ(x,n,k) → x=m). ◦ relace Důk taková, že každá čísla m a n jsou v této relaci právě tehdy, když existují posloupnost formulí d a formule φ taková, že f(d)=m a f(φ)=n a d je kód důkazu φ v T, je rekurzívní. Nechť systém T je bezesporný a jsou v něm dokazatelné všechny formule, které jsou dokazatelné v Peanově aritmetice. Pak existuje pravdivá aritmetická formule, která není v T dokazatelná. Raději poznamenám, že tato verze není doslova zobecněním předchozí, protože mluví o formálních systémech, kde jsou důkazy posloupnosti formulí. Oproti tomu předchozí verze mluvila i o dokazatelnosti v kalkulech, kde důkaz tvoří něco jiného než posloupnosti formulí – totiž dokazatelnosti v libovolném standardním kalkulu predikátové logiky.
Formální systém ZS2 Nový formální systém se pokusím udělat co nejpodobnější systému ZS1, odlišný jen v tom, že bude mluvit o důkazech v sobě samém místo o důkazech v Peanově aritmetice. K tomu bude potřeba, moci v něm popsat všechny jeho formule (narozdíl od ZS1, který popisoval jen aritmetické formule). Drobný zádrhel je v tom, že když zavedeme predikát sloužící k popisu formule (např. predikát Elem1 jako u ZS1), rozšíříme i množinu formulí, o které chceme popisovat – konkrétně budeme potřebovat další predikát k popisu atomické formule vytvořené s pomocí tohoto predikátu (např. formule ,Elem1(X,Y,Z)’). Jedna možnost by byla, zavést obdobu uzávorkování v našem jazyce v podobě predikátového operátoru: aplikací tohoto operátoru na n-místný predikát P bychom získali n+1-místný predikát, který by říkal, že první člen je formule tvořená predikátem P na zbylými n členy. Kdybychom takový operátor označili ,JeFormule’, říkala by formule JeFormule P(X,x1,...xn), kde x1,...xn jsou buď velké nebo malé proměnné, že X je formule ,P(x1,...xn)’. Tím bychom se ale dost vzdálili jazyku predikátové logiky, a proto radši zavedu nekonečné množství nových predikátů: Raději poznamenám, že Gödelův důkaz jsme schopni provést díky tomu, že formule Peanovy aritmetiky v jistém smyslu o důkazech ve formálních teoriích mluvit umějí – totiž při nějakém jejich nestandardním čtení – ovšem v kalkulu není možné provést jisté odvození, které by z takového čtení vycházelo, a které my provést můžeme. 20
32
Formalizace důkazu
Predikátový symbol ve formuli Zamýšlené čtení X je proměnná y Prom1(X,y) Prom2(X,Y) X je proměnná Y Konst(X) X je konstanta 0 Fun1(X,Y) X je term tvaru ,S(Y)’ Fun2(X,Y,Z) X je term tvaru ,(Y)+(Z)’ Fun3(X,Y,Z) X je term tvaru ,(Y)∙(Z)’ Elem1(X,Y,Z) X je elementární formule tvaru ,Y=Z’ Elem2(X,Y,Z) X je elementární formule tvaru ,Y>Z’ Elem3(X,Y,Z) X je formule tvaru ,Y≥Z’ Elem4(X,Y) X je formule tvaru ,JePravdiváZS2(Y)’ Elem5(X,Y) X je formule tvaru ,JeDokazatelnáZS2(Y)’ Elem6(X,Y,Z) X je formule tvaru ,JeKódZS2(Y,Z)’ Neg(X,Y) X je formule tvaru ,(Y)’ Impl(X,Y,Z) X je formule tvaru ,(Y)→(Z)’ Disj(X,Y,Z) X je formule tvaru ,(Y)(Z)’ Kvant(X,y,Z) X je formule tvaru ,y(Z)’ Elem17(X,W,Y) X je formule tvaru ,Prom1(W,Y)’ Elem18(X,W,Y) X je formule tvaru ,Prom2(W,Y)’ ... Elem29(X,Y,Z) X je formule tvaru ,Neg(Y,Z)’ Elem30(X,W,Y,Z) X je formule tvaru ,Impl(W,Y,Z)’ Elem31(X,Y,Z) X je formule tvaru ,Disj(W,Y,Z)’ Elem32(X,Y,Z) X je formule tvaru ,Kvant(W,Y,Z)’ ... pro k>32: Elemk(X,Y1, ...Yi) X je formule tvaru ,Elem k-16(Y1, ...Yi)’ přičemž Elemk je vždycky o 1 více-místný než Elemk-16. Kromě těch bude jazyk nového systému obsahovat ještě predikáty JePravdiváZS2, JeDokazatelnáZS2 a JeKódZS2. Ke každému termu t a ke každé formuli φ pak obdobně jako u systému ZS1 definujeme formuli ψt(X), resp. ψφ(X), která říká, že X je term t, resp. formule φ (u bodů, které se liší od těch u ZS1, je plný puntík):
Jestliže t je proměnná y, pak ψt je formule Prom1(X,y). Podobně pro velké proměnné a pro konstantu.
◦ Jestliže t je term tvaru ,S(t1)’, pak ψt je formule ,Y(Fun1(X,Y) ψt1(Y))’. ◦ Jestliže t je term tvaru ,t1+t2’, pak ψt je formule ,Y Z (Fun2(X,Y,Z) ψt1(Y) ψt2(Z))’. Podobně pro funktor násobení.
Jestliže φ je tvaru ,t1=t2’, pak ψφ je formule ,Y Z (Elem1(X,Y,Z) ψt1(Y) ψt2(Z))’. Podobně pro ostatní atomické formule, kterých je teď nekonečně mnoho.21
◦ Jestliže φ je tvaru ,φ1’, pak ψφ je formule ,Y (Neg(X,Y) ψφ1(Y))’. ◦ Jestliže φ je tvaru ,φ1→φ2’, pak ψφ je formule ,Y Z (Impl(X,Y,Z) ψφ1(Y) ψφ2(Z))’. Podobně pro disjunkci. 21
Například, jestliže k>16 a formule φ je tvaru ,Elemk(t1,... tn)’, pak ψφ je formule
Y1,... Yn (Elemk+16(Y1,... Yn) ψt1(Y1) ... ψtn(Yn)).
33
Formalizace důkazu
◦ Jestliže φ je tvaru ,xk φ1’, kde xk je k-tá proměnná, pak ψφ je formule ,Z (Kvant(X,k,Z) ψφ1(Z))’. Axiomy nového systému by měly být obdobné jako u ZS1, jen mluvit o formulích tohoto systému a důkazech v něm místo v Peanově aritmetice. Systém, který nazvu ZS2, by měl tedy obsahovat: ◦ axiomy standardního kalkulu predikátové logiky a jeho odvozovací pravidla, aplikovatelná na formule se dvěma druhy proměnných ◦ axiomy Peanovy aritmetiky ◦ axiomy: X (ψφ(X) → JePravdiváZS2(X)) ↔ φ
pro každou formuli φ jazyka systému ZS2,
X (JeDokazatelnáZS2(X) → JePravdivá ZS2(X)), X (ψφ(X) ↔ JeKódZS2(n,X))
pro každou aritmetickou formuli φ a její kód n,
y (y(DůkZS2(y)) ↔ Y (JeKódZS2(y,Y) JeDokazatelnáZS2(Y))). Přitom aritmetická formule DůkZS2(x,y) by měla popisovat a vystihovat relaci „... je kód důkazu formule s kódem ... v ZS2“ při nějakém vhodně zvoleném kódování jazyka systému ZS2. Potíž je, že DůkZS2(x,y) má být sestrojena podle toho, jaké axiomy systém ZS2 obsahuje, přičemž má sama být obsažena v jednom z axiomů. Z toho, co bylo zatím řečeno, není proto jisté, že bude formule DůkZS2(x,y) pro nějaké kódování jazyka ZS2, a tedy výše popsaná množina axiomů, vůbec existovat.22 Předpokládejme na chvíli, že existuje nějaké takové kódování formulí ve výše popsaném jazyce, že relace „... je kód důkazu formule s kódem ...“ je rekurzívní a existuje systém ZS2, jak jsme ho popsali.
Důkaz sporu v hypotetickém ZS2 Stejně jako v Peanově aritmetice by šlo v ZS2 dokázat formuli ,DokZS2(n) → DokZS2(m)’, jestliže n by byl kód Gödelovy formule pro ZS2 (tedy DokZS2(n)) a m kód formule ,0≠0’. ZS2 by ale „věděl“, že podmínka DokZS2(m) je ekvivalentní podmínce dokazatelnosti formule s kódem m, tedy formule ,0≠0’, a že z dokazatelnosti formule plyne její pravdivost. Proto by v něm (stejným způsobem jako obdobná formule v ZS1) byla dokazatelná formule DokZS2(m), a tedy i DokZS2(n). Ovšem potom DokZS2(n), a proto by z Peanových axiomů (a tedy i v ZS2) byla dokazatelná formule DokZS2(n). A to je kýžený spor.
22 Dalo by se očekávat, že formule Důk ZS2 bude obsahovat nějaký popis axiomu, v němž se má vyskytovat, který bude mít délku přinejlepším srovnatelnou s délkou tohoto axiomu. Ovšem vzhledem k tomu, že o kódování jazyka ZS2 a způsobu sestrojení formule DůkZS2 se zatím nic neřeklo, není to jisté.
34
Formalizace důkazu
Proč by ZS2 byl sporný? Kdyby existoval formální systém ZS2, byl by sporný. To se může zdát zarážející díky tomu, že systém ZS2 na první pohled neříká nic špatného: o všech jeho axiomech kromě axiomu tvrdícího pravdivost v něm dokazatelných formulí bychom se mohli přesvědčit, že jsou pravdivé. Protože ZS2 by byl sporný, musel by pak být nepravdivý axiom X (JeDokazatelnáZS2(X) → JePravdivá ZS2(X)). Z toho se zdá, jako by spornost hypotetického systému ZS2 spočívala v tom, že tvrdí pravdivost v sobě dokazatelných formulí, což se ale od „rozumného“ formálního systému dá očekávat – zjistíme-li o nějakém matematickém tvrzení, že je dokazatelné, nepochybujeme přece o tom, že je pravdivé. Důvod spornosti hypotetického ZS2 se proto dá vidět už v tom, že ZS2 toho „ví“ příliš mnoho o dokazatelnosti v sobě samém. Odpověď na otázku: „Proč není v bezesporném systému dokazatelná Gödelova formule?“ by pak mohla být: „Protože abychom mohli dokázat Gödelovu formuli, potřebovali bychom formální systém, který toho „ví“ dost o dokazatelnosti v sobě samém, kvůli čemuž bude sporný.“ Myslím, že k posouzení, nakolik je taková odpověď uspokojivá, bude užitečné připomenout si smysl našeho zkoumání. Na otázku, proč není jistá pravdivá formule v určitém bezesporném systému dokazatelná, už máme od Gödela jednu odpověď: protože z její dokazatelnosti by plynula spornost systému. Tím otázku zodpovídáme jakoby z toho úhlu pohledu, z jakého se na věc díváme, tvrdíme-li, že v každém dostatečně silném formálním systému (takovém, v němž jsou dokazatelné Peanovy axiomy a jistá pravdivá aritmetická formule) je toho dokazatelného příliš mnoho, totiž spor. Nezodpovídáme ji ale z toho úhlu pohledu, z jakého se na věc díváme, říkáme-li, že v každém bezesporném, „rekurzívně popsatelném“ systému je toho o přirozených číslech dokazatelného příliš málo. Dosud jsme možná učinili pokrok v porozumění problému z první stránky: trošku jsme upřesnili, co by mohlo znamenat, že toho systém dokáže příliš mnoho, totiž že „ví“ příliš mnoho o dokazatelnosti v sobě samém. Myslím, že pro porozumění problému z této stránky bude užitečné, vyjasnit, jak z vědění o dokazatelnosti v sobě samém vzniká spor a v jakém smyslu se dá mluvit o tom, co formální systém „ví“, a vůbec o čem dokáže mluvit. Dalo by se říct, že zkoumání přineslo určitý pokrok v porozumění problému z druhé stránky: ukázalo se, že není jednoduché najít formální systém, jehož axiomy by popisovaly vše, co je potřeba k formálnímu důkazu vědět. První problém byl, najít k teorii Θ takovou formuli φ, že by byla Gödelovou formulí pro nově vzniklou teorii, Θ {φ}, tedy γΘ {φ}. Druhý problém byl, najít k systému ZS2 axiom obsahující formuli, která popisuje relaci DůkZS2. Naštěstí axiom, který jsme se pokoušeli najít, vyjadřuje tvrzení, jež se nepovažuje za samozřejmé – je v podrobném důkaze dál zdůvodňováno, a formální systém umožňující podrobnější zachycení důkazu by tento axiom nemusel obsahovat. K lepšímu pochopení problému z téhle stránky by proto mohlo pomoci, pokusit se formalizovat důkaz podrobněji. Celkově se dá říct, že cesta k oboustrannému porozumění problému se zdá být, přesněji charakterizovat systém, v němž bychom uměli Gödelovu větu dokázat. Nejdřív se pokusím vyjasnit, jak z vědění o dokazatelnosti v sobě samém vzniká spor a v jakém smyslu se dá mluvit o tom, co formální systém „ví“. Pak se pustím do dalšího pokusu o formalizaci. Úplně stranou přitom zůstává otázka, zda k důkazu tvrzení o přirozených číslech vyjádřitelného aritmetickou formulí skutečně potřebujeme mluvit o něčem jiném než o nich, a pokud ano, proč.
35
Formalizace důkazu
Obrázek 3.1, který jsem si vypůjčil z internetové stránky Johna Case (viz [2]).23
Kruhovost a spor Pokusím se na několika příkladech přiblížit, jak z kruhovosti vzniká spor. Jestliže větu Věta A je nepravdivá. nazveme A, dostaneme větu, o níž jsme schopni ukázat, že je pravdivá a zároveň nepravdivá. To, že vyvstává paradox, by se dalo zdůvodnit asi takhle: Představujeme si, že je tu na jedné straně něco, o čem mluvíme, a na druhé straně tvrzení, která o tom vypovídají. Pravdivost těchto tvrzení je pak jednoznačně určena tím, o čem se mluví. Jenže pokud pravdivost tvrzení je jednou z věcí, o kterých se mluví, je pravdivost tvrzení určována pravdivostí tvrzení. Pokud je pravdivost některého tvrzení určována opačně, než jaká by byla, ať by byla jakákoli, je toto tvrzení paradoxní – pravdivé, pokud nepravdivé, a nepravdivé, pokud pravdivé.24
Překvapení může pocházet z toho, že to, o čem se mluví, a tvrzení, která o tom vypovídají, si představujeme jako oddělené jedno od druhého, a pravdivost všech tvrzení jako určovanou jedním a ne druhým, a proto neproblematickou. Všimněte si, že robot si nevidí na dráty k očím. To by mohlo být podstatné. Jestliže je pravdivost věty naopak určována jako tatáž, ať je jakákoli, není určena jednoznačně. To bude podobné i u dalších příkladů.
23 24
36
Formalizace důkazu
Dalším příkladem může být paradox lodního holiče: lodní holič je člověk, který holí každého na lodi, kdo se neholí sám. Lodní holič pak holí sám sebe právě tehdy, když se neholí, což je pro každého nesplnitelný úkol, pročež žádná loď nemá lodního holiče. Problém, který má adept na lodního holiče, jde popsat takto: můžeme si představit, že úkol lodního holiče je určen stavem věcí na lodi – podle toho, kdo na lodi se neholí, se určí, koho má lodní holič holit. Jenže stav věcí na lodi je současně určován tím, jaký je úkol holiče, protože holič – jeden z lidí na lodi – se oholí nebo neoholí podle toho, co je mu uloženo. Paradox vzniká, když je úkol holiče určován opačně, než jaký by byl, ať by byl jakýkoli. Blíž k matematice má paradoxní vlastnost čísel, s níž podobnou jsme se setkali dříve: „být číslem, které nelze definovat méně než deseti slovy“. K paradoxu dospějeme, pokud budeme předpokládat nejmenší číslo s touto vlastností, to totiž, protože ji má, ji současně nemá. Paradox nás může zaskočit, jestliže si představujeme, že je definováním vlastnosti jednoznačně určené, které číslo danou vlastnost má a které nikoli – díky tomu, že některá čísla s pomocí nejvýše deseti slov definovat lze a jiná nikoli. Jenže to, která čísla jde definovat s pomocí nejvýše deseti slov, je zase určováno tím, která mají tuto vlastnost – můžeme totiž definovat číslo jako nejmenší s touto vlastností. Paradox pak vzniká, když je tato vlastnost definicí určována jinak, než jaká by byla, ať by byla jakákoli (v našem případě ji jisté číslo má právě tehdy, když ji nemá). Jestliže by spornost formálního systému, který by umožnil formalizovat důkaz Gödelovy věty, byla způsobena tím, že toho „ví“ příliš mnoho o dokazatelnosti v sobě, měli bychom se podívat na to, jaký je problém s pojmem dokazatelnosti v sobě samém. Označme následující výrok V: Výrok V není dokazatelný. Předpokládejme, že V je nepravdivý. Pak je ale, vzhledem k tomu, co říká, dokazatelný, a tedy pravdivý. Tím jsme dokázali, že výrok V je pravdivý. Potom ale není dokazatelný – jak je tedy možné, že jsme ho dokázali? Nebo také: předpokládejme, že výrok V je dokazatelný. Pak je ale pravdivý. Tedy není (vzhledem k tomu, co říká) dokazatelný. Tím jsme dokázali, že výrok V není dokazatelný – to jsme ale dokázali výrok V! Má-li formální systém být bezesporný, nemůže umožnit odvození odpovídající předchozím úsudkům. K učinění předchozích úvah ovšem stačilo vědět, co výrok tvrdící svoji nedokazatelnost říká, a počítat s tím, že co je dokazatelné, je pravda – což je ovšem něco, co činí dokazatelnost dokazatelností. Zdá se tedy, že bezesporný systém, který věří, že ze dvou opačných tvrzení je vždy jedno pravdivé a druhé nepravdivé (že buď φ anebo φ), skutečně nemůže být schopný mluvit o dokazatelnosti v sobě samém. Příčinu paradoxu bychom mohli, podle vzoru předchozích příkladů, popsat takto: předpokládáme, že dokazatelnost nebo nedokazatelnost výroku je dána nějakými našimi pevně určenými schopnostmi dokazování, tedy nezávisle na procesu dokazování. K čemu lze v procesu dokazování dospět, je pak určeno tím, zda má výrok vlastnost dokazatelnosti. Jenže vlastnost dokazatelnosti je zase určována tím, k čemu v procesu dokazování dospíváme – dokážeme-li jej, je dokazatelný. Paradox vzniká, jestliže je vlastnost dokazatelnosti výroku určována opačně, než jaká by byla, ať by byla jakákoliv. Jestliže neschopnost bezesporného systému dospět k jisté pravdivé aritmetické formuli je dána jeho neschopností mluvit o dokazatelnosti v sobě samém, bylo by dobré popsat přesněji, co to vlastně znamená.
37
Formalizace důkazu
O čem (mlu)ví formální systém O významu výrazů v jazyce formálního systému se dá mluvit přinejmenším v dvojím smyslu: ◦ může se myslet standardní význam výrazů daného jazyka či význam, který se výrazům rozhodneme přidělit. V takovém smyslu se mluví například o tom, jaké tvrzení která aritmetická formule vyjadřuje. Význam se pak nijak nevztahuje k dokazovacím schopnostem toho kterého formálního systému. ◦ může se myslet význam, který výrazům nějak dodají axiomy a odvozovací pravidla formálního systému. Takový význam pak nemá nic společného s tím, jak tyto výrazy standardně čteme a dá se o něm mluvit jen ve vztahu k tomu kterému formálnímu systému, teorii nebo případně kalkulu (k poslednímu např. u významu logických spojek). Jestliže máme charakterizovat, o čem kalkul dokáže mluvit nebo kolik toho o čem „ví“, můžeme tak učinit s ohledem na to, jak se jeho výrazy rozhodneme číst. Například formální systém tvořený standardním kalkulem a axiomem JePravdiváFormule(g) ↔ JeVeMněDokazatelnáFormule(g) pak v tomto smyslu umí mluvit o dokazatelnosti formulí v sobě samých a „ví“, že formule g je pravdivá právě tehdy, když v něm není dokazatelná (tedy pokud výrazy čteme tak, jak nás poprvé napadne). Ve svých dokazovacích schopnostech se ale podstatně neliší třeba od formálního systému tvořeného kalkulem a axiomem JeLiché(1) ↔ JeSudé(1), díky čemuž můžeme říct, že je bezesporný – což bychom možná od systému, který „ví“ o existenci formule tvrdící svoji nedokazatelnost v něm samém, nečekali. Zdá se proto, že charakterizovat systém z hlediska toho, o čem dokáže mluvit nebo o čem „ví“, by bylo dobré nezávisle na tom, jaké významy jeho výrazům standardně přidělujeme. Na druhou stranu, nenapadá mě, jak bychom mohli popsat, o čem systém mluví nebo co „ví“, aniž bychom to nějak porovnali s tím, o čem mluvíme my nebo co víme. Například, o Peanově aritmetice můžeme říct, že dokáže mluvit o aritmetice přirozených čísel díky tomu, že funkce v ní označené ,+’ a ,∙’ se tu v lecčems chovají stejně jako sčítání a násobení. Taky můžeme prohlásit, že toho „ví“ dost o rekurzívních relacích, díky tomu, že každou rekurzívní relaci popisuje nějaká aritmetická formule, která ji zároveň v Peanově aritmetice vystihuje (ve smyslu, v jakém jsem toto slovo používal výše). Totéž bychom mohli říct o systému, který by z Peanovy aritmetiky vznikl třeba záměnou symbolů ,+’ a ,∙’ za ,-’ a ,/’. Naopak o systému, jehož axiomy bych nedokázal přečíst jako pravdivá tvrzení o čemkoli (o odvozovacích pravidlech nemluvě), bych vůbec nebyl schopný říct, o čem dokáže mluvit nebo co „ví“. Z toho se zdá, že charakterizovat, o čem dokáže formální systém mluvit, bychom mohli podle toho, zda jeho výrazům dokážeme přiřadit takový význam, aby se systém „choval“ tak, jako by jim rozuměl, přesněji řečeno: aby se význam, který výrazům dodávají axiomy a odvozovací pravidla daného systému, dostatečně shodoval s významem, který jim přiřazujeme. Zůstává samozřejmě otázka, jak určit význam, který je dán axiomy a odvozovacími pravidly, jak porovnávat, nakolik se význam takto určený shoduje s významem, který se rozhodneme výrazům přiřadit, a vůbec nakolik jsme schopní učinit námi přidělovaný význam předmětem našeho zkoumání. Kvůli tomu se může zdát formální charakterizace systému z hlediska toho, o čem dokáže mluvit, zcela nedosažitelná. Naštěstí existuje osvědčený způsob, jak tak tajemnou věc, jakou je význam, učinit předmětem seriózního zkoumání, a to skrze to, čemu se připisuje pravdivost.
38
Formalizace důkazu
Naše používání aritmetických výrazů
Kalkul a Peanovy axiomy
určují
Význam našich aritmetických výrazů směr zkoumání
určují
?? ??
Význam výrazů v Peanově aritmetice směr zkoumání
umíme porovnat
Pravdivá tvrzení o přirozených číslech
Formule dokazatelné v Peanově aritmetice e Obrázek 3.2: Význam aritmetických výrazů
Nakolik se shoduje význam, který výrazům přiřadíme, s významem, který jim dodává formální systém, se dá nyní posoudit podle toho, nakolik se pravdivost tvrzení, která vyjadřují jisté formule, shoduje s dokazatelností těchto formulí v daném systému. O čem formálním systém dokáže mluvit, se pak dá posoudit podle toho, zda je v něm dokazatelných dostatečně mnoho formulí, které vyjadřují – při nějakém jejich čtení – pravdivá tvrzení. Přitom toto „čtení“ nemusí být jen přiřazením (snadno popsatelných) významů jednotlivým symbolům – mohou být přiřazeny významy termům (jménům) nebo formulím, jejichž částem odpovídající význam přiřadit neumíme. Gödel ukázal, jak některé aritmetické formule číst jako tvrzení o důkazech formulí v některém formálním systému tak, aby dostatečně mnoho takových pravdivých tvrzení bylo dokazatelných. V tomto smyslu tedy ukázal, že některé formální systémy dokážou mluvit o důkazech v sobě samých. Z hlediska zkoumání toho, čemu formální systém „rozumí“ a co „ví“, má takový postup tu nevýhodu, že se při něm zcela zanedbává proces dokazování – způsob, jakým systém k dokazatelným formulím dospívá – který není v pravdivosti takových formulí, jež nemluví (při daném přiřazení jim významu) o dokazování v tomto systému, nijak obsažen. Pak třeba nedokážeme vůbec rozlišit, čemu daný systém „nerozumí“ a o čem toho dost „neví“,25 kteréžto intuitivní rozlišení můžeme provést třeba, když prozkoumáme jeho axiomy a odvozovací pravidla (a které jsem činil u ZS1 a ZS2). Proto budu dál zkoumat jen to, o čem formální systém dokáže mluvit.
Snaha o formální vymezení intuitivních pojmů Řekli jsme, že formální systém je sporný, jestliže umí mluvit o dokazatelnosti v sobě samém. Nyní se můžeme pokusit vyjádřit tuto podmínku (nebo alespoň nějakou, splněnost jíž ze splněnosti této vyplývá) formálněji:
25
To naštěstí neplatí u lidí – můžeme se například ptát: „proč si myslíš, že ...?“
39
Formalizace důkazu
Nechť formální systém T splňuje toto: 1.
T obsahuje pravidlo modus ponens (odloučení) a jsou v něm dokazatelné všechny formule, které vzniknou dosazením formulí jazyka T za výrokové proměnné ve výrokových tautologiích.26
2.
existuje takové přiřazení f, které každé formuli z některé množiny formulí jazyka systému T přiřadí nějaké tvrzení tak, že ke každé formuli φ jazyka systému T existují takové formule ψ1 a ψ2, že f(ψ1)=„Formule φ je v T dokazatelná“ a f(ψ2)=„Formule φ není v T dokazatelná.“
3.
pro každé formule φ, ψ1 a ψ2 platí, že jestliže f(ψ1)=„Formule φ je v T dokazatelná“ a f(ψ2)=„Formule φ není v T dokazatelná.“, pak je v T dokazatelná formule tvaru ,ψ2↔ψ1’.
4.
jestliže je formule φ v T dokazatelná, pak každá formule ψ taková, že f(ψ)=„Formule φ je v T dokazatelná“, je v T dokazatelná.
Pak ◦
o systému T a přiřazení f budu říkat, že T mluví při f o dokazatelnosti v T. Přiřazení f budu říkat čtení formulí z .
◦
o systému T, množině a přiřazení f budu říkat, že formule z mluví v systému T při f o dokazatelnosti v něm. konečně, jestliže f(φ) je pravdivé tvrzení, budu říkat, že φ je při f pravdivá.
◦
První podmínce bychom mohli říkat podmínka, aby dotyčný systém „uměl“ (aspoň trochu) logicky usuzovat, druhé podmínka relevantního čtení formulí a třetí a čtvrté podmínky, aby systém „rozuměl“ formulím při daném čtení.27
Jazyk systému T tedy obsahuje výrokové spojky. Požadavek, který klade definice, bychom mohli považovat za nepřijatelně mírný: formální systém například nemusí ani „vědět“, že z dokazatelnosti formule plyne existence jejího důkazu, nemusí ani být schopen při daném čtení samotnou formuli „pojmenovat“. Jde o to, že už splnění podmínek kladených definicí zaručuje, že formální systém dokáže provést některá odvození odpovídající úsudkům, které jsou z hlediska současného zkoumání zajímavé, a jejichž proveditelnost bychom mohli u každého formálního systému, který o formální dokazatelnosti dokáže v intuitivním smyslu mluvit, očekávat. Požadavek kladený definicí (konkrétně v bodě 4.) se dá vidět i jako příliš přísný: systém by nás mohl přesvědčit, že mluví o dokazatelnosti v T, i když všechny formule dokazatelné v T za dokazatelné „nemá“, třeba kdyby o všech 1 000 000 formulích, které mají důkaz ne delší než 1 000 000 , „věděl“, že jsou dokazatelné. 26 27
40
Formalizace důkazu
Jestliže T je formální systém a f je čtení formulí jazyka systému T z množiny a existují takové formule φ a ψ, že f(ψ)=„Formule φ není v T dokazatelná.“ a v T je dokazatelná ekvivalence φ ↔ ψ, budu říkat, že v T existuje při f kritická autoreferenční formule φ z množiny . Prozatím můžeme vyslovit větu: Nechť systém T je bezesporný a mluví při čtení f formulí z množiny o dokazatelnosti v T. Nechť v T existuje existuje při f kritická autoreferenční formule φ z . Pak φ je při f pravdivá a v T není dokazatelná. Důkaz: Nechť pro formule φ a ψ platí, že f(ψ)=„Formule φ není v T dokazatelná.“ a v T je dokazatelná ,φ ↔ ψ’. Předpokládejme, že formule φ je v T dokazatelná. Pak podle podmínky 1. je v T dokazatelná i formule ψ, podle podmínky 2. existuje formule χ taková, že f(χ)=„Formule φ je v T dokazatelná“, a podle podmínky 4. je χ v T dokazatelná. Podle podmínky 3. je ale dokazatelná formule tvaru ,χ.↔ ψ’, a proto, podle podmínky 1., i formule ψ a φ. Z předpokladu, že v T je dokazatelná formule φ, jsme tedy dospěli k tomu, že T je sporný. Proto formule φ není v T dokazatelná, a tedy je při f pravdivá. □ O systému, ke kterému existuje formule v jeho jazyce, jež je při čtení f pravdivá, avšak v tomto systému nedokazatelná, budu říkat, že je vzhledem ke čtení f neúplný. Gödelovi se podařilo k Peanově aritmetice najít takové čtení aritmetických formulí, že Peanova aritmetika28 při tomto čtení mluví o dokazatelnosti v Peanově aritmetice, existuje při něm kritická autoreferenční formule a navíc jsou formule (z příslušné množiny) při tomto čtení pravdivé právě tehdy, když jsou pravdivé při jejich standardním čtení – tedy když jsou to pravdivé aritmetické formule. Proto existuje pravdivá, avšak v Peanově aritmetice nedokazatelná aritmetická formule. Množina výše označená jako je tu množina aritmetických formulí DokPA(n) a ,DokPA(n)’, kde n je kód nějaké formule, a ono čtení, které nazvu f, je takové, že pro každou formuli φ a její kód n je f(DokPA(n))=„Formule φ je v Peanově aritmetice dokazatelná“ a f(,DokPA(n)’)=„Formule φ není v Peanově aritmetice dokazatelná.“ Na předchozí definici by nás mohlo zarazit, že podle ní může formální systém T mluvit o dokazatelnosti v T, aniž by byl sporný (což je třeba případ Peanovy aritmetiky). Přitom se výše prohlašovalo, že formální systém, který by v intuitivním smyslu dokázal mluvit o dokazatelnosti v sobě samém, by byl sporný. Neshoda by mohla pramenit z toho, že definice se vztahuje i na systémy, v nichž není možné provést některá podstatná logická odvození – vyžadují se jen „znalosti“ výrokové logiky. Další věc je, že pro systém, o kterém mluví definice, nemusí (podle toho, co bylo zatím řečeno) existovat kritická autoreferenční formule. Ani jedno ale neplatí o Peanově aritmetice, která je přesto bezesporná. 28
nahlížena teď ne jako množina axiomů, ale jako formální systém tvořený Peanovými axiomy a kalkulem
41
Formalizace důkazu
Háček je v tom, že formální systém – nazvěme ho T – může mluvit o dokazatelnosti v T, aniž by „věděl“, že mluví o dokazatelnosti v sobě samém. Spor ovšem, pokud víme, nevzniká z pojmu dokazatelnosti v T, ale s pojmu dokazatelnosti v sobě samém, jak jsem se pokusil ukázat výše. Zkusím proto formálněji popsat, kdy formální systém mluví o dokazatelnosti v sobě samém a „ví“ o tom: Nechť formální systém T mluví při čtení f o dokazatelnosti v T a pro všechny formule φ a ψ platí: jestliže f(φ)=„Formule ψ je v T dokazatelná“, pak v T je dokazatelná formule tvaru ,φ→ψ’ (tedy z tvrzení, že ψ je dokazatelná, umí T usoudit ψ). V takovém případě budu říkat, že T mluví při f vědomě o dokazatelnosti v sobě samém. Peanova aritmetika nyní dokáže mluvit o dokazatelnosti v sobě samé, ale ne vědomě: z tvrzení, že φ je v ní dokazatelná (při libovolném čtení, při kterém mluví o dokazatelnosti v sobě samé), neodvodí φ. Nakonec můžeme vyslovit větu: Nechť systém T mluví při čtení f formulí z množiny vědomě o dokazatelnosti v sobě samém a nechť v něm existuje při f kritická autoreferenční formule z . Pak T je sporný. Důkaz: Kritickou autoreferenční formuli z nazvěme φ. Pro nějakou formuli ψ pak platí, že f(ψ)=„Formule φ není v T dokazatelná“ a v T je dokazatelná ekvivalence ,φ ↔ ψ’. Podle podmínky 2. existuje taková formule χ, že f(χ)=„Formule φ je v T dokazatelná“. Podle podmínky 3. je v T dokazatelná ekvivalence ,ψ↔χ’, podle podmínky 5. je v T je dokazatelná implikace ,χ→φ’. Podle podmínky 1. jsou proto postupně dokazatelné i ,χ→χ’ ,χ’, φ. O formuli φ ale víme z předchozí věty (díky tomu, že T mluví při f o dokazatelnosti v T), že není v T dokazatelná, jestliže je bezesporný. Systém T je tedy sporný. □ O bezesporných formálních systémech nyní víme, že při žádném čtení jejich formulí nemluví vědomě o dokazatelnosti v sobě samých, jinými slovy – popisuje-li výše uvedená definice skutečně nutnou podmínku pro připsání schopnosti vědomého mluvení o dokazatelnosti v sobě samém, jak jí intuitivně rozumíme – při žádném způsobu čtení jeho formulí jako tvrzení o dokazatelnosti v něm se systém nechová tak, jako by jim rozuměl. Formální systém, který by umožňoval formalizovat náš důkaz Gödelovy formule pro něj samý, má být tohohle schopný, a přitom být bezesporný, což se ukázalo jako nemožné. Když se takový systém pokoušíme sestrojit tím, že dodáváme jeho axiomy, narážíme na tuto nemožnost z druhé strany: nejsme schopni najít takové axiomy, které by vyjadřovaly (při jejich zamýšleném čtení) podstatná pravdivá tvrzení v jeho jazyce.
42
Formalizace důkazu
FORMALIZACE PODRUHÉ Protože neformální důkaz Gödelova výroku bychom měli být schopni krok po kroku popsat, měli bychom k němu využít jen nějaké konečné množství zřejmých tvrzení nebo jasných výchozích principů. Jde nyní o to, zjistit, které buď nedokážeme v jazyce logiky vyjádřit, anebo je z nějakého důvodu může oprávněně využít jen někdo, kdo není formální systém, pro který tvrzení dokazujeme.
Struktura důkazu pro konkrétní systém Důkaz pravdivosti Gödelovy formule pro konkrétní systém se dá rozdělit na dvě části: ◦ důkaz Gödelovy věty pro tento systém, neboli důkaz tvrzení, že pokud je tento systém bezesporný, je Gödelova formule pro něj pravdivá a není v něm dokazatelná. ◦ důkaz bezespornosti tohoto systému. Důkaz Gödelovy věty pro určitý systém T lze provést takto: 1. Najít vhodné kódování formulí jazyka tohoto systému a důkazů v něm. 2. Najít aritmetickou formuli DůkT(x,y) a o ní dokázat, že popisuje relaci „... je kód důkazu formule s kódem ... v tomto systému“ a vystihuje ji tu – tedy dokázat korespondenční lemma pro relaci „... je kód důkazu formule s kódem ... v systému T“ a formuli DůkT(x,y). 3. Sestrojit takovou formuli, která je v daném systému dokazatelně ekvivalentní formuli tvaru ,x DůkT(n)’ a její kód je n. O této formuli dokázat, že není v daném systému za předpokladu jeho bezespornosti dokazatelná, a tedy je pravdivá. Důkaz bezespornosti některých systémů, jejichž důkazy jsou posloupnosti formulí, umíme provést takto: 1. Dokázat, že všechny důkazy délky 1 jsou důkazy pravdivé formule. Např. u Peanovy aritmetiky to znamená ověřit, že její axiomy vyjadřují pravdivá tvrzení o přirozených číslech. 2. Dokázat, že pokud všechny důkazy délky n jsou důkazy pravdivé formule, pak i všechny důkazy délky n+1 jsou důkazy pravdivé formule. Např. u Peanovy aritmetiky se využije toho, že prvních n členů důkazu délky n+1 tvoří zase nějaký důkaz, a ověří se, že odvozovací pravidla standardního kalkulu zachovávají pravdivost.
Formální systém ZS3 Hledaný systém můžeme předběžně rozdělit na několik částí: a. logický aparát b. axiomy vystihující poznatky o přirozených číslech a posloupnostech (viz. část „O čem se v důkaze mluví“ na začátku kapitoly) c. axiomy popisující pravdivost formulí v jazyce tohoto systému d. axiomy popisující kódování formulí v jazyce tohoto systému e. axiomy popisující dokazatelnost v tomto systému Systém necháme „považovat“ formule za posloupnosti čísel, s nimiž se formule nejdřív ztotožňují (nikoli za samotná čísla, která už budou kódy formulí). Části a. a b. pak může tvořit nějaký systém, který toho „ví“ dost o přirozených číslech a posloupnostech jimi tvořených, případně obohacený o odpovídající definice jmenné konstanty 0, funktorů S, + a ∙ a predikátů > a ≥. Takový systém může být například Zermelo-Fraenkelova teorie množin (dále jen ZF; nahlížená jako systém tvořený množinou axiomů a kalkulem), kde jsou čísla i jejich posloupnosti označovány stejným druhem proměnných - množinovými.
43
Formalizace důkazu
Zbývá určit axiomy tvořící poslední tři části. Díky tomu, že formule jsou ztotožněny s posloupnostmi čísel, o nichž formule v jazyce daného systému umějí mluvit, nebude potřeba dodávat další predikáty pro popis formulí, jak to bylo u ZS1 a ZS2. c. Ke každé formuli můžeme definovat formuli ψφ, která ji popisuje, podobně jako u předchozích systémů. Ke každé formuli φ tu pak bude axiom: x (ψφ(x) → JePravdiváZS3(x)) ↔ φ, kdy v oboru proměnnosti proměnné x jsou všechny konečné posloupnosti čísel. d. Dodáme axiom definující odpovídajícím způsobem predikát JeKódZS3 (jestliže kódování formulí čísly bude zvoleno podobně, jak jej zvolil Gödel, neměl by být problém formuli popisující toto kódování sestrojit). e. Konečně axiom popisující dokazatelnost by měl říkat: Pro každou formuli φ platí, že φ je dokazatelná právě tehdy, když pro nějaké číslo n existuje konečná posloupnost formulí, která má délku n, její poslední člen je φ a pro každou formuli ψ1 v posloupnosti platí: ψ1 je buď axiom vytvářeného systému, nebo existuje formule ψ2 taková, že ψ2 předchází v posloupnosti ψ1 a ψ1 je z ψ2 odvozena generalizací, nebo existují formule ψ2 a ψ3 takové, že obě předcházejí v posloupnosti ψ1 a ψ1 je y formulí ψ2 a ψ3 odvozena s pomocí modu ponens. To bychom mohli symbolicky zapsat: x(JeDokazatelnáZS3(x) ↔ kz(PosloupnostDélky(z,k) Člen(x,k,z) yj(Člen(y,j,z) → JeAxiomZS3(y) v l (Člen(v,l,z) k≥l OdvozenaGeneralizací(y,v)) v w l m (Člen(v,l,z) Člen(w,m,z) k≥l k≥m OdvozenaMP(y,v,w)))), kde v oboru proměnných v,w,x a y mají být všechny konečné posloupnosti čísel (formule), v oboru proměnné z mají být konečné posloupnosti těchto posloupností (důkazy) a v oboru proměnných j, k, l, m mají být přirozená čísla a zkratkovitě zapsané formule by měly říkat toto: Formule PosloupnostDélky(z,k) Člen(x,k,z) JeAxiomZS3(x) OdvozenaGeneralizací(x,v) OdvozenaMP(x,v,w)
Má říkat z je posloupnost o délce k x je k-tý člen posloupnosti z x je axiom vytvářeného systému x je z v odvozena aplikací pravidla generalizace x je z v a w odvozena aplikací modu ponens
Přitom formule JeAxiomZS3(y), popisující množinu axiomů vytvářeného systému, by sama měla být podformulí jednoho z nich. Jestliže bychom měli takovou formuli sestrojit „nejpřímočařeji“ – tak, abychom při jejím čtení poznali, jakou množinu formulí (či posloupností čísel) popisuje – dá se očekávat, že by taková formule byla delší než každý z axiomů. Mohli bychom se ale pokusit nahradit „přímočarý“ popis axiomů formulí, z níž by systém množinu svých axiomů „poznal“: najít takovou formuli, o které by bylo v daném systému (zatím bez hledaného axiomu) dokazatelné, že je ekvivalentní výše popsané formuli, kterou bychom chtěli přidat jako axiom.
44
Formalizace důkazu
Systém, jehož části a. až d. jsou vytvořeny popsaným způsobem ze systému ZermeloFraenkelovy teorie množin, označím ZS3–. Systém ZS3 by pak měl vzniknout přidáním axiomu popisujícího – ačkoli možná ne „nejpřímočařeji“ – dokazatelnost v ZS3. Zkusím nyní zjistit, jestli takový axiom existuje.
Existuje systém ZS3? Pro lepší přehlednosti budu dále zapisovat formuli tvaru x(JeDokazatelnáZS3(x) ↔ kz(PosloupnostDélky(z,k) Člen(x,k,z) yj(Člen(y,j,z) → φ v l (Člen(v,l,z) k≥l OdvozenaGeneralizací(y,v)) v w l m (Člen(v,l,z) Člen(w,m,z) k≥l k≥m OdvozenaMP(y,v,w)))) ještě zkráceněji x(JeDokazatelnáZS3(x) ↔ (... φ ...)). Přitom je potřeba dát si pozor na to, že případné volné proměnné x, y, z, j nebo k ve formuli φ se tu stanou vázanými. Předpokládejme, že by existovala taková formule, kterou označím ψ, že by v ZS3– byla dokazatelná ekvivalence ψ ↔ x(JeDokazatelnáZS3(x) ↔ (... JeAxiomZS3(y) ... )), kde formule JeAxiomZS3(y) by popisovala axiomy systému vzniklého přidáním ψ k ZS3– jako axiomu. Tím bychom dostali systém, v němž je dokazatelné totéž co v systému, jaký jsme popsali výše (ale o němž se neprokázalo, že existuje). Problém, zda existuje formule dokazatelně ekvivalentní nějaké, která popisuje množinu axiomů, jedním z nichž je ta první, se podobá problému, který vyřešil Gödel, totiž zda existuje formule, která je dokazatelně ekvivalentní nějaké, jež popisuje podmínku nedokazatelnosti té první. I v tomto případě platilo, že formule tvaru ,Dok(n)’ (která byla pravdivá tehdy, když formule s kódem n nebyla dokazatelná) má kód podstatně větší než n, a tedy nemůže existovat přímo formule s kódem n, která by byla tvaru ,Dok(n)’. Gödel ale dokázal rafinovanou konstrukcí sestrojit formuli s kódem n, která byla formuli ,Dok(n)’ dokazatelně ekvivalentní. Pokusím se vyřešit problém existence systému ZS3 podobně: nejdřív sestrojit vhodnou formuli φ(v,w), která by říkala, že v je kód axiomu v systému, který vznikne přidáním formule s kódem w jako axiomu k ZS3–. Potom obdobným postupem jako v důkazu věty o pevném bodě k této formuli najít takovou formuli ψ s kódem n, že by ekvivalence ψ ↔ x(JeDokazatelnáZS3(x) ↔ (... v(JeKódZS3(v,y) φ(v,n)) ... )) byla dokazatelná v ZS3–.29 Jeden rozdíl oproti formulím, o nichž mluví ve svém důkaze Gödel, je v jazyce: jazyk ZS3– obsahuje o čtyři predikáty víc než jazyk aritmetiky. I tak se ale dá (bez potíží) najít vhodné kódování, aby relace Drobný zádrhel je v tom, že predikát JeDokazatelnáZS3 nepatří do jazyka ZS3–, protože se v žádném z axiomů systému ZS3– nevyskytuje. To bychom mohli vyřešit třeba tak, že bychom do ZS3– přidali (jinak nepodstatný) axiom 29
x(JeDokazatelnáZS3(x) ↔ JeDokazatelnáZS3(x)).
45
Formalizace důkazu
„... je kód axiomu v systému, který vznikne přidáním formule s kódem ... k systému ZS3– jako axiomu“ byla rekurzívní (a dalo se proto použít korespondenční lemma k sestrojení formule φ) a relace „... je kód formule vzniklé dosazením do formule s kódem ... jména čísla ... za proměnnou y“ později umožnila dokázat větu o pevném bodu (tedy sestrojit odpovídající formuli Subst). Formuli, která popisuje a v ZS3– vystihuje první z nich, označím JeAxiomZS3-(v,w). Vezměme nyní formuli x(JeDokazatelnáZS3(x) ↔ (... v(JeKódZS3(v,y) JeAxiomZS3-(v,n)) ... )). K té bychom chtěli najít takovou formuli ψ s kódem n, že by platila ekvivalence ψ ↔ x(JeDokazatelnáZS3(x) ↔ (... v(JeKódZS3(v,y) JeAxiomZS3-(v,n)) ... )) a tato ekvivalence byla dokazatelná v systému ZS3–. To se dá provést obdobně, jako jsme sestrojili formuli ψ v důkazu věty o pevném bodu (formule ψ pak bude tvaru x(Subst(x,k,k) x(JeDokazatelnáZS3(x) ↔ (... v(JeKódZS3(v,y) JeAxiomZS3-(v,n)) ... ))) pro nějaké číslo k takové, že ψ vznikne z formule s kódem k dosazením termu k za nějakou proměnnou). Systém, který vznikne přidáním ψ jako axiomu k systému ZS3–, budu dále nazývat ZS3. V ZS3 je nyní dokazatelná formule x(JeDokazatelnáZS3(x) ↔ (... v(JeKódZS3(v,y) φ(v,n)) ... )). Díky tomu, že v ZS3 jde dokázat, že kódování je prostá funkce, je tu poslední formule dokazatelně ekvivalentní x(JeDokazatelnáZS3(x) ↔ (... JeAxiomZS3(y) ... )), kterážto (tedy jaká nějaká) původně měla být jeho axiomem.
Jak dokázat γZS3 v ZS3 Díky axiomům popisujícím pravdivost, kódování a dokazatelnost formulí v jazyce ZS3 a díky tomu, že ZF (a tedy i ZS3) toho „ví“ dost o přirozených číslech i jejich posloupnostech, je možné provést formální důkaz Gödelovy formule pro systém ZS3 za předpokladu jeho bezespornosti, tedy důkaz formule x(ψ,0≠0’(x) → JeDokazatelnáZS3(x)) → γPA, takřka přesně odpovídajícím způsobem jako neformální důkaz, který byl načrtnut v předchozí kapitole. Rozdíl je jen ve třech věcech: ◦
nemluví se o ztotožňování aritmetických formulí s posloupnostmi čísel: formule už tu jsou s posloupnosti čísel ztotožněny.
◦
korespondenční lemma se dokazuje pro jednu konkrétní relaci, totiž „... je kód důkazu formule s kódem ... v ZS3“, zkráceně DokZS3, vyjádřenou pak ve formálním důkaze formulí DokZS3(x,y).
◦
je potřeba provést důkaz ekvivalence formule sestrojené konstrukcí z věty o pevném bodě s formulí popisující „přirozeným způsobem“ dokazatelnost v ZS3.
V dosavadním důkaze se nevyužívají znalosti o číslech, jejich posloupnostech apod., které by „neměla“ třeba teorie ZF (např. znalost pravdivosti Gödelova výroku pro ZF), ani logické kroky, které by systém nebyl s to postihnout. K důkazu pravdivosti formule γZS3 ovšem zbývá formálně dokázat bezespornost systému ZS3. 46
Formalizace důkazu
Formální důkaz bezespornosti Neformálně můžeme dokázat bezespornost systémů jako je Peanova aritmetika a ZS1 tak, že ověříme pravdivost axiomů a to, že odvozovací pravidla pravdivost zachovávají. Přesněji řečeno, přidělíme symbolům tvořícím formule takový význam, aby tvrzení vyjadřovaná axiomy byla pravdivá a aby odvozovací pravidla pravdivost zachovávala.30 Matematickou indukcí podle délky důkazu z toho dokážeme, že všechna formálně dokazatelná tvrzení jsou pravdivá, a tedy nemůže být dokazatelný spor. Tentýž postup bychom mohli zkusit formalizovat při hledání důkazu bezespornosti ZS3 v něm samém. Přitom předem víme, že takový postup nebude pro ZS3 možné korektně provést. První krok důkazu spočívá v ověření pravdivosti axiomů. Pro každý axiom φ systému ZS3 je možné v ZS3 dokázat formuli x (ψφ(x) → JePravdiváZS3(x) díky tomu, že ZS3 obsahuje axiom x(ψφ(x) → (JePravdiváZS3(x)↔ φ)). K formalizaci prvního kroku bychom ale měli být schopni pro každou formuli – nazvu ji ψ(x) – která říká, že x je instancí některého schématu ZS3, např. schématu A → (B → A), dokázat formuli x(ψ(x) → JePravdiváZS3(x)). Nepřipadá mi ale zřejmé, jak bychom tohle mohli v systému ZS3, kde je pravdivost formulí definována pro každou formuli zvlášť, provést: zdá se, jako by systém ZS3 „nerozuměl“ platnosti schémat, nýbrž jen „věděl“ o pravdivosti jejich jednotlivých instancí – jinak řečeno, „nerozuměl“ obecné souvislosti mezi pravdivostí libovolné formule φ1 a formule tvaru ,φ2 → φ1’, nýbrž „věděl“ jen, že za předpokladu pravdivosti určité formule φ1 je pravdivá i jistá formule tvaru ,φ2 → φ1’. Podobný problém jako se schématy je i s odvozovacími pravidly. Není to ale problém nepřekonatelný v tom smyslu, že můžeme přidat k systému axiomy, které tvrdí pravdivost určitých typů formulí. Například, jestliže by formule, kterou zapíšu JeImpl(x,y,z), říkala, že formule x je tvaru ,y→z’, pak by systém mohl obsahovat axiom tvaru: x y z (JeImpl(x,y,z) → (JePravdiváZS3(x) ↔ (JePravdiváZS3(y) → JePravdiváZS3(z)))). Pak by s využitím instance schématu ,A → (B → A)’: JePravdiváZS3(x) → (JePravdiváZS3(y) → JePravdiváZS3(x)), bylo možné dokázat platnost tohoto schématu, totiž x y z w ((JeImpl(z,y,x) JeImpl(w,x,z)) → JePravdiváZS3(w)).31 Mohli bychom se pak ptát, zda by se tu potom vůbec dalo mluvit o formalizaci důkazu bezespornosti – dodání axiomů tvrdících platnost schémat a odvozovacích pravidel už má dost 30 Obecněji nemusíme přidělovat význam (všem) symbolům – stačí najít jakýkoliv způsob, jak číst formule tak, aby vyjadřovaly pravdivá tvrzení a aby byla pravdivost zachována odvozováním. Jestliže ovšem daný systém obsahuje standardní kalkul, dá se očekávat, že např. logické spojky nabudou standardního významu – dá-li se vůbec mluvit o významu symbolů takto odděleně. 31 Otázka, zda formální systém musí obsahovat jinou definici pravdivosti, než jakou jsme původně zaváděli a která sestávala z množiny axiomů podobných instancím tzv. T-schématu:
T(jméno věty A) A, se zdá zajímavě souviset s tzv. deflační teorií pravdy a s problémem sebereflexe, o kterém se ještě dál zmíním.
47
Formalizace důkazu
blízko k dodání axiomu tvrdícího pravdivost všech dokazatelných formulí. Je tu ale ještě jeden problém, a to, že z pravdivosti dokazatelných formulí – aspoň v jistém smyslu – nelze vždycky usuzovat na bezespornost. Například tvrzení, že věta A: Věta A je nepravdivá. je pravdivá právě tehdy, když je nepravdivá, lze považovat za pravdivé (jsme-li ochotní vůbec o pravdivosti věty A mluvit). Ovšem z tohoto tvrzení už se dá (myšlenkovým postupem odpovídajícím odvození, které lze provést v kalkulu) usoudit, že věta A je a zároveň není pravdivá. Vezměme formuli y (JeKódZS3(x,y) → JePravdiváZS3(y)), která říká, že formule s kódem x je nepravdivá. Tuto formuli nazvu φ(x). K ní pak můžeme s použitím konstrukce z důkazu věty o pevném bodu najít formuli χ, jejíž kód je n a je v ZS3 dokazatelně ekvivalentní formuli φ(n). V ZS3 je tedy dokazatelná ekvivalence χ ↔ y (JeKódZS3(n,y) → JePravdiváZS3(y)). Protože je tu taky dokazatelná y (ψχ(y) → JeKódZS3(n,y)) (tedy za předpokladu, že axiom popisující kódování formulí a definice formulí ψφ jsou odpovídající), jsou tu dokazatelné i χ ↔ y (ψχ(y) → JePravdiváZS3(y)), y (ψχ(y) → JePravdiváZS3(y)) ↔ y (ψχ(y) → JePravdiváZS3(y)), a proto i y(ψχ(y)). Ovšem ψχ(y) je popis nějaké konečné posloupnosti čísel, a protože v ZF (a tedy i v ZS3) se o každé konečné posloupnosti čísel dá dokázat, že existuje (každá konečná posloupnost čísel je množina), je ZS3 sporný. Postup, kdy se z pravdivosti dokazatelných formulí usuzuje na bezespornost systému, tedy v tomto případě selhal. Potíž lze vidět v tom, že systém, v němž jsme tento postup formalizovali, se zdál rozumět pojmu pravdivosti svých formulí, který se ukázal být rozporuplný (podobně jako dříve pojem dokazatelnosti v sobě samém). V té souvislosti se můžeme ptát, jestli si sami můžeme být jistí tím, kdy používáme „bezpečné“ pojmy – zda umíme „předem“ odlišit problematické od neproblematických. K tomu se dostanu v příští kapitole. Mohli bychom se pokusit vyřešit problém s existencí formule, která – volně řečeno – „tvrdí“ svou vlastní nepravdivost tím, že bychom každou formuli, která říká, že některá formule je pravdivá, nahradili touto (druhou) formulí, a zbavili se tak predikátu JePravdiváZS3. Pak bychom ale nemohli vyjádřit tvrzení pravdivosti všech dokazatelných formulí, z něhož se usuzuje na bezespornost. Bylo by proto potřeba provést důkaz bezespornosti jinak, o což už se v této práci nebudu pokoušet. V každém případě se dá říct, že ve vystižení problému po „technické“ stránce došlo ke změně: problém spornosti systému schopného dokázat Gödelovu větu a problém nemožnosti najít k tomu postačující axiomy – problémy, které se dosud mohly zdát zcela nesouvisející, se nyní ukazují v novém světle: s využitím Gödelovy finty jsme k systému ZS3 našli axiom, který popisuje dokazatelnost z axiomů, mezi něž patří; ten samý fígl nám ale umožnil najít formuli, která „mluví“ o nepravdivosti sebe sama. S hodnocením po vzoru Járy Cimrmana: „Je to taková pěkná tečka za tím naším případem“ pokusů o formalizaci zanechám.
48
Interpretování Gödelovy věty
K KAAPPIITTO OLLA A 44:: IIN NT TE ER RPPR RE ET TO OV VÁ ÁN NÍÍ G GÖ ÖD DE ELLO OV VY YV VĚ ĚT TY Y “Počkejte, nevnášejte nám sem zase nové problémy. My teď stojíme před úkolem očesat švestku, viď, Sváťo? A jsme velmi rádi, že o tom víme.” “Jen aby nám to vydrželo.” - buď J. Cimrman, nebo L. Smoljak a Z. Svěrák
Gödelova věta se zdá souviset s otázkou vztahu mezi lidskou myslí a počítačem. Přesněji řečeno, zdá se něco vypovídat o hranicích možností jednoho v porovnání k těm druhého. Zkusím využít předchozího zkoumání k tomu, abych zjistil, nakolik jde Gödelovu větu z takové souvislosti podezírat. Jestliže dokážeme pravdivost Gödelovy formule pro nějaký formální systém, dokážeme něco, co daný systém – je-li bezesporný – dokázat nemůže. Odpověď na otázku, co formálnímu systému chybí k tomu, aby v něm bylo možné Gödelovu formuli dokázat tak, jak ji dokazujeme my, jsme se snažili najít sestrojením formálního systému, v němž by formalizovaná podoba důkazu existovala. Ukázalo se, že některá tvrzení, jež o systému vyslovujeme, nelze konsistentně vyslovovat o sobě samém, přesněji řečeno, že některé námi v důkaze použité pojmy nelze užívat k výpovědi o sobě samém a vyhnout se sporu. Z toho se může zdát, jako by omezení formálního systému spočívalo prostě v tom, že je formální systém – že to, čím je, jej činí neschopným mluvit konsistentně o tom, o čem my konsistentně mluvit můžeme. Význam výrazů jazyka formálního systému lze vidět jako určovaný množinou formulí v něm dokazatelných. Problematický výraz je pak takový, jemuž se dá podle toho, jaká je množina dokazatelných formulí, alespoň do určité míry oprávněně připsat význam problematického pojmu, přičemž se dá říct, že čím složitější je formální systém, tím komplexnější je tento význam (přesněji řečeno: tím složitěji je příslušný pojem definován). Z toho hlediska se problém ukazuje jako strukturální záležitost – otázka vztahu mezi „bohatostí“ množiny dokazatelných tvrzení a „stavby“ formálního systému. Přitom se zdá, že je tu jisté nepřekonatelné omezení v tom, že pokud by měla množina formulí dokazatelných v určitém systému „dodávat“ některým výrazům význam jistých pojmů (např. dokazatelnosti v sobě samém), obsahovala by už spor. Otázka, jaký (a jestli vůbec) je rozdíl mezi naším usuzováním a schopnostmi formálních systémů, si ale žádá podrobnějšího prozkoumání. Naše výhoda oproti formálnímu systému, pro nějž umíme dokázat Gödelovu větu, se zdála spočívat v tom, že jsme dokazování v něm schopní vidět jako předem nějak pevně určené a můžeme jej chápat jako mluvícího o dokazování v sobě samém v pravdivých větách aritmetiky. Můžeme se tedy ptát, zda takovou výhodu budeme mít oproti každému formálnímu systému, na nějž se Gödelova věta vztahuje. Zkusím nejprve zjistit, co z Gödelova výsledku vyplývá pro situaci, kdy by schopnosti člověka usuzovat o přirozených číslech popisoval formální systém, na jaký se věta vztahuje. O systému budu přitom říkat, že se na něj vztahuje Gödelova věta, jestliže bude splňovat předpoklady druhé z výše uvedených verzí.
MYSL JAKO FORMÁLNÍ SYSTÉM (BOBŮV PŘÍPAD) Představme si, že existuje takový formální systém, označme ho ČL, na který se za předpokladu jeho bezespornosti vztahuje Gödelova věta a matematik Bob může dospět k pravdivosti právě těch tvrzení vyjádřitelných aritmetickými formulemi, která jsou vyjádřena formulemi dokazatelnými v tomto systému. Pak by existovala pravdivá aritmetická formule, která by v ČL
49
Interpretování Gödelovy věty
nebyla dokazatelná, a Bob by tedy nebyl s to dokázat tvrzení, jež vyjadřuje, za předpokladu, že neumí dokázat, že jedna se nerovná jedna. Předpokládejme nejprve, že Bob nezná vztah mezi svými schopnostmi a dokazatelností v ČL, a proveďme myšlenkový experiment: ukažme Bobovi systém ČL (podobnou situaci znázorňuje obrázek 3.1 v předchozí kapitole) a nechme jej zkoušet dokázat jeho bezespornost. Kdyby se mu to podařilo, stačilo by mu zjistit, že se na ČL vztahuje Gödelova věta, a dokázal by pravdivost Gödelovy formule pro ČL, která je pravdivá právě tehdy, když není v ČL (a tedy ani Bobem) dokazatelná. Bob by tedy dokázal nepravdivé tvrzení, jsa nejspíš přesvědčen, že dokázal pravdivé. Z této formule by nyní Bob mohl odvodit spor, jenže formule je nejspíš tak dlouhá, že Bob ji v životě nedočte do konce, ani ji nenapíše – leda s pomocí nějaké zkratky jako ,DokČL(n)’ (dalo by se říct, že Bob by v podstatě nevěděl, co o přirozených číslech dokázal, věděl by jen, že pravdivost této formule je ekvivalentní její nedokazatelnosti v ČL). Ačkoliv by činnost Bobovy mysli popisoval sporný systém, nemusel by Bob tento rozpor ve svém usuzování nikdy odhalit. Tím získáváme první hypotézu H1: Naše usuzování o přirozených číslech může vést ke sporu, ale my jsme to zatím nezjistili. Když to zjistíme, nedokážeme s tím nic udělat. Jestliže Bobovo usuzování není rozporné a on ví, že se na systém ČL za předpokladu jeho bezespornosti vztahuje Gödelova věta, nemůže dokázat bezespornost systému ČL. Jestliže je připraven z pravdivosti formulí dokazatelných v ČL usoudit na jeho bezespornost, nemůže dokázat ani pravdivost jeho axiomů a správnost odvozovacích pravidel – tedy nemůže odhalit, že tak sám usuzuje. Další možnost je, že by Bob nebyl s to poznat, že se na systém ČL za předpokladu jeho bezespornosti vztahuje Gödelova věta. To se může zdát dost divné, představíme-li si, že Bob má před sebou nějaký srozumitelný popis axiomů, schémat a odvozovacích pravidel, jaký máme např. u systému Peanovy aritmetiky. Kdyby ale Bob tento systém „potkal ve světě“ třeba v podobě stroje, který vypisuje důkazy v něm, je možná přestavitelné, že by nedokázal a ani v principu nemohl dokázat třeba to, že relace „...je kód důkazu formule s kódem ... v ČL“ je, pro nějaké kódování jazyka ČL, rekurzívní32. V každém případě je tu hypotéza H2: Existuje formální systém, který popisuje činnost lidské mysli, a člověk není schopen dokázat pro něj Gödelovu větu. Nakonec si představme, že by Bob nějak zjistil, že systém ČL popisuje jeho schopnosti dokazovat některá matematická tvrzení. Potom by věděl, že formule γČL je pravdivá právě tehdy, když ji nemůže dokázat. Mohl by pak uvažovat takto: Řekněme, že γČL mohu dokázat. Pak by ale byla nepravdivá, takže ji dokázat nemohu. Potom je ale pravdivá. Jenže tím jsem ji dokázal! Bob už by tedy krátkou úvahou uměl dospět k tomu, že nemůže počítat s pravdivostí tvrzení, které je schopen dokázat, a nemohl by s tím nic dělat. Jestliže by tedy Bobovo matematické usuzování bylo formalizovatelné v kalkulu ČL, nesměl by to Bob zjistit, pokud by měl moci důvěřovat svým usuzovacím schopnostem. Předpokládáme-li, že můžeme bezrozporně používat aritmetické pojmy, které formální systémy, na něž se vztahuje Gödelova věta, používat nemohou, předpokládáme tím také, že naše myšlení buď nelze v takových systémech formalizovat, anebo to nemůžeme zjistit.
32
třeba proto, že by k vhodnému popisu ČL vůbec nemohl dospět
50
Interpretování Gödelovy věty
Máme tu zatím dvě hypotézy, přičemž se musím přiznat, že správnosti první z nich (H1) se mi nechce moc věřit. Kromě těch je tu ještě hypotéza, že lidské usuzování nemůže žádný formální systém, na nějž se vztahuje Gödelova věta, zachytit: Neexistuje formální systém, na nějž se vztahuje Gödelova věta a v němž by byly dokazatelné právě ty aritmetické formule, které vyjadřují tvrzení, jež jsme schopní (kdy) dokázat. Tady bychom se však mohli bránit tomu, mluvit o nějakém rozlišení tvrzení na ty, které jsme, a ty, které nejsme schopní dokázat – ukázalo se například, že z pohledu některých formálních systémů nelze toto rozlišení učinit a vyhnout se sporu. Předchozí hypotézu bychom proto mohli radši přeformulovat: H3: Neexistuje formální systém, na nějž by se vztahovala Gödelova věta a v němž by byly dokazatelné všechny aritmetické formule,jejichž pravdivost jsme s to dokázat. V hypotéze H3 už se mluví jen o dokazatelnosti některých tvrzení – konkrétně těch, která lze dokázat v nějakém formálním systému, na nějž se vztahuje Gödelova věta. H3 plyne z těchto předpokladů: 1. Naše usuzování o přirozených číslech je bezrozporné, 2. Jestliže formální systém splňuje předpoklady Gödelovy věty, umíme to zjistit, a naší schopnosti dokázat Gödelovu větu. Zdá se tedy, že Gödelova věta nevylučuje případ, že bychom dokázali jen tolik, co jistý formální systém. Jestliže ale v usuzování o přirozených číslech nemůžeme dospět ke sporu, nedokázali bychom pak zjistit, že se na takový systém vztahuje Gödelova věta. Vysvětlení můžeme vidět v tom, že pokud ano, byli bychom schopní popsat dokazatelnost námi samými, což se z pozice někoho či něčeho se schopnostmi formálního systému splňujícího předpoklady Gödelovy věty ukázalo vést ke sporu. Vypadá to ovšem, že samotná Gödelova věta toho moc neříká o schopnostech usuzování mimo hranice jistého druhu formálních systémů: o tom se něco ukáže až tehdy, kdy dokážeme Gödelovu větu pro nějaký konkrétní systém – tedy ukážeme, že tento systém splňuje její předpoklady.
Je člověk ve výhodě? Jestliže pro nějaký systém dokážeme Gödelovu větu, umíme ho vidět jako mluvícího o dokazatelnosti v sobě samém v pravdivých větách aritmetiky určitého druhu. Jestliže existuje formální systém, který předpoklady Gödelovy věty splňuje a přesto popisuje naše dokazování výroků v jazyce aritmetiky, nemůžeme tohohle být schopní (tedy pokud nemáme dospět ke sporu). S pomocí výraziva z předchozí kapitoly můžeme říct, že bychom v takovém případě nedokázali najít takové čtení f aritmetických formulí, které by formulím druhu y φ(n), kde φ(x) je určitá (jediná) formule popisující nějakou rekurzívní vlastnost, přiřadilo tvrzení Formule s kódem n je v daném systému dokazatelná, pravdivost formulí při čtení f by se shodovala s jejich pravdivostí při standardním čtení a nalezení kódu formule vzniklé substitucí jména čísla n za proměnnou y ve formuli s kódem k by byla „dobře proveditelná“ procedura. Buď bychom proto nemohli dokazování v daném systému dobře popsat s pomocí rekurzívní relace „... je kód důkazu formule s kódem ...“ při vhodném kódování, přestože by tu taková relace byla, nebo bychom neuměli ukázat, že daný systém se v pravdivosti jistých formulí (popisujících nacházení se v této relaci) nemýlí, ačkoli by se v ní skutečně nemýlil. (Není divu, pokud u formálních systémů, které sami vytváříme, tento případ nenastává.)
51
Interpretování Gödelovy věty
SEBEREFLEXE: CELEK V SOBĚ SAMÉM Není pochyb o tom, že z našeho hlediska se mysl zdá projevovat schopnosti, které v důkazech ve formálním systému nepostihneme. Jednou z nich je schopnost sebereflexe, kterou můžeme vidět například v tomto: Víme, že ať budou výroky A a B jakékoliv, shledáme tvrzení „A → (B → A)“ pravdivým. Jestliže si něco myslíme, jsme často schopní uvědomit si, že si to myslíme, a občas dokonce, proč si to myslíme. Dokonce bych řekl, že tento postup je jádrem logického uvažování. Na úrovni jazyka se sebereflexe objevuje, když říkáme, že tvrzení je pravdivé, nebo že platí, že..., kdy jakoby spojujeme různé úrovně mluvení (jazyk a metajazyk) v jednu. Přitom takové obraty nejspíš potřebujeme k tomu, abychom vyjádřili platnost logických schémat. Z dosavadního zkoumání není jisté, jestli sebereflexe má nějaké hranice. U některých formálních systémů tomu tak bylo, ovšem formální systém se nebyl schopný nijak vypořádat se sporem – nemohl se (z našeho hlediska) vyvíjet. Oproti tomu se zdá, že naše mysl takovou schopnost má, alespoň do určité míry. Otázka možnosti sebereflexe či toho, nakolik jsme schopní učinit svoji myšlenkovou činnost předmětem našeho zkoumání, by potom mohla souviset s otázkou, nakolik jsme schopní naše myšlení změnit. Jestliže zákonitost, kterou jsme viděli (a matematicky popsali) u formálních systémů, lze zobecnit i pro člověka, bylo by k úplnému poznání našeho myšlení potřeba, být připraveni změnit jakýkoli jeho aspekt: jakékoli jeho zachycení by se totiž tímto zachycením stávalo nepravdivé. Připadá mi, že právě k tomu směřují některé finty vynalezené na druhém konci světa: „Jak je možné vyhnout se chybě, když není přípustná ani řeč, ani mlčení?“ „Vždy si vzpomenu na Kiangsu v březnu, na křik koroptve, na množství vonících květů.“ Sebereflexe se na úrovni jazyka objevuje v podobě autoreference, kterou zkusím prozkoumat trochu podrobněji, ježto by mohla některé aspekty sebereflexe pomoci odhalit.
Autoreference Autoreferenci využívá hlavní myšlenka Gödelovy věty. Pro porozumění konstrukci Gödelovy formule, její pravdivosti i nedokazatelnosti je potřeba (nějak) porozumět tomuto jevu. Nejdřív se zaměřím na to, jaké nástroje k autoreferenci známe, přičemž budu hledat především možnost popsat celek uvnitř tohoto celku, konkrétně formální systém uvnitř něho samého. Schopnost o něčem mluvit zřejmě nespočívá v tom, najít nějaké symboly: jde o to, dodat těmto symbolům odpovídající význam, který se projeví ve schopnosti z tvrzení jimi vyjádřených usuzovat, ať už jde o naše uvažování nebo odvoditelnost ve formálním systému.33 Začnu se známým případem „kritické“ autoreference, větou A: Věta A je nepravdivá. Abychom věděli, co věta říká, potřebujeme se podívat před ní, na ,A’ s dvojtečkou.34 Tím se ovšem zdá, jako by to, co věta A říká, nebylo popsáno samotnou touhle větou. To samo nám ale nemusí vadit – význam výrazů věty nehledáme v ní samé (což je možná rozdíl oproti množinám dokazatelných formulí). Jenže význam toho, co stojí mimo větu, má být zase určen touto větou. Jinými slovy, aby dávala věta dobrý smysl, musí už mít to, co následuje za ,A’ s dvojtečkou, dobrý 33 Například, nebyla by potíž, obohatit jazyk formálního systému s množinou axiomů A o symbol ,A’ a jeho axiomy popsat fomulí ,xA’. Otáza ale je, jak formálnímu systému „říct“, co všechno z toho může vyvodit. 34 Mimoto je potřeba vědět, že připsáním ,A’ s dvojtečkou před větu vztáhneme tuto větu na sebe. Jak byste popsali, co připisování ,A’ s dvojtečkou znamená? Možná nějak jako: „podívejte se za to, co následuje: to je A“.
52
Interpretování Gödelovy věty
smysl: mluví se tu přeci o jeho pravdivosti. Proto se zdá, že můžeme vůbec pochybovat o smysluplnosti takového vyjádření. Nástroj, jakým je ,A’ s dvojtečkou, bychom nemohli použít k popisu formálního systému uvnitř tohoto systému už proto, že ,A’ s dvojtečkou bychom museli umístit před popis tohoto systému.
A A:: V Věěttaa A A jjee nneepprraavvddiivváá
Další metoda, jak výrazy „namířit“ na výrazy, je metoda uzávorkování. Nepravdivost věty pak můžeme vyjádřit takto: Věta ,...’ je nepravdivá. Protože věta mluvící o větě s pomocí uzávorkování je delší než věta, o které takto mluví, nemůže věta s pomocí uzávorkování takto mluvit o sobě samé (pokud není nekonečná: nekonečné věty totiž jsou delší, než jsou). V praxi to potom vypadá tak, že chceme napsat větu: Věta ,Věta ,Věta ,…’ je nepravdivá.’ je nepravdivá.’ je nepravdivá, ale nikdy se nám to nepodaří. Z toho ovšem není nijak vyloučeno, že by existovala věta, nazvěme ji ,…’, o níž bychom byli schopní ukázat, že její pravdivost je ekvivalentní pravdivosti věty Věta ,...’ je nepravdivá. Další způsob popisu výrazů je s pomocí slovních spojení jako ,věta, která ...’ – například: první gramaticky správná česká věta, která má sto písmen a začíná písmenem P. Přitom se předpokládá, že označovaný výraz je tímto popisem jednoznačně určen. Nebezpečí s takovými způsoby popisu je, že jimi určovaný výraz může mít být určován sebou samým,35 což lze vidět například u popisu: věta, která vznikne z věty ,Věta x je nepravdivá’ dosazením věty ,Věta y je nepravdivá’, která vznikne dosazením věty ,Věta x je nepravdivá’ za y, za x sestrojeného s pomocí zkombinování dvou způsobů popisu výrazu. Tady je věta x určována s pomocí věty y, která je zase určována s pomocí věty x, přičemž není ani zaručeno, že taková věta – a tedy ani věta splňující popis – bude existovat, ani že tato věta bude určena jednoznačně. Konečně nejjednodušší způsob, jak vyjádřit sebepopírající větu, je nejspíš: Tato věta není pravdivá či Toto není pravda.
Takhle se jde dívat i na každý popis, který žádný výraz nesplňuje – výraz, který má být určovaný tímto popisem, je určovaný sebou samým opačně, než jaký by byl, ať by byl jakýkoliv. Například u popisu první gramaticky správná česká věta x, která je kratší než x je věta x určována s pomocí délky věty x, tedy jí samé, která má být jiná, než jaká by byla, ať by byla jakákoliv. 35
53
Interpretování Gödelovy věty
Zdá se, že popis celku uvnitř tohoto celku umožňují z předchozích způsobů jen poslední dva, přičemž u posledního by bylo potřeba předpokládat, že je tu nějaký výraz jako ,toto’, který bychom mohli použít k vyjádření jako ,tato teorie’, ,toto všechno’ apod., a kterému by nebylo potřeba nijak dodávat význam. Předposledního způsobu popisu výrazů využil (společně s kódováním) Gödel k sestrojení autoreferenční formule: formule tvaru ,φ(n)’ má vždycky kód větší než n, ovšem formule tvaru x(Subst(x,k,k) φ(x)), která mluví o formuli vzniklé dosazením jména čísla k za proměnnou y ve formuli s kódem k, už nikoli. O Gödelově formuli se dá hovořit jako o svého druhu popisu celku uvnitř tohoto celku, ovšem s tou výhradou, že význam symbolů jím není nijak určen. O formuli DůkPA(x,y) se dá mluvit jako o popisu dokazatelnosti v Peanově aritmetice (což je právě to, co nás na ní zajímá) v ní samé, ovšem s tou výhradou, že význam kódování není v ní jakožto systému obsažen. O systému ZS3 se oproti tomu dá tvrdit, že obsahuje popis sebe sama (tedy dokazatelnosti v sobě), jenže je kvůli tomu sporný. Přitom jeho rozdíl oproti některým jiným sporným systémům je spíš intuitivní: totiž, že můžeme k neformálnímu důkazu hovořícímu o dokazatelnosti v něm najít odvození v něm, které shledáme odpovídajícím.
K čemu vlastně slouží autoreferenční věty? Na běžné používání vět se dá dívat takto: máme nějaké přesvědčení, které se větami (takovými, kterým má smysl připisovat pravdivost) snažíme vyjádřit. Dalo by se říct, že větu vytváříme k tomu, co už máme na mysli. Oproti tomu větou A žádné takové přesvědčení, aspoň zpočátku, nevyjadřujeme: její obsah vznikne až tím, že jí vytvoříme. V tom smyslu by se dalo o větě A prohlásit, že je jaksi umělá: nikdo ji ve skutečnosti říct nechce, protože jí – dokud ji nevysloví – nemá co vyjádřit. Dalo by se soudit, že k problému nedochází takovým používáním jazyka, k jakému jsme jazyk vytvořili – vznikne až tím, když se rozhodneme jazyk učinit předmětem sebe sama – což se dá vidět jako vytváření problému, který by jinak vůbec nebyl problémem. Zabývat se větami jako A se pak ale může zdát jako nesmyslná činnost. Otázka je, zda kterákoli jiná činnost může být smysluplnější – zda může existovat obsah věty předtím, než tu nějaká věta je. Koneckonců, přesvědčení, že na počátku bylo slovo, je docela rozšířené.
(PO)ZNÁME PŘIROZENÁ ČÍSLA? Jestliže se na formální systém, nezvěme jej T, vztahuje Gödelova věta, existuje nestandardní interpretace formulí jazyka aritmetiky, která splňuje všechny formule v T dokazatelné. Konkrétně to znamená, že množina objektů, o nichž aritmetické formule v této interpretaci mluví, se podstatně liší od množiny přirozených čísel. V tom smyslu se dá říct, že formální systém „neví“, co přesně jsou přirozená čísla. Jestliže naše usuzování o přirozených číslech popisuje některý formální systém, dá se v tomtéž smyslu tvrdit, že taky nevíme, co přesně jsou přirozená čísla: z naší matematické praxe není jednoznačně určeno, o čem mluvíme. Ovšem že to není jednoznačně určeno, by mohl posoudit jen někdo, kdo „přirozeným číslům“ rozumí líp než my. V jakém smyslu se pak ale dá vůbec mluvit o tom, kdo „přirozeným číslům“ rozumí líp – k čemu (objektivnímu) se dá porozumění vztahovat? Zdá se, že tím, že naše porozumění číslům je lepší, než jaké „má“ formální systém, si můžeme být jistí díky tomu, že víme, jak formální systém funguje. Kdyby pak pro nás někdo dokázal Gödelovu větu, mohl by si být jistý, že přirozeným číslům rozumí líp než my. Proto se mi zdá, že alespoň v tomhle smyslu se dá o porozumění pojmu přirozeného čísla mluvit. Naše omezení popisované formálním systémem by nemuselo být nepřekonatelné: například je podle všeho docela dobře možné, že předtím, než Gödel dokázal svoji větu, jsme se nepřekročili schopnosti ztělesněné Peanovou aritmetikou: nedokázali jsme žádné tvrzení vyjádřitelné v jazyce
54
Interpretování Gödelovy věty
aritmetiky, které by nebylo formálně dokazatelné v Peanově aritmetice. Zdá se ovšem, že naše představa množiny přirozených čísel je docela jasná. Mohli bychom se proto ptát, zda je vším, co dnes o číslech dokážeme říct, tato množina jednoznačně určena – anebo zda s dalším pokrokem v matematice můžeme zjistit – podobně jako dřív u pojmu matematického nekonečna – že dnes vlastně nebylo vůbec jasné, která čísla máme na mysli.
SHRNUTÍ Podle předchozích zkoumání se zdá, že Gödelova věta nedává žádnou definitivní odpověď na otázku vztahu mezi hranicemi schopností lidské mysli a možnostmi strojů. Ukazuje ale, jak lze účinně spojit dva způsoby pohledu na tutéž věc: intuitivní porozumění významu s matematickým popisem. Kromě toho se dá, že téma autoreference, ke kterému nás Gödelova věta naléhavě přivádí a které může být úzce spojeno s otázkou naší schopnosti porozumět sobě samým, poskytuje obrovské množství možností, s čím si lámat hlavu. Možná dokonce, že s ním dobře popsatelným způsobem souvisejí i zajímavé matematické problémy. O tom už ale v téhle práci, která se k závěru blíží tak rychle, že skončí dřív, než řeknete šv
55
PPO OU UŽ ŽIIT TÁ Á LLIIT TE ER RA AT TU UR RA A Adams, D. (1979): The Complete Hitchhiker's Guide. Wings Books, 1996 Cimrman, Smoljak, Svěrák: Švestka. Ladislav Horáček – P, 1998 Dummett, M. (1963): The Philosophical Significance of Gödel's Theorem. Ratio V, 140-155. Engström, F. (2002): First-order arithmetic, Supplementary material, Version 1.1. zdroj internet [1], 2002. Gaifman, H. (2000): What Gödel's Incompleteness Result does and does not Show. Journal of Philosophy 97, 2000, 462-70. Gödel, K. (1931): Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I. Monatshefte für Mathematik und Physik 38, 173-198. Hofstadter, D. R.: citáty z Metamagical Themas. Basic Books, Inc., 1985, Chapter 16. Kleene, S. C. (1976): The Work of Kurt Gödel. Journal of Symbolic Logic 41, 761-778. Nagel, E., Newman, J. R. (1958): Gödelův důkaz. Vysoké učení technické v Brně, nakladatelství VUTIUM, 2003 Shapiro, S. (1998): Proof and Truth: Through Thick and Thin. Journal of Philosophy, Volume XCV, 1998, 493-521. Smith, P. (2005): An Introduction to Gödel΄s Tudorem. rukopis. Švejdar, V.: moje zápisky z přednášky Teorie algoritmů v r. 2001. Watts, A. W.: přeložený citát z The Way of Zen. Vintage Books, New York 1957, 183.
ODKAZY NA INTERNETOVÉ STRÁNKY: [1] http://www.cs.chalmers.se/Cs/Grundutb/Kurser/matlog/material/arithmetic.pdf [2] http://www.cis.udel.edu/~case/self-ref.html [3] http://www.cut-the-knot.org/selfreference/index.shtml
56
