Mechanická vyvoditelnost, formulovatelnost, dokazatelnost

Na počátku svého (vcelku půvabného) článku psaného formou dialogu autorka praví: „Gödelova popularita je velmi podobná Einsteinově. Na jedné straně povrchnost, na druhé pár zasvěcených.“ Vřele souhlasím a jelikož se jako profesionální matematický logik pokládám za jednoho z pár zasvěcených, dovoluji si poznamenat, že autorka používá pojem „mechanická vyvoditelnost“ poněkud temným a dvojznačným způsobem: chvíli jako formulovatelnost (expresivita), chvíli jako „formální dokazatelnost“. Není pravda (odporuje obvyklé definici důkazu), že předpoklad bezespornosti dělá důkaz důkazem; a v autorčině větě „Gödel dokázal, že je-li formální systém dostatečně bohatý, pak se dají mechanicky vyvodit věty podobné paradoxu, které by mohly systém znehodnotit“ mohou slova „mechanicky vyvodit“ znamenat pouze „formulovat, vyjádřit“, nikoli „formálně dokázat“. Gödel právě ukázal, že kdyby jeho formule (vyjadřující svou nedokazatelnost) byla v systému formálně („mechanicky“, chcete-li) dokazatelná, byl by sporný. Běžný význam „mechanické vyvoditelnosti“ (zejména“ mechanické vyvoditelnosti z axiomů“, str. 467) je právě „formální dokazatelnost“.

Abych čtenáře neunavoval, doporučuji, aby z dialogu prostě vynechal (anebo bral cum grano salis) místa, kde autorka mluví o mechanické (formální) vyvoditelnosti. Zmatek je mj. také ke konci prvního sloupce str. 468: Gödelovi se podařilo dovolenými formulačními kroky dojít k číslu, které po dekódování znamenalo „Toto číslo do systému nepatří“, tj. „není v něm formálně dokazatelné“. Nebylo v něm formálně vyvozeno ve smyslu „formálně dokázáno“, takže autorka se mýlí, když říká, že „fyzicky“ tam vlastně bylo. Autorka později správně říká (a to je to, o co jde), že Gödelova věta znamená vlastně parafrázovaně „Tato věta se nedá dokázat“ – a to je pravda. (Mimochodem: žádný paradox.) Nakonec poznámka k bibliografii: všechny citované české články jsou z knihy J. Malina, J. Novotný (editoři): Kurt Gödel, Nadace Universitatis Masarykiana, Brno 1996 (za zmatek v referencích možná nemůže autorka). Můj citovaný článek o Gödelově důkazu Boží existence (z této knihy) nesouvisí s tematikou autorčina dialogu; zato si však dovolím doporučit čtenáři (i autorce) z téhož svazku svůj výklad Gödelových vět, který tam figuruje pod názvem „Matematik a logik“.

RNDr. Petr Hájek, DrSc.

Odpověď na připomínky RNDr. Petra Hájka, DrSc.

Z poznámky RNDr. Petra Hájka se dovídám, jak snadno může dojít k záměně termínů „mechanická vyvoditelnost“ a „formální dokazatelnost“. A přitom zaměnitelné nejsou, aniž by se porušil smysl zvláště na místech, která Petr Hájek zmiňuje. Za neuvážlivě zvolený termín „mechanická vyvoditelnost“ se jemu i ostatním čtenářům omlouvám.

To, co jsem měla tím termínem na mysli, nazývá Gödel rekurzivitou. V jeho slavném článku z roku 1931 se vyskytují termíny „rekurzivní pojem“, „rekurzivní třídový znak“, „rekurzivní relace“ apod., ale zejména je rekurzivní nerozhodnutelná věta (česky článek vyšel v knize editorů Maliny a Novotného, viz citaci opravenou Petrem Hájkem). V komentáři k témuž článku používá Stephen C. Kleene (S. Feferman ed., Kurt Gödel, Collected Works I, Oxford, 1986) pro odpovídající pojmy označení „recursivly definable“ („rekurzivně definovatelný“), „(statement) expressible in S“ („/tvrzení/ vyjádřitelné v systému S“) apod.

Je-li číslo vyjádřitelné v systému S, pak obrazně řečeno „fyzicky“ v systému je. Systémem se zde ovšem nemyslí množina dokazatelných formulí, ale formální systém obsahující predikátovou logiku 1. řádu a aritmetiku, který použil Gödel.

Že ve výše uvažovaném systému není žádný paradox, je úhelný kámen matematické logiky, který do základu zasadil Gödel. Konstruoval svou nerozhodnutelnou větu diagonální metodou jako před ním Jules Richard svůj paradox, a navíc dbal, aby všechny kroky vedoucí k jejímu vyjádření byly rekurzivní. Pak náhle uviděl, že za předpokladu bezespornosti není ta věta paradoxní jako Richardova, ale pravdivá. Takže rekurze (mechanická vyvoditelnost) není totéž, co důkaz. Důkaz dělá důkazem (nedefinuji, chci pouze rozlišit dva pojmy) předpoklad bezespornosti.

Ve snaze odstranit z jazyka paradoxy využil krátce po Gödelově objevu jeho přítel Alfred Tarski myšlenky, jež k objevu vedly. Tarského postup, jak známo, hierarchizuje jazyk. Z reakce matematických logiků pokud jde o paradoxy soudím, že chápou Gödelův objev jako způsob, jak „vidět“ skutečnost bez paradoxů, čili na rozdíl od Tarského matematičtí logikové hierarchizují ontologii.

Diskuse o Gödelových výsledcích je dlouhodobě živá a vzrušující. Ačkoli RNDr. Petr Hájek ve svém neobyčejně inspirujícím článku „Matematik a logik“ napsal, že „filozofické zhodnocení …Gödelových výsledků… nemohu než přenechat jiným“, přála bych si, aby si to ještě rozmyslel.

RNDr. Blažena Švandová