mff2024mff2024mff2024mff2024mff2024mff2024

Aktuální číslo:

2024/3

Téma měsíce:

Elektromobilita

Obálka čísla

Mechanická vyvoditelnost, formulovatelnost, dokazatelnost

(K článku Gödel a paradoxy, Vesmír 75, 466, 1996/8)
 |  5. 11. 1996
 |  Vesmír 75, 629, 1996/11

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á

OBORY A KLÍČOVÁ SLOVA: Logika
RUBRIKA: Diskuse

O autorech

Petr Hájek

Blažena Švandová

Doporučujeme

Jak to bylo, jak to je?

Jak to bylo, jak to je? uzamčeno

Ondřej Vrtiška  |  4. 3. 2024
Jak se z chaotické směsi organických molekul na mladé Zemi zrodil první život? A jak by mohla vypadat jeho obdoba jinde ve vesmíru? Proč vše živé...
Otazníky kolem elektromobilů

Otazníky kolem elektromobilů uzamčeno

Jan Macek, Josef Morkus  |  4. 3. 2024
Elektromobil má některé podstatné výhody. Ale samotné vozidlo je jen jednou ze součástí komplexního systému mobility s environmentálními dopady a...
Návrat lidí na Měsíc se odkládá

Návrat lidí na Měsíc se odkládá uzamčeno

Dušan Majer  |  4. 3. 2024
Tragédie lodi Apollo 1 nebo raketoplánů Challenger a Columbia se již nesmí opakovat. Právě v zájmu vyšší bezpečnosti se odkládají plánované cesty...