o nloderní logice, metamatematice a logice dokazatelnosti*

o nloderní logice, metamatematice a logice dokazatelnosti* Petr Hromek čtenář právě dočetl (anebo nedočetl a rovnou nalistoval tuto

stránku) Smullyanovu populární knihu věnovanou zkoumání podivného kontinentu, jímž je logika a metamatematika. Protože tyto zajímavé oblasti moderního myšlení nejsou podle mého názoru příliš známé a protože tato knížka není určena čtenářům specialistům, ale spíše zvídavým amatérům, dovoluji si na její závěr připojit pár poznámek.

o Kurtu Godelovi Aniž to čtenář možná ví, phběh Smullyanovy knihy se nejméně dvěma způsoby dotýká také naší vlasti. Za prvé, Kurt Godel, hlavní protagonista knížky, logik a matematik známý po celém světě,je totiž naším spoluobčanem - narodil se 28. dubna 1906 v Brně v Pekařské ulici číslo 5 (v roce 1915 se spolu se svými rodiči přestěhoval do Pellicovy ulice 8a). Za druhé, kniha se nedotýká naší vlasti jen díky této historické náhodě, ale také proto, že do jejího děje zasáhli také čeští logikové. Avšak zpět ke Godelovi. V Brně Kurt Godel navštěvoval ně­ meckou základní školu a německé reálné gymnázium, kde měl na vysvědčení pouze jednu známku horší než jedničku kupo• Za cenné rady a připomínky děkuji dr. Vítězslavu Švejdarovi.

284

divu právě z matematiky - a bydlel zde až do svých univerzitních studií ve Vídni, která nastoupil v roce 1924. V roce 1931, tj. ve vě­ ku 251et, publikoval svoji slavnou práci o neúplnosti fonnálních matematických systémů (práce se původně vztahuje k systému A. N. Whiteheada a Bertranda Russella vyloženém v třísvazko­ vém díle Principia Mathematica). Nejznámější výsledek se týká neúplnosti aritmetiky a čtenář se o něm populární fonnou doče­ tl právě v této knížce. Po této práci se Godel věnoval axiomatické teorii množin a problému filosofických základů matematiky. V roce 1940 se mu podařilo spolu s manželkou Adélou krkolomnou cestou přes Lotyšsko, Litvu, Rusko, Čínu a Japonsko uprchnout do USA. Tam našel Godel - spolu s mnoha jinými uprchlíky před Hitlerem - nový domov. V průběhu druhé svě­ tové války se tak v Americe sešla řada význačných evropských intelektuálů. Jako příklad uvedeme významného polského logika Alfreda Tarského, rakouského filosofa Rudolfa Carnapa (před válkou Carnap působil v Praze) a Alberta Einsteina, který byl v USA nejbližším přítelem Kurta Godela. S Einsteinem Godel sdílel rovněž zaměstnání ve známém princetonském Ústavu pro vyšší studia a věnoval se zde mimo jiné interpretaci teorie relativity. Originální myslitel Kurt Godel však kromě pronikavého logického a matematického nadání dostal do vínku rovněž slabší psychickou povahu. Trpěl depresemi a hypochondrickými záchvaty, kvůli nimž často přerušoval výuku na akademických institucích. Po hospitalizaci nemocné manželky se jeho stav ještě zhoršil, až vyústil do chorobné podezíravdsti. Géniova smrt byla smutná - zemřel 14. ledna 1978 na podvýživu a vysílení, protože ze strachu, že jej někdo chce otrávit, odmítal stravu. Adéla Godelová jej přežila o tři roky.

o moderní logice Práce Kurta Godela byla "bleskem z čistého nebe" pro logiku a matematiku začátku dvacátého století. K tomu si však musí285

me nejprve něco málo říci o moderní logice. Tradiční logika, tj. logika, jak jí bylo vyučováno od Aristotelových dob přes celou antiku, středověk a novověk, se totiž věnovala něčemu, co bychom mohli pojmenovat jako "nauka o správném myšlení". Za". bývala se tak problematikou, jak vznikají abstraktní pojmy, jak vznikají jednoduché a složené výroky, naukou o jednoduchých vztazích mezi pojmy (naph1dad o nadřazenosti a podřazenosti pojmů, o "rozsahu a obsahu" pojmů apod.) a jednoduchých vztazích mezi výroky, zde zejména tzv. sylogismy. (Sylogismus je jednoduchý úsudek se dvěma předpoklady a závěrem, kde předpoklady vypovídají o vztazích mezi pojmy MaP a pojmy M a S a dokazovaný závěr o vztazích mezi pojmy S a P.) Důle­ žitou součástí tradiční logiky byla rovněž nauka o správné argumentaci. Avšak tato logika, vesměs zpracovaná neformálně, nemohla stačit potřebám moderní exaktní matematiky na jednu stranu se totiž zabývala řadou věcí, které jsou pro matematiku nepodstatné (např. psychologickými aspekty myšlení), na druhou stranu se tím, co je pro matematiku nejdůležitější, tj. naukou o logickém vyplývání a jeho zákonitostech, nezabývala dostatečně obecným a přesným způsobem. Moderní logika se tedy musela nejprve vymanit ze zajetí filosofie a psychologie, a poté začala pracovat novými metodami, zejména exaktními matematickými metodami odtud název "matematická logika". Ústředním tématem moderní logiky se tak - místo "nauky o správném myšlení" - stala "nauka o logickém vyplývání". Ke zrodu takto pojaté moderní logiky přispěli zejména G. Boole, E. Schroder, Gottlob Frege, který v roce 1879 uveřejnil své významné dílko Begriffsschrift (Pojmové písmo) a zejména již zmínění B. Russell a A. Whitehead a později rovněž německý matematik David Hilbert.

o vztahu matematiky a logiky Moderní logika tedy vyvstala z potřeb matematiky, avšak brzy se vytlě1i1a jako samostatný obor bádání. Vztah logiky

286

k matematice nicméně brzy překročil pouze pomocnou roli. Gottlob Frege kupříkladu dospěl k názoru, že matematika není vlastně ničím jiným než logikou. Matematiku obvykle chápeme jako nauku o číslech, trojúhelnících, množinách atd., které existují nezávisle na naší mysli v jakémsi matematickém "nebi". Frege však tvrdil, že všechny tyto matematické objekty nemusí být ve skutečnosti ničím jiným než (byť komplikovaně sestrojenými) čistě logickými pojmy. Frege tak vysvětlil odvěkou záhadu, proč jsou matematická tvrzení nutně pravdivá - jednoduše proto, že se jedná o logické pravdy, tj. pravdy dané logickou strukturou jazyka a světa. Tento názor vešel do dějin pod názvem "logicismus". Poté, co B. Russell nalezl závažnou chybu ve Fregeho systému, logicistickou filosofii matematiky dále rozvíjeli zejména B. Russell a A. Whitehead, kteří značnou část matematiky skutečně vydedukovali z, logiky. Logika však ovlivnila rovněž myslitele uvažující jiným způ­ sobem. David Hilbert sice také přijímal moderní logiku, začal s ní však pracovat jako s čistým formálním jazykem, který nemusí mít žádný "mimojazykový" význam. Na tuto myšlenku přišel Hilbert srovnáním s geometrií. Odvěkým problémem geometrů bylo zjistit, zda Eukleidův pátý axiom (slavný axiom o rovnoběžkách) vyplývá z ostatních axiomů, nebo nikoliv. Teprve Hilbert dokázal, že tento axiom je na ostatních nezávislý. Přijmeme-li tedy pátý Eukleidův axiom, pak vybudujeme eukleidovskou geometrii. Nepřijmeme-li však tento axiom, můžeme budovat jiné typy geometrie, které jsou z matematického hlediska stejně oprávněné. Podle Hilberta tedy otázka, zda eukleidovská geometrie je tou jedinou "pravou" geometrií, nemá žádný dobrý smysl - obě geometrie jsou pouze formálními matematickými systémy. Podle Hilberta tak není tře­ ba převádět matematiku na logiku, ale můžeme ji považovat jednoduše za nějaký formální systém, resp. formální jazyk. Hilbert dále zavedl jiná kritéria "existence" matematických objektů než Frege. (Slovo "existence" píšeme v uvozovkách, protože ať jsou matematické objekty čímkoliv, jistě nejsou stejně existující jako reálné předměty, jimiž jsou stoly,

287

židle nebo třeba tato kniha.) U Fregeho má prioritu otázka, zda určité matematické objekty existují, neboli zda máme k dispozici příslušné čistě logické pojmy. Tato otázka musí být rozhodnuta předem, a je-li zodpovězena kladně, tj. jestliže uvažované matematické objekty skutečně "existují", pak pravdivá tvrzení o těchto objektech musí být navzájem bezesporná. Hilbert jednoduše obrátil pořadí těchto podmínek. Podle něj platí, že kdykoli jsou tvrzení o nějakých objektech navzájem bezesporná, pak tyto objekty "existují", a že každý bezesporný formální systém je smysluplný. Matematikové tak mají naprostou volnost studovat libovolné formální systémy bez ohledu na to, zda jim odpovídá něco "mimo jazyk", tj. zda vůbec existují nějaké užitečné interpretace těchto systémů. Tento názor vešel do dějin pod názvem "formalismus". významnou variantu formalismu představuje tzv. Hilbertův program. Podobně jako se Frege domníval, že celou matematiku lze vyvodit jen z logiky, domníval se Hilbert, že ji lze založit čistě formalistickým způsobem, a podal obecné instrukce, jak postupovat. Nejprve je dle Hilberta zapotřebí rozdělit matematiku na dvě části, na tzv. matematiku reálnou a tzv. matematiku ideální. Toto rozlišení mezi reálnou a ideální matematikou má kopírovat dělení vědecké teorie na experimentální a teoretickou část. Podobně jako teoretické výpočty v nějaké fyzikální teorii nesmí odporovat experimentálním výsledkům, nesmí výsledky ideální matematiky být nikdy ve sporu s reálnou matematikou. Konečně, reálnou matematikou se zde míní tzv. finitární matematika, kam patří především jednoduchá tvrzení jako 2 + 5 =:: 7, 2 + 2 =6, 2145 x 4 578::: 9 819 810 apod. Pro všechna tato tvrzení platí, že jejich pravdivost či nepravdivost lze ověřit pomocí nějakého konečného množství výpočtů. Hilbert dále mezi finitární tvrzení počítá tzv. obecná finitární tvrzení, jako jsou např. aritmetická tvrzení a + b b + a (tj. rozumíme: pro všechna a, b platí. .. ), a x b = b x a (opět: pro všechna a, b ... ) apod. Tvrzení typu a + b = b + a jsou podle Hilberta finitární, protože jsou jen zobecněním tvrzeni jako 4 + 5 =5 + 4,21 + 789 =789 + 21 atd., kde po každém kon288

krétním dosazení dostaneme nějaké pravdivé tvrzení. Omezíme-li se místo matematiky jen na aritmetiku, pakje finitární aritmetika často považována za totéž jako takzvaná primitivní rekurzivní aritmetika. (Někteří matematikové však finitární aritmetiku ztotožňují s ještě slabšími systémy.) Podle Hilberta reálná matematika (tj. finitární matematika) představuje pevný a neproblematický základ. Zbývá tedy dokázat, že metody a výsledky ideální matematiky nemohou být nikdy v rozporu s reálnou matematikou. Opět, omezímeli se na aritmetiku, pak je zapotřebí dokázat, že ideální aritmetika je konzervativní vuči finitární aritmetice. Konečně, P07 žadavkem konzervativnosti rozumíme v případě aritmetiky jednoduše to, že nějaký aritmetický teorém lze dokázat metodami ideální aritmetiky jedině tehdy, jestliže jej lze dokázat metodami finitární aritmetiky. Tolik ve stručnosti k Hilbertovu programu. Jeho detailnější popis by si vyžadoval mnohem větší prostor a k dalším podrobnostem čtenáře odkazujeme na literaturu, kterou doporučujeme v závěru. A právě do této situace zasáhl překvapivým. způsobem Kurt Godel. Jeho větu o neúplnosti lze považovat za dukaz, že matematiku nelze úplně vyčerpat žádným formálním matematickým systémem, tj. nelze ji s žádným formálním systémem ztotožnit. Uvažujeme-li totiž o matematice jako o ideálním matematickém "nebi" (jak si matematiku představují tzv. matematičtí platonikové), v němž zcela nezávisle na nás existují matematické objekty, a jakákoli tvrzení o těchto objektech jsou buď absolutně pravdivá, nebo absolutně nepravdivá, pak Godelovy věty nám říkají, že žádný formální jazyk nemůže úplným způsobem toto "nebe" popsat. Každá taková formalizace je totiž nutně neúplná, neboli vždy lze formulovat (přesněji: v dostatečně bohatých systémech lze formulovat ... ) taková matematická tvrzení, že je pomocí metod příslušného formálního systému nelze dokázat ani vyvrátit. Konečně platí, že metodami finitární aritmetiky nelze dokázat ani bezespornost aritmetiky samotné. Tím je ohrožena i smysluplnost HUbertových kritérií "existence" matematických objektů, a tudíž i kritéria přijatel-

289

nosti některých matematických systémů a teorií. Formalistické filosofii matematiky se různými ústupky podařilo řadě z těchto problémů uniknout, nicméně se zdá, že některé z vysněných cílů Hilbertova programu zmizely nenávratně. Konečně, zbývá zmínit se ještě o intuicionistické filosofii matematiky, kterou založil holandský matematik L. E. 1. Brouwer. Na rozdíl od logicismu, který se snaží vyvodit veškerou matematiku z logiky, a formalismu, který ji považuje za nějaký neinterpretovaný jazyk, intuicionisté matematiku dů­ sledně považují za specifickou tvořivou lidskou činnost, kterou žádným z těchto dvou způsobů nelze adekvátně postihnout. Tomuto pojetí odpovídají rovněž odlišná kritéria "existence" matematických objektů. Nějaký matematický objekt existuje podle intuicionistů pouze tehdy, jestliže jej lze skutečně zkonstruovat. Odpovídajícím způsobem intuicionisté formulují také vlastní kritérium pravdivosti - matematický teorém lze považovat za pravdivý jedině tehdy, jestliže jej lze matematickými metodami (tyto metody však nemusí být formální) skutečně dokázat (v intuicionistickém smyslu hovoříme o konstruktivní dokazatelnosti). Podle intuicionistů tedy matematická pravdivost spadá v jedno s konstruktivní dokazatelností, a tudíž nemohou existovat žádné nepoznatelné matematické pravdy. (Logicisté a formalisté existenci nepoznatelných pravd připouštějí.) Intuicionistická matematika tak nutně musí klást dodateč­ né požadavky na používání některých metod běžných v klasické matematice. Klasická matematika kupříkladu s oblibou používá důkaz sporem, podle nějž k důkazu, že nějaké tvrzení je pravdivé, stačí dokázat, že z negace tohoto tvrzení plyne spor. Intuicionistický důkaz však spočívá v provedení nějaké matematické konstrukce. Důkaz sporem by pak znamenal, že ze skutečnosti, že nějaká matematická konstrukce (konstrukce negace dokazovaného tvrzení) je sporná, plyne, že nějaká docela jiná konstrukce je uskutečnitelná. To však není nijak zaručeno! Tudíž, intuicionističtí matematikové obecnou platnost důkazu sporem neuznávají. 290

Přestože intuicionističtí matematikové mají řadu výhrad vů­ klasické matematice a logice a přestože Brouwer považoval za nemožné formulovat "intuicionistickou" logiku, jeho žák Arend Heyting se o to pokusil. Víme, že sémantika klasické logiky vychází z pojmu pravdivosti. Heyting však ukázal, že pro sémantiku intuicionistické logiky je vhodnější, vyjdeme-li z pojmu dokazatelnosti. Jestliže p a q jsou nějaká dvě tvrzení intuicionistické matematiky, pak důkaz tvrzení p&q se musí skládat z konstruktivního důkazu tvrzení p a konstruktivního důkazu tvrzení q. (Příslušná podmínka pro klasickou logiku by zněla: Tvrzení p&q je pravdivé právě tehdy, jestliže jsou pravdivá zároveň obě tvrzení pi q. Ostatní formulace si čtenář jistě doplní sám.) Podobně, důkaz tvrzení pvq musí obsahovat konstruktivní důkaz tvrzení p nebo konstruktivní důkaz tvrzení q, dále dů­ kaz tvrzení p:::>q musí spočívat v nějaké metodě, jak konstruktivní důkaz p přeformulovat na konstruktivní důkaz q, a konečně důkaz tvrzení ~p spočívá v důkazu, že konstrukce, která má dokázat tvrzení p, je sporná. Této sémantice intuicionistické logiky se dnes říká "Brouwerova-Heytingova-Kolmogorovova sémantika". Její podrobná interpretace je však poměrně obtížná a byla podána řada velmi různých interpretací. Pro nás je však zajímavé to, že interpretacÍ Heytingovy logiky se zabýval také Kurt Godel a právě v souvislosti s intuicionistickou logikou byla poprvé zmíněna logika dokazatelností. Nicméně od Godelovy formulace v jeho článku z roku 1933 vedla k logice dokazatelnosti, jak ji známe dnes, ještě dlouhá cesta. či

o logickém vyplývání, materiální implikaci a striktní implikaci Logické systémy zavedené Fregem, Russellem, Whiteheadem, Hilbertem a jinými pracují s tzv. materiální implikací, tj. nám dobře známou "obyčejnou" implikací. Ppokusíme-li se však pomocí této implikace formalizovat pojem logického vyplývání, můžeme se dostat do problémů. 291

Materiální implikace p:::Jq si totiž nijak nevšímá toho, co ří­ kají její oba členy, ale pouze jejich pravdivostních hodnot. Považujeme-li platné "logické vyplývání" jednoduše za vztah daný pravdivou materiální implikací, tj. za něco, co je vyčer­ pávajícím způsobem určeno nějakou pravdivostní tabulkou, pak je vše v pořádku. Americký filosof a logik C. I. Lewis se nicméně domníval, že skutečný pojem vyplývání nelze redukovat tímto způsobem, ale že mezi dvěma výroky (resp. mezi nějakou množinou výroků a jedním samostatným výrokem) logické vyplývání platí jedině tehdy, jestliže druhý výrok lze opravdu vyvodit z prvního výroku (resp. z dané množiny výroků). Máme-li například výroky p, p:::Jq a q, pak výrok q skutečně můžeme pomocí pravidla'modus ponens vyvodit na základě výroků p a p:::Jq. To lze pomocí materiální implikace zapsat jako tvrzení (p&(P:::Jq) ):::Jq. Skutečnost, že toto odvození lze provést, tak odpovídá jiné skutečnosti, tj. že formule (p&(P:::Jq»:::Jq je tautologií. Avšak výrok q nelze vyvodit na základě výroku q samotného, protože to je důkaz kruhem, který ve skutečnosti nic nedokazuje! Nicméně - příslušná formule q:::Jq je také tautologií I Řečeno ještě jinak: Přirozený jazyk, jak jej běžně používáme, je jistě vynikajícím nástrojem k obecnému dorozumívání, má však z hlediska logiky jednu drobnou nevýhodu - totiž je víceznačný. Řada výrazů, které běžně používáme, tak má několik různých významů. Jako př11dad lze uvést výrazy "oko", "můs­ tek", "kohoutek", "motýlek" apod. Víceznačné však mohou být také jiné výrazy, dokonce i spojka "jestliže, pak", s jejíž pomocí běžně převádíme implikaci p:::Jq do slovní podoby. N apř11dad ve větě "Jestliže je Petr v Olomouci, pak je v české republice" tato spojka rozhodně nemůže být materiální implikací! Kdyby tomu tak bylo, dostali bychom následující absurdní úsudek: Jestliže je Petr v Olomouci, pak je v České republice. Jestliže je Petr v Oxfordu, pak je ve Velké Británii. Tudíž: Jestliže je Petr v Olomouci, pak je ve Velké Británií, nebo jestliže je Petr v Oxfordu, pak je v České republice.

292

Označme výrok "Petr je v Olomouci" jako p, výrok "Petr je v České republice" jako q, výrok "Petr je v Oxfordu" jako r a konečně výrok "Petr je ve Velké Británií" jako s. Pak tento úsudek odpovídá formuli «p::::>q)&(r::::>s) )::::>( (p::::>s )v( r::::>q», která je tautologií, jak si čtenář může snadno ověřit. Ne každý výskyt výrazu "jestliže, pak" tedy vyjadřuje materiální implikaci. Tj. naopak: materiální implikace nemusí správně formalizovat všechny významy "vyplývání", všechny významy spojky "jestliže, pak" apod. Lewis se tedy domníval, že ;,správný" pojem vyplývání je třeba formalizovat jinak. V klasické logice totiž platí tautologie -p::::>(p::::>q) (slovy: je-li p nepravdivý výrok, pak z něj "plyne" jakýkoli výrok) a p::::>(q::::>p) (slovy: je-li p pravdivý výrok, pak "plyne" z libovolného výroku), a interpretujeme-li obě tautologie jako tvrzení o vyvoditelnosti, můžeme skutečně dojít k některým nepříjemným důsledkům. Jelikož tautologie p::::>(q::::>p) a -p::::>(p::::>q) mohou mít "paradoxní" důsledky, pojmenoval je Lewis jako "paradoxy implikace" - píšeme v uvozovkách, protože se o skutečné paradoxy nejedná. (Někdy je k těmto "paradoxům" počítána rovněž formule (p::::>q)v(q::::>p ), tj. slovně, že pro libovolné dva výroky p a q platí jedna či druhá implikace neboli jedno či druhé" vyplývání".) Lewis tak poukázal na pojem, který podle jeho názoru nelze adekvátně formalizovat materiální implikací. To ale zdaleka neznamená, že se jí musíme vzdát. Materiální implikace je totiž v řadě jiných situací tím nejvhodnějším, logickým pojmem, který máme k dispozici. K tomu však musíme implikaci chápat správným způsobem, tj. jako složený podmínkový výrok, nikoli jako tvrzení, že jeden výrok lze deduktivně vyvodit z druhého výroku. Předpokládejme například, že p::::>q vyjadřuje výrok "Jestliže bude pršet, pak si vezmu deštník". Abych dostál svému slibu (aby tato implikace byla pravdivá), pak v případě, že prší, musím si vzít deštník. Jestliže však neprší, co musím učinit, abych dostál svému slibu, tj. aby implikace p::::>q byla'pravdivá? Musím si deštník vzít nebo nikoliv? Z pravdivostní tabulky víme, že implikace je nepravdi-

293

vá jedině tehdy, jestliže výrok p je pravdivý a výrok q nepravdivý. Tj. svůj slib mohu porušit pouze tak, že v situaci, kdy skutečně prší, si nevezmu deštník. Nicméně, není-li první výrok pravdivý, pak nemám žádnou možnost, jak implikaci p::>q falzifikovat. Neprší-li, musíme výrok "Jestliže bude pršet, pak si vezmu deštník" považovat za pravdivý nehledě na to, zda jsem si deštník vzal nebo nikoliv. Chápeme-li materiální implikaci tímto způsobem, pak na tautologiích p::>(q::>p) a -p::>(p::>q) skutečně není nic paradoxního. Pro potřeby definice "správného" pojmu logického vyplývání, tj. ve smyslu vyvoditelnosti, nikoli ve smyslu materiální implikace, tak Lewis zavedl nový pojem, tzv. "striktní" implikaci, kterou zapsal pomocí znaku ,,-3". Lewis definuje, že striktní implikace p-3 q platí pouze tehdy, jestliže nen( možné, aby p byl pravdivý a q nepravdivý výrok, neboli jestliže tato implikace platí nutně. Striktní implikace již definuje "logické vyplývání" o něco korektněji a formule -p -3 (p-3 q), p-3 (q -3 p), (p-3 q)v( q -3 p) apod. skutečně v Lewisových systémech nejsou tautologiemi. Konečně, také spojku "jestliže, pak" ve výše uvedeném úsudku o Petrovi, který je někdy v Olomouci a někdy v Oxfordu, můžeme formalizovat pomocí striktní implikace. A vskutku, není možné, aby Petr byl v Olomouci a zároveň nebyl v České republice. Naopak,je možné, že je v Olomouci a není ve Velké Británii. Jinými slovy, ani formule «p-3q)&(r-3s»::>«p-3s)v(r-3q» není v Lewisových systémech tautologií. Nicméně v roce 1936 předložil Alfred Tarski novou definici pojmu logického vyplývání pomocí materiální implikace. Jedná se o jeho slavnou tzv. modelově-teoretickou definici,jejíž náznaky lze vystopovat k Bernardu Bolzanovi až do devatenáctého století. V moderních učebnicích logiky nalezneme téměř univerzálně právě tuto definici. Naproti tomu většina Lewisových systémů dnes představuje jen historickou kuriozitu, a dokonce i nejznámější Lewisovy systémy S4 a Ss byly později znovu objeveny nezávisle na Lewisovi. (Lewis sám však systémy S4 a Ss nepovažoval za přI1iš důležité a prefero-

294

nimi systém Sz.) Ostatně, i toto značení Lewisových je pozdějšího data. Důležitá je pro nás však skuteč­ nost, že skrze Lewisovu práci jsme dospěli k moderní modální logice. val

před

systémů

o modální logice Mnozí filosofové a logikové kritizovali systémy striktní implikace především kvůli pojmům nutnosti a možnosti, které Lewis nikdy uspokojivě nedefinoval. Lewis totiž se svými systémy pracoval výhradně syntakticky, tj. jako s čistými formálními jazyky bez příslušné mimojazykové interpretace. Teprve koncem padesátých let dvacátého století byly díky logikům Jaako Hintikkovi, Arthuru Priorovi a zejména Saulu Kripkemu nalezeny uspokojivé sémantické definice těchto pojmů. Řekne­ me, že výrok p je v nějakém světě w nutně pravdivý, jestliže je pravdivý ve všech světech, které jsou možnými alternativami vůči světu w. Místo formulace, že nějaký svět je možnou alternativou vůči světu w, se častěji používá formulace, že tento svět je dosažitelný ze světa w. Podobně řekneme, že výrok p je ve světě w možná pravdivý, jestliže je pravdivý v alespoň jednom světě, který je možnou alternativou vůči w, resp. který je dosažitelný ze světa w. Na první pohled se zdá, že tyto definice byly nalezeny za cenu zavedení nového obtížně uchopitelného pojmu, tj. pojmu "možný svět". Ve skutečnosti se ukázalo, že s pojmem možných světů se pracuje poměrně snadno a že k fungující modální logice stačí definovat možné světy jako cokoli, vůči čemu nabývají výroky pravdivostní hodnoty. Roli možných světů tak mohou plnit různé věci a otázkou, čím tyto světy jsou, se samotní logikové nemusejí příliš trápit. (Existuje nicméně jedno vlivné pojetí, podle nějž jsou možné světy "množinami výroků". Každý možný svět je tedy jakousi vyčerpáva­ jící a bezespornou "historií" světa. Právě jedna z těchto historií je faktuálně pravdivá, tj. vypovídá o tom, jak je tomu 295

ve skutečnosti. Tato historie představuje aktuální svět. Jiné historie vypovídají o jiných možných světech, tj. o jakýchsi alternativách vůči našemu světu.) Zásadní roli v sémantice modální logiky tedy hraje pojem dosažitelnosti. Nemáme zde však pouze jeden pojem, ale řadu různých pojmů a v návaznosti na to řadu různých modálnfch systémů a různých pojetí nutnosti. Můžeme například požadovat, aby žádný možný svět nebyl dosažitelný sám sobě. Dostaneme jeden modální systém a jedno pojetí nutnosti. Na druhou stranu, můžeme požadovat, že každý svět musí být dosažitelný sám sobě. Dostaneme tak jiný systém a jiné pojetí nutnosti. Podobně můžeme definovat, že pokud je světu w dosažitelný svět w', pak tento vztah musí platit také obráceně, tj. že světu w' je dosažitelný svět w. Dostaneme opět jiný systém a jinou nutnost. A tak dále. Místo jednoho sy~tému modální logiky jsme tedy získali velké množství různých systémů. (A možná až příliš mnoho :- to je také jeden z důvodů, proč někteří filosofové modální logiku odmítají.) Tato rozmanitost modální logiky však má jednu výhodulze ji totiž interpretovat celou řadou různých způsobů. Jedna z interpretací je například temporální. V tomto pojetí před­ stavují možné světy různé časové okamžiky. Místo tvrzení, že světu w je dosažitelný svět w', pak řekneme, že časový okamžik t předchází okamžik ť. Konečně tvrzení, že výrok p je ve světě w nutný, odpovídá tvrzení, že výrok p je pravdivý ve všech časových okamžicích, které následují za okamžikem t. Pak můžeme exaktně studovat různá filosofická pojetí času, závislosti pravdivosti výroků na čase apod. Dále můžeme jiným způsobem interpretovaťpojem nutností. Místo s výrokem "nutně p" lze pracovat s výrokem "závazně p". V tomto pojetí jsme nutnost nahradili pojmem příkazu, tj. nějaké závazné normy. (Výroku "možná p" by pak odpovídal výrok "je povoleno p".) Nyní se dá definovat logika, s jejíž pomocí lze exaktně studovat normativní systémy, např. právní systémy, popř. etické systémy. V tomto případě řekneme, že jsme pojmu nutnosti dali deontickou, resp. normativní inter-

296

pretaci. Konečně můžeme výrok "nutně p" interpretovat jako "osoba x věří p", dále jako "osoba x ví, že pOl apod. Nyní řekne­ me, že jsme podali epistemickou interpretaci - musíme však poznamenat, že v tomto případě dostaneme nikoli jeden ope~ rátor "nutnosti" B, ale pro každou osobu x, y, z, ... zvlášť jeden operátor Bx, By, Bz, ... V knize jsme pracovali převážně s epistemickou interpretací operátoru "B" a vystačili jsme většinou s jednou osobou (resp. s jedním systémem). Podobné další filosofické interpretace modální logiky by zřejmě nebraly konce. Významné aplikace má však modální logika také v teoretické informatice. "Možné světy" můžeme tentokrát považovat za jednotlivé stavy počítače, který zpracovává zadaný program. Jestliže jako "P" označíme uvažovaný program, pak zápisem "Pq" rozumíme tvrzení "po provedení programu P je pravdivé tvrzení q". Hovoříme zde však o tzv. nedeterministických programech, tj. provedení programu P nemusí nutně vést k jednomu konkrétnímu výsledku, ale může mít různé výsledky. Příslušným zpfisobem dále reinterpretujeme rovněž pojem dosažitelnosti. Místo tvrzení, že světu w je dosažitelný svět w', tak řekneme, že po stavu x počítače (při provádění programu P) následuje stav x'. Tvrzení "nutně Pq", tj. že provedení programu P pokaždé vede k situaci, v níž je pravdivé tvrzení q, zapíšeme jako ,,[P]q". Podobně tvrzení "možná Pq", tj. že provedením programu P mfižeme dojít k situaci, v níž je pravdivé tvrzení q, zapíšeme jako ,,(P)q". Tato logika - známá pod názvem "dynamická logika" - dále umožňuje programy rfizně propojovat. Tím dostaneme - podobně jako v případě epistemické interpretace - celou řadu operátoru "nutnosti" a "možnosti" - pro každý jednotlivý program P je~ den operátor nutnosti fP] a jeden operátor možnosti (P). Provedení programu P, za nímž následuje provedení programu Q, dále zapíšeme jako "P;Q" a konečný počet opakovaných provedení původního programu P jako "P*". Uvažujme jednodu-' chý příklad, formuli (P*)q=(qv(P;P*)q). Tato formule nám ří­ ká, že ke stavu, kdy po konečném počtu provedení programu P platí q, lze dospět buď tak, že již máme k dispozici stav, kdy

297

platí q, nebo tak, že můžeme program P provést nejprve jednou a pak opakovaně tak dlouho, dokud nedostaneme stav, kdy platí q. Důležité věty o úplnosti aritmetické interpretace dynamické logiky dokázal český logik Petr Hájek. Aritmetickou interpretací přitom rozumíme takovou interpretaci, kdy operátory nutnosti v dynamické logice, tj. např. [P], [Q] apod., . považujeme za operátory dokazatelnosti v rámci aritmetiky. Tak jsme se od úvah o logicích různých typů a o metafyzické nutnosti a možnosti dostali až ke komplikovaným úvahám týkajícím se interpretace počítačových programů a teoretické informatiky. Neexistuje tedy pouze velké množství různých modálních logik, ale rovněž jejich různých filosofických a jiných interpretací. Je vskutku podivuhodné, že takovou rozmanitost lze zkonstruovat na základě jen několika málo jednoduchých pojmů.

o modální logice dokazatelnosti Již jsme se zmínili o striktní implikaci a o tom, že úspěšně řeší "paradoxy" materiální implikace. Bohužel však neřeší všechny problémy. V Lewisově systému můžeme odvodit napříkla4 následující formule: -Mp-3 (p-3 q) (tj. slovně: je-li p nemožné, pak z p plyne jakýkoli výrok q) a Np-3 (q-3 p) (slovně: je-li p nutné, pak plyne z jakéhokoli výroku q). (Poznámka: "Mp" zde znamená "možná p" a "Np" "nutně p".) Z těchto a z jiných důvodů nelze Lewisovu striktní implikaci považovat za adekvátní formalizaci vyplývání ve smyslu matematické dokazatelnosti. Jako uspokojivější řešení byla objevena modální logika dokazatelnosti. Ze Smullyanovy knihy dobře víme, že pro modální logiku dokazatelnosti jsou podstatné tři věci: (1) Godelovy věty o neúplnosti, (2) teorie modalit, (3) metody, jimiž lze dosáhnout sebereference. Avšak tyto teoretické poznatky vznikaly v různém čase. Modální logika dokazatelnosti tedy také vznikala postupně, po drobných krůčcích, splétala se z různých 298

proudů a teprve 40 let po objevti Godelových vět poprvé spatřila světlo světa. Na rozdíl od modální logiky tedy nemůžeme

poukázat na žádného jejího zakladatele, jako jsme se v přípa­ dě modální logiky mohli jednoznačně odvolat na C. 1. Lewise. Místo jednoho zakladatele totiž máme v tomto případě zakladatelů několik, a dokonce ze tří různých států. Mezi nejdůležitější protagonisty samozřejmě patří Kurt . Godel, který poskytl první a třetí komponentu, tj. věty o neúplnosti a aritmetické metody dosažení sebereference. uetí komponentou logiky dokazatelnosti je modální interpretace pojmu dokazatelnosti. Již jsme se zmínili, že Godel skutečně zvažoval modální interpretaci dokazatelnosti a že na tuto myšlenku přišel prostřednictvím úvah o interpretaci intuicionistické logiky. Ve svém článku z roku 1933 Godel píše: Heytingovu výrokovou intuicionistickou logiku můžeme interpretovat prostřednictvím pojmů obyčejné výrokové logiky a pojmu "p je dokazatelné tvrzení" (píšeme Bp). Stačí, při­ jmeme-li následující systém axiomů: (1) Bp::rp (2) Bp::r(B(p::rq)::rBq) (3) Bp::rBBp ... a nové odvozovací pravidlo: Jestliže platí A [tj. je-li A ně­ jaký teorém], pak odtud můžeme vyvodit BA. Godelem navržený systém odpovídá Lewisovu systému 54' Axiom (1) nám Ťl'ká, že jestliže je nějaké tvrzení dokazatelné, pak je pravdivé. Jinými slovy: Tento axiom nám udává překla­ dová pravidla mezi intuicionistickou a klasickou matematikou. Godel totiž ve své interpretaci Heytingovy logiky vychází z předpokladu, že je-li nějaké tvrzení dokazatelné, tj. "pravdivé" v intuicionistickém smyslu, pakje pravdivé rovněž v obyčejném smyslu, tj. je teorémem klasické matematiky. Zbývající dva axiomy se pak věnují vlastnostem pojmu dokazatelnosti. Axiom (2) říká, že je-li dokazatelné tvrzení p a zá299

roveň

dokazatelná implikace p:::>q, pak je dokazatelné také tvrzení q,dále axiom (3), že je-li dokazatelné tvrzení p, pak lze dokázat, že toto tvrzení je dokazatelné, a konečně Godelovo odvozovací pravidlo (pravidlo nutnosti) nám umožňuje vyvodit, že jestliže formule A je teorémem, pak tato formule je dokazatelná. Tyto axiomy jsou čtenáři již dobře známy. MůŽeme ještě poznamenat, že dokazatelnost platí pouze "v jednom směru", tj. že neplatí žádná obdoba axiomu (3) pro "nedokazatelnost". Jinými slovy: Není-li tvrzení p dokazatelné, nelze obecně vzato dokázat, že toto tvrzení není dokazatelné. Pojem dokazatelnosti je zde míněn v "absolutním" smyslu, a nikoli v rámci nějakého konkrétního systému. Avšak s touto interpretací pojmu dokazatelnosti jsou potíže. Uvažujme totiž nějaký konkrétní systém, např. systém Peanovy aritmetiky, a dejme tomu, že Godelův systém vyjadřuje zákonitosti dokazatelnosti v feanově aritmetice. Pak jestliže jsou teorémy všechna tvrzení Bp:::>p, musí být teorémem také tvrzení Bbl.. Podle Godelova odvozovacino pravidla dále platí B(Bbl.). Nicméně formule Bbl. je ekvivalentní s formulí -Bl.. Mluvíme-li o Peanově aritmetice, pak -Bl. nám říká, že Peanova aritmetika je bezesporná. Konečně, B(Bbl.) je ekvivalentní s B( - Bl.). Tím jsme dostali tvrzení, že v rámci Peanovy aritmetiky je možno dokázat bezespornost Peanovy aritmetiky. Právě to však na základě Godelových vět není možné! To znamená, že Godelem navržený systém není ještě vhodnou logikou dokazatelnosti. Abychom našli příčinu, proč tento systém selhává, musíme si blíže ukázat, co je vlastně formální dokazatelností míněno. Formální dokazatelnost, tak jak s ní pracoval Godel ve své objevitelské práci z roku 1931, totiž není žádným primitivním (tj. jednoduchým a dále neanalyzovatelným) pojmem. Zopakujme si ve stručnosti, jak formální dokazatelnost definujeme. Víme již, že nejprve je nutno zavést číslování všech výrazů příslušného jazyka a že po očíslování výrazů očíslujeme také všechny formule příslušného formálního systému. Místo o vlastnostech tvrzení (tj. nějakých pravdivých či nepravdi300

vých sentencí systému) tak můžeme hovořit o vlastnostech příslušných čísel. K některým tvrzením systému existují důka­ zy (těmto tvrzením řľkáme dokazatelná tvrzenľ) a k některým nikoliv. Uvažujme tvrzení q a přidělme mu číslo, které označí­ me jako #q. Jestliže existuje důkaz tvrzení q, pak tento důkaz je nějaká posloupnost p tvrzení Pl' P2' ... , Pn> která začíná axiomy systému (tj. Pb P2 apod. jsou axiomy systému), a končí tvrzením q (neboli: Pn = q), přičemž všechny členy této posloupnosti musí být odvozeny korektním způsobem prostřed­ nictvím povolených odvozovacích pravidel systému. Příslušné posloupnosti p můžeme rovněž přidělit číslo, které označíme jako #p. Godel nyní ukázal, že v daném formálním systému, je-li jeho jazyk dostatečně bohatý, je možno exaktním způso­ bem zavést formuli Důk(x,y), která má tu vlastnost, že posloupnost p je důkazem tvrzení q tehdy a jen tehdy, když formule Důk( #p,#q) je teorémem příslušného formálního systému. Máme-li definovánu funkci Důk(x,y), pak pojem formální dokazatelnosti definujeme uvnitř formálního systému jednoduše jako 3xDůk(#X,#q), tj. slovně "existuje taková posloupnost x, která je důkazem tvrzení q". V našem systému tedy Bq znamená totéž jako 3xDůk(#x,#q). Avšak existenční kvantifikátor má nekonstruktivní povahu. To znamená, že přestože nějaké tvrzení 3xDůk(#x,#q) je v daném systému pravdivé, nemusíme být schopni sestrojit jeho formální důkaz v rámci tohoto systému. V takovém přípa­ dě však nemusíme být schopni v rámci systému dokázat ani tvrzení 3xDůk(#x,#q):::Jq, tj. Bq:::Jq, a to přestože pro konkrétní posloupnost p je důkaz formule Důk(#p,#q):::Jq triviální. Godelův axiom (1) ať v "absolutním" smyslu vyhovuje, či nikoliv - se tedy určitě nehodí k systematizaci formálního pojmu dokazatelnosti. Nicméně v některých případech jsme schopni sestrojit důkaz tvrzení 3xDůk(#X,#q):::Jq, tj. tvrzení Bq:::Jq, a tudíž platí B(Bq:::Jq). V takovém případě dále platí, že příslušné tvrzení q je dokazatelné, tj. Bq. Právě tento poznatek dokázal v roce 1954 Martin H. LOb v docela jiné souvislosti (v návaznosti na problém předložený 301

Leonem Henkinem) a dnes je znám pod názvem Lobova vě­ ta. Ani objev Lobovy věty v roce 1954 (publikován byl v roce 1955) však ještě nevedl ke vzniku modální logiky dokazatelností. Tento systém tak vznikal postupně v průběhu šedesátých a sedmdesátých let dvacátého století na třech různých místech: v USA, Itálii a v Holandsku. V USA se poprvé objevila LObova formule, tj. formule B(Bp~p)~Bp. Uvedl ji TImothy Smiley (avšak na tuto formulí jej prý upozornil Saul Kripke), nikoli ovšem v souvislosti s logikou dokazatelnosti, ale kupodivu ve spojitosti s úvahami o neúplnosti určitých formálních systémů etiky. Mezi hlavní průkopníky logiky dokazatelnosti v USA pak patřili Saul Kripke, George Boolos, Craig Smorynski, Robert Solovay, Robert Goldblatt, Warren Goldfarb a jiní. Skutečnost, že Godelovu druhou větu lze snadno odvodit jako důsledek LObovy věty (a naopak), objevil Kripke pravděpodobně již' v roce 1966, tento výsledek však nepublikoval. Kripkův důkaz byl uveřejněn až v roce 1974 v knize George Boolose a Richarda Jeffreyho Computability and Logic. V roce 1973 Kripke dokázal věty o korektnosti a úplnosti logiky dokazatelností vůči třídě všech tranzitivních a obráceně fundovaných struktur. (Upozorňujeme, že Raymond Smullyan v knize nepoužívá výraz "obráceně fundovaná" struktura, ale výraz "terminální" struktura. Tento výraz však není běžně používán.) Připomínáme, že modální strukturou rozumíme něja­ kou třídu možných světů a na ní definovanou relaci dosažitelnosti - zde tedy hovoříme o tranzitivní a obráceně fundované (resp. "terminální") relaci dosažitelností. Jiný směr výzkumu, který také vedl ke vzniku logiky dokazatelnosti, inicioval v roce 1972 Roberto Magari. Stalo se tak údajně poté, co na kongresu v Santa Margherita Ligure vyslechl příspěvky, které dle jeho názoru hrubě dezinterpretovaly význam Godelových vět o neúplnosti. Spolu s ním se v Itálii na tomto výzkumu dále podíleli především Franco Montagna, Giovanni Sambin, Silvio Valentini, Claudio Bernardi a jiní. Na rozdíl od svých amerických kolegů dospěli italští logikové k 10302

· gice dokazatelnosti prostřednictvím algebraických systému, které Roberto Magari pojmenoval jako "diagonalizovatelné algebry" a později jako "Lobovy algebry". Tyto algebry v podstatě představují algebraický model logiky dokazatelnosti. Konečně, v Holandsku ke vzniku logiky dokazatelnosti při­ spěli D. H. de Jongh, Henrik Barendregt, Krister Segerberg, Hans van Maaren a další. D. H. de Jongh dokázal například, že axiom Bp:::>BBp lze v logice dokazatelnosti vyvodit z ostatních axiomu (v kapitole 18 tento poznatek Smullyan pojmenovává jako "Kripkeho, de Jonghova a Sambinova věta") a spolu s M. Lobem formuloval v roce 1974 hypotézu o aritmetické úplnosti logiky dokazatelnosti (hypotézu nezávisle na nich formulovali v USA Saul Kripke a George Boolos). Tuto očekávanou hypotézu o úplnosti aritmetické interpretace logiky dokazatelnosti dokázal v roce 1975 (dukaz byl publikován v roce 1976) Robert Solovay. Mimo kripkovskou sémantiku (tj. interpretaci prostřednictvím třídy všech tranzitivních a obráceně fundovaných modálních struktur) tedy existuje také aritmetická sémantika logiky dokazatelnosti, kterou mužeme zavést následujícím zpfisobem: Uvažujme funkci *, která všem formulím logiky dokazatelnosti přiřadí nějakou uzavřenou formuli Peanovy aritmetiky (neboli něja­ kou sentenci Peanovy aritmetiky). Této funkci říkáme aritmetická realizace, platí-li pro ni podmínky (1) 1.* :::: 1. (tj. aritmetickou realizací logické nepravdy je nějaké nepravdivé aritmetické tvrzení, např. 1 + 1 = 3), (2) (p:::>q)* p*:::>q* (realizaci implikace lze převést na implikaci dvou aritmetických tvrzení, kde prvním členem je realizace prvního členu formule a druhým členem realizace druhéhočlt}nu formule) a (3) (Bp)* :::: B(p*) (tj. realizací formule Bp je tvrzení, že realizace p* je nějaká dokazatelná aritmetická formule). Řekneme, že modální formule A je apodiktická, jestliže její realizací A * je pokaždé nějaká dokazatelná aritmetická formule. Sólovayova věta nám říká, že každá apodiktická modální formule A je teorémem logiky dokazatelnosti, neboli jinými slovy, že není-li nějaká modální formule A teorémem logiky dokazatelnosti, 303

pak A není apodiktická, tj. její realizací A>I< nemusí být pravdivé aritmetické tvrzení. V té době byla modální logika dokazatelnosti definitivně na světě. Tím byl také dán dohromady materiál, na němž George Boolos založil svoji knihu The Unprovability oj Consistency. Na knize začal Boolos pracovat ihned poté, co mu Solovay sdělil podrobnosti svého důkazu a prvních dvanáct kapitol (tj. více než 150 stran, přičemž kniha má celkem 184 stran!) údajně napsal během hektických šesti týdnů v létě 1976. Boolosova kniha byla publikována v roce 1979. Historie tím však zdaleka nekončí, ale spíše začíná. Nové otázky lze položit kupříkladu v souvislosti s modální predikátovou logikou. V predikátové logice dokazatelnosti můžeme totiž uvažovat tvrzení typu BV'xPx (při aritmetické interpretaci: je dokazatelné, že všechna čísla mají vlastnost P), V'xBPx (slovy: pro všechna čísla je dokazatelné, že mají vlastnost P), B3xPx (slovy: je dokazatelné, že existuje číslo, které má vlastnost P) apod. Zvláštní význam má tzv. formule Ruth BarcanMarcusové V'xBPx:JBV'xPx (slovy: jestliže je pro všechna čís­ la dokazatelné, že mají vlastnost P, pak je dokazatelné, že všechna čísla mají vlastnost P), o níž lze dokázat, že je nepravdivá, a její konverze, tj. formule BV'xPx:JV'xBPx (slovy: jestliže je dokazatelné, že všechna čísla mají vlastnost P, pak je pro všechna čísla dokazatelné, že mají vlastnost P), která je pravdivá. Výsledky týkající se ne axiomatizovatelnosti predikátové logiky dokazatelnosti objevili Franco Montagna a ne· závisle na něm Vann McGee a ruští logikové Sergej Artemov a Valerij Vardanyan. Další nové poznatky se týkají zkoumání logiky dokazatelnosti v rámci různých matematických teorií. Je pozoruhodné, že mnohé axiomatické teorie mají stejnou logiku dokazatelnosti. Zajímavé problémy byly vysloveny také v souvislosti se slabými teoriemi, tzv. bounded arithmetic (překládá se jako: slabá aritmetika). Důležitým podnětem k výzkumu slabé aritmetiky je skutečnost, že má vztah k výpočtové složitosti. Kupříkladu český logik Pavel Pudlák doká304

zal v SO.letech 20. století různá zobecnění Godelových vět pro slabé teorie. Dosud nevyřešený problém úplnosti logiky dokazatelnosti vůči slabým teoriím formulovali A. Berarducci aR. Verbrugge. Ve své práci z roku 1993 sice dokázali někte­ ré dílčí výsledky, problém však není dosud zcela vyřešen. Jiná zajímavá rozšíření logiky dokazatelnosti se týkají tzv. "logiky interpretovatelnosti". Tato logika používá navíc nový binární modální symbol (tj. symbol, který zapisujeme mezi dvě formule). jehož úkolem je formalizovat vztah, že jednu teorii lze interpretovat v nějaké jiné teorii. Konečně, v posledních letech bylo také dokázáno, že logika dokazatelnosti a Lewisův systém 84 zdaleka nejsou neslučitelné, jak předpokládá Smullyan v kapitole 23. Příklady logických teorií, které mají vlastnosti obou systémů, předložila TanyaYavorskaja. Tolik tedy k přľběhu logiky dokazatelnosti, který rozhodně není u konce. Kromě nových objevů v tomto oboru lze zejména očekávat její aplikaci na nematematické oblasti, možná právě v souvislostí s epistemickou logikou nebo s kognitivní vědou, jak předpovídá Smullyan.

o tom, kde se dovědět více Na úplný závěr těchto stručných poznámek navedeme čtená­ který by se rád o logice dověděl více, k dalšímu studiu. Kniha, kterou čtenář právě dočetl, jistě poskytuje vynikající populární uvedení do logiky, tematický záběr této knihy je nicméně poměrně úzký. Přístupnou formou se lze o logice vľce dočíst v řadě různých publikací. Doporučíme čtenáři alespoň dva texty, které jsou používány ve vysokoškolských kursech logiky pro studenty filosofie. Jedná se o knihu J. Štěpán, Klasická logika, Vydavatelství Univerzity Palackého, Olomouc, 2001. Vhodným doplňkem tohoto učebního textu s řadou řešených příkladů je P. Hromek, Logika v příkladech, Vydavatelství Univerzity Palackého, 010mouc,2002. ře,

305"

K hlubšímu seznámení s moderní logikou a její teorií mů­ žeme doporučit knihu R. Smullyan, Logika prvého rádu, Alfa, Bratislava, 1979. V této knize je čtenář uveden do logiky a její metateorie velmi stručnou formou. Nicméně v knize se používá nepříliš obvyklý systém dedukce pomocí metody sém'antických tabulek. K seznámení s moderními neklasickými logikami lze využít knihu M. Mleziva, Neklasické logiky, Nakladatelství Svoboda, Praha, 1970. Výklad týkající se modální logiky je nicméně zastaralý a například o kripkovské sémantice se kniha vůbec nezmiňuje.

Podrobně se zabývá matematickou logikou kniha A. Sochor, Klasická matematická logika, Karolinum, Praha, 2001. Tato kniha je určena již vážným zájemcům o logiku. Začáteč­ níky, kteří se s logikou teprve seznamují, by mohla spíše odradit. Další knihou podrobně se věnující moderní logice je V. Švejdar, Logika: neúplnost, složitost a nutnost, Academia, Praha, 2002. Autor se profesionálně věnuje metamatematice a neklasickým logikám. V této knize je logice dokazatelnosti věnován jeden s~mostatný oddíl. Ani tato kniha není určena začá tečníkům.

Z anglicky psané literatury lze kromě již zmíněné Boolosovy knihy (tj. The Unprovability of Consistency) doporučit monografii C. Smoryóski, Self-Reference and Modal Logic, Springer-Verlag, New York - Berlin - Heidelberg - Tokyo, 1986. Aktuálnější poznatky obsahuje novější (a bohužel již poslední) Boolosova monografie G. Boolos, The Logic of Provability, Cambridge University Press, Cambridge - New York - Melbourne, 1993. Tato monografie nově zpracovává a zásadně rozšiřuje témata vyložená v The Unprovability of Consistency a lze zde najít rovněž poučení o aplikacích logiky dokazatelnosti v teorii množin a aritmetice druhého řádu a o predikátové logice dokazatelnosti. Velmi užitečný a srozumitelný přehledový článek o logice dokazatelnosti s odkazy na nejaktuálnější poznatky a problé306

my lze najít v Internetové encyklopedii Stanford Encyclopedia of Philosophy (ed. E. Zalta) .. Jedná se o článek R. Verbrugge: "Provability Logic"; 2003, URL=http://plato.stanford.eduJentriesllogic-prova bility/. Rovněž Raymond Smullyan této problematice od roku 1987, kdy byla poprvé publikována naše kniha, věnoval následující tři monografie (první z nich je dle autora vhodná také pro "začátečníky", tj. pro ty čtenáře, kteří již absolvovali základní kurs logiky): R. Smullyan, áodel's lncompleteness Theorems, Oxford UnIversity Press, New York - Oxford, 1992, R. Smullyan, Recursion Theory for Metamathematics, Oxford University Press, New York - Oxford, 1993, a R. Smullyan, Diagonalization and Self-Reference, Clarendqn Press, Oxford, 1994. K obecnému úvodu do modální logiky lze doporučit knihu G. E. Hughes, M. 1. Cresswell, A New lntroduction to Modal Logic, Routledge, London - New York, 1996. Zde čtenář nalezne srozumitelný popis řady různých systémů modální logiky (jejichž praktické využití je nicméně v některých příkla­ dech problematické). Vhodný úvod do modální logiky pro čtenáře, který se zajímá spíše o filosofii než o matematiku, lze najít v knize M. Fitting, R. Mendelsohn, First-Order Modal Logic, Kluwer Academie Publishers,Dordrecht Boston - London, 1998. Diskusi týkající se toho, do jaké míry Godelovy věty dokazují neudržitelnost HUbertovy formalistické filosofie matematiky, je věnována kniha M. Detlefsen, Hi/bert's Program: An Essay on Mathematical lnstrumentalism, D. Reidel Publishing Company, Dordrecht - Boston - Lancaster - Tokyo, 1986. Poznámky k životu a dílu Kurta Godela (s ukázkami z jeho díla) lze najít ve sborníku vydaném k 90. výročí Godelova narození, 1. Malina, 1. Novotný (editoři), Kurt Godel, Nadace Universitas Masarykiana v Brně, Nakladatelství Georgetown v Brně, Nakladatelství a vydavatelství NAUMA v Brně, 1996. Zájemce o Goq.elovo filosofické dílo má k dispozici výběr 307

Godelových prací K. Godel, Filosofické eseje, OIKOYMENH, Praha, 1999. Tento výbor se věnuje Godelově filosofii mate~ matiky a obsahuje všechny významnější Godelovy články k to~ muto tématu. O filosofii matematiky v obecnějším kontextu se čtenář mt1že poučit v zajímavé knížce 1. D. Barrow, Pi na nebesich: O poč(tán(, myšleni a bytí, Mladá fronta, Praha, 2000. (Musíme však upozornit, že kniha, resp. její překlad, obsahuje řadu nepřesností.) Zde čtenář nalezne rovněž diskusi zajímavé filosofické interpretace Godelových vět, podle níž tyto věty dokazují, že lidská mysl je nealgoritmické povahy, a tudíž ji nelze adekvátně modelovat prostřednictvím žádného výpočetního stroje. Konečně, historické poznámky o peripetiích vzniku logiky dokazatelnosti a její rané historii lze najít v článku G. Boolos, G. Sambin, "Provability: The Emergence of a Mathematical Modality", Studia Logica 50 (1991), s.1-23.

308