1. pr-SYSTÉM
  2. ROZHODOVACÍ PROCEDURA
  3. ZDOLA NAHORU A SHORA DOLŮ

KAPITOLA DRUHÁ: VÝZNAM A FORMA V MATEMATICE

Matematik

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ředstavuo 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.

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í.

ZDOLA NAHORU A SHORA DOLŮ

Metodu, kterou jsme si právě popsali, můžeme označit za rozhodovací proceduru shora dolů, proti níž stojí procedura zdola nahoru, o níž budeme mluvit nyní. Velmi se podobá džinově systematické metodě generování teorémů pro MIU-systém, komplikuje ji však přítomnost schématu axiomů. Vytvoříme si „košík“, do něhož budeme házet teorémy v tom pořadí, v jakém je budeme tvořit. Bude se to odehrávat následujícím způsobem:

(1a) Do košíku vhodíme nejjednodušší možný axiom (-p-r--).

(1b) Na vhozenou položku uplatníme odvozovací pravidlo a výsledek dáme rovněž do košíku.

(2a) Do košíku vhodíme druhý nejjednodušší axiom.

(2b) Na každou položku v košíku uplatníme odvozovací pravidlo a všechny výsledky hodíme do košíku.

(3a) Do košíku vhodíme třetí nejjednodušší axiom.

(3b) Na každou položku v košíku uplatníme odvozovací pravidlo a všechny výsledky hodíme do košíku. a tak dále.

Krátké zamyšlení ukáže, že tímto způsobem se nám nevyhnutelně podaří vytvořit každý teorém pr-systému. Košík se navíc postupem času plní stále delšími a delšími teorémy. To je opět důsledek nepřítomnosti pravidla zkracování. Jestliže tedy máme řetězec --p---r-----, u něhož chceme otestovat, zda jde o teorém, stačí nám jít podle očíslovaných kroků a přitom neustále kontrolovat, zda se neobjevil náš řetězec. Pokud se ukáže — je to teorém! Jestliže bude v určité chvíli vše, co půjde do košíku, delší než náš řetězec, zapomeňme na to — teorém to není. Toto je rozhodovací procedura zdola nahoru, protože si razí cestu od základů, to znamená od axiomů. Procedura, o níž jsme mluvili předtím, má charakter shora dolů, protože funguje přesně obráceně: prodírá se zpět k základům.