1. KAPITOLA DRUHÁ: VÝZNAM A FORMA V MATEMATICE
    1. pr-SYSTÉM
    2. ROZHODOVACÍ PROCEDURA

KAPITOLA DRUHÁ: VÝZNAM A FORMA V MATEMATICE

Inspiraci pro své dvě postavy jsem našel právě v Dvojhlasé invenci. Stejně jako si Lewis Carroll dovolil vypůjčit Želvu a Achilla od Zenona, dovolil jsem si zase já vypůjčit si oba dva od Lewise Carrolla. V Carrollově dialogu se stále znovu a znovu děje totéž, až na to, že pokaždé na neustále vyšší úrovni; je to úžasná analogie k Bachovu Nekonečně stoupajícímu kánonu. Když ale odhlédneme od jeho vtipu, ponechává dialog otevřen hluboký filozofický problém: řídí se slova a myšlenky formálními pravidly, nebo nikoli? Je to problém, který řešíme v celé knize.

V této a následující kapitole si ukážeme několik nových formálních systémů. Získáme tím mnohem širší pohled na samotný pojem formálního systému. Na konci příští kapitoly už by tak čtenář měl mít vcelku solidní představu o schopnostech formálních systémů a měl by pochopit, proč se jimi matematici a logici tolik zabývají.

pr-SYSTÉM

Formální systém vytvořený pro tuto kapitolu budeme nazývat pr-systém. Pro matematiky nebo logiky žádný zvláštní význam nemá — vznikl jen pro potřeby této knihy a jeho význam spočívá pouze v tom, že skvěle ilustruje řadu myšlenek, které v knize hrají důležitou roli. Náš pr-systém má tři symboly: p r — tedy písmena p, r a pomlčku.

Kromě toho má pr-systém nekonečný počet axiomů. Proto je všechny nelze sepsat a my si musíme najít nějaký způsob, jak je popsat. Vlastně chceme více než jen jejich pouhý popis, potřebujeme způsob, jímž rozlišíme, zda daný řetězec axiomem je, nebo není. Pouhý popis by sice mohl axiomy charakterizovat úplně, ale nejasně — což byl také problém způsobu charakterizování teorémů v MIU-systému. Nechceme se pachtit neurčitě — možná dokonce nekonečně — dlouho, jenom abychom zjistili, že daný řetězec axiomem je, nebo není. Budeme si proto definovat axiomy tak, aby rozhodovací procedura pro to, zda určitý řetězec složený z našich tří symbolů p, r a pomlčky je axiomem, byla zcela zjevná.

DEFINICE: xp-rx- je axiomem tehdy, když se x skládá pouze z pomlček. Musíme zdůraznit, že „x“ musí v obou výskytech reprezentovat tentýž řetězec pomlček. Axiomem je například —— p- r——-. Vlastní výraz „xp-rx-“ axiomem samozřejmě není (protože „x“ nepatří do pr-systému); je to spíše něco jako forma, v níž jsou všechny axiomy odlévány, a nazývá se schéma axiomů. pr-systém bude mít pouze jedno odvozovací pravidlo:

PRAVIDLO: Předpokládejme, že pro všechna x, y a z platí, že reprezentují určité řetězce složené pouze z pomlček. Dále předpokládejme, že xpyrz je teorém. Potom je i xpy-rz- teorémem. Dosaďme si například za x „--“, za y „---“ a za z „-“. Pravidlo nám říká: Jestliže – p - - -r- je teorém, pak jím bude i --p----r--. Tato věta, jak je pro odvozovací pravidla typické, stanoví přičinnou spojitost mezi „teorémovostí“ dvou řetězců, avšak netvrdí, že teorémem je jeden nebo druhý z nich sám o sobě. K procvičení bude nejužitečnější, když si sami najdete rozhodovací proceduru pro zjištění teorémů pr-systému. Není to nijak těžké; když si s tím chvíli pohrajete, asi na to přijdete. Zkuste si to.

Kermit tea time

ROZHODOVACÍ PROCEDURA

Předpokládám, že jste na tom pracovali, takže je možná zbytečné poukazovat na to, že každý teorém pr-systému má tři oddělené skupiny pomlček, oddělené jedním p a jedním r, přesně v tomto pořadí. (Můžeme si to dokázat argumentem založeným na „dědičnosti“, právě tím, který ukázal, že všechny teorémy MIU-systému musí začínat na M.) To znamená, že už jen s ohledem na pouhou formu můžeme vyloučit z teorémů řetězec typu --p--p--p--r----.

Zdůrazňovat spojení „s ohledem na pouhou formu“ může působit hloupě — je snad na řetězci něco jiného než jeho forma? Co jiného by ještě mohlo hrát roli při určování jeho vlastností? Je zřejmé, že nic. Mějme to však na paměti během další rozpravy o formálních systémech; představa „formy“ se začne komplikovat, bude nabývat abstraktnějšího charakteru a budeme muset více přemýšlet o významu slova „forma“. Nicméně, jako dobře utvořený řetězec si označme jakýkoli řetězec, který začíná skupinou pomlček, po níž následuje jedno p, za ním je druhá skupina pomlček, po ní r a nakonec poslední pomlčková skupina.

Zpátky ale k rozhodovací proceduře... Kritériem „teorémovosti“ je, že souhrnná délka prvních dvou skupin pomlček by se měla rovnat délce skupiny třetí. Tak například - - p--r---- teorémem je, protože 2 plus 2 se rovná 4, zatímco --p--r- jím není, jelikož 2 plus 2 není 1. Chceme-li zjistit, proč je toto kritérium správné, podívejme se na příslušné schéma axiomů. Očividně v něm vznikají pouze axiomy, které splňují součtové kritérium. Za druhé se můžeme podívat na odvozovací pravidlo. Jestliže první řetězec vyhovuje kritériu sčítání, musí to platit i pro druhý — a naopak, pokud první řetězec kritériu sčítání nevyhovuje, pak totéž Platí i pro druhý. Dané pravidlo dělá z kritéria sčítání dědičnou vlastnost teorémů: každý teorém přenáší tuto vlastnost na své potomky. To dokazuje, že kritérium sčítání je správné.

Mimochodem, pr-systém má vlastnost, která nám umožní s jistotou říci, že rozhodovací procedura existuje, ještě před nalezením samotného sčítacího kritéria. Je to skutečnost, že pr-systém není komplikován protisměrnými proudy pravidel prodlužování a zkracování; má pouze pravidla prodlužování. Každý formální systém, který říká, jak udělat z kratších teorémů delší, ale nikdy ne naopak, musí mít pro své teorémy rozhodovací proceduru. Představme si, že je dán řetězec. Nejprve si ověříme, zda je to axiom (předpokládám, že pro určení, zda je něco axiom, existuje rozhodovací procedura — jinak je to beznadějné). Pokud to axiom je, pak je to z definice i teorém, čímž test skončil. Předpokládejme tedy, že to axiom není. Aby to byl v tomto případě teorém, musel by vzniknout z kratšího řetězce prostřednictvím některého z pravidel. Zkoušením jednoho pravidla po druhém můžeme nejen určit pravidla, která by mohla případně daný řetězec odvodit, ale také přesně stanovit, které kratší řetězce by mohly být jeho předky v „rodokmenu“. Tímto způsobem „zredukujeme“ problém na zjištění, zda je některý z nových, ale kratších řetězců teorém. Stejným testem pak může projít každý z nich. Nejhorší, co se může stát, bude množení stále kratších řetězců, které bude nutné všechny testovat. Když se budeme tímto stylem prokousávat zpět, nevyhnutelně se budeme stále přibližovat zdroji všech teorémů — schématům axiomů. Zkracovat řetězce donekonečna nemůžeme; nakonec tak buď zjistíme, že jeden z kratších řetězců je axiom, nebo uvízneme v bodu, kde budeme nuceni konstatovat, že mezi našimi kratšími řetězci žádný axiom není a žádný z nich už se nedá zpětnou aplikací některého pravidla dál zkrátit. Ukazuje to, že u formálních systémů ve skutečnosti zdaleka nejde jen o pravidla prodlužování; kouzlo formálních systémů je spíše ve vzájemné souhře pravidel prodlužování a zkracování.