Formální systémy

Toto je první díl seriálu o logice, který volně sleduje myšlenky D.Hofstadtera sepsané v jeho knize Gödel, Escher, Bach. Navigace: úvodní článek - příští díl.

Pod logikou si obvykle představujeme disciplínu zkoumající zásady, kterými se musí řídit myšlení, má-li si nárokovat spolehlivost. V historii existovaly různé přístupy k logice. Po dlouhou dobu byly populární aristotelské sylogismy, které stanovovaly, jaké operace je možno provádět s některými množinovými výroky. Kanonický příklad sylogismu je toto odvození:

1. Všichni savci jsou zvířata.
   
2. Všechny krávy jsou savci.
   
3. Některé krávy jsou zvířata.
   

V každém sylogismu třetí výrok plyne z prvních dvou. Sylogismus uvedený výše je platný [*]. Jiný příklad sylogismu, tentokráte neplatného:

1. Všichni savci jsou zvířata.
   
2. Všechny krávy jsou zvířata.
   
3. Některé krávy jsou savci.
   

Sylogismus je neplatný navzdory tomu, že všechny tři výroky jsou pravdivé. Neplatnost znamená, že nahradíme-li krávy, zvířata a savce jinými kategoriemi, může se stát, že první dva výroky budou pravdivé, zatímco třetí nikoli. Platnost sylogismu je vlastností jeho struktury, nikoli věcí, o kterých sylogismus mluví. Z tohoto důvodu je vhodné použít abstraktnější symbolickou notaci, která dá lépe vyniknout logické struktuře. Dnes by člověk první sylogismus zapsal třeba takto:

0. ∃x:K(x)
   
1. ∀x:S(x)⇒Z(x)
   
2. ∀x:K(x)⇒S(x)
   
3. ∃x:K(x)∧Z(x)
   

Symbol S(x) reprezentuje výrok „x je savec“, nicméně platnost sylogismu nezávisí na této interpretaci. Nultý výrok je doplnění nevyjádřeného předpokladu, že existuje aspoň jedna kráva.

Středověký způsob nakládání se sylogismy byl v jistých ohledech velmi těžkopádný. Existuje 256 typů různých sylogismů (které dostaneme z našeho prvního různým prohazováním pozic krav, savců a zvířat a záměnami slov „některé“, „všechny“ a „žádné“) z nichž pouze 24 je platných, a středověký logik jednoduše memorizoval těchto 24 variant, obvykle s užitím určitých mnemotechnických pomůcek (detaily viz článek na anglické Wikipedii). Z dnešního pohledu se takový přístup zdá absurdní. Místo memorizace čtyřiadvaceti schémat platných sylogismů si pamatujeme, jaké operace je možné činit s logickými symboly. Například víme, že implikace je transitivní, což znamená, že platí-li A⇒B a zároveň platí B⇒C, pak platí i A⇒C, díky čemuž z 1. a 2. odvodíme ∀x:K(x)⇒Z(x). Pomocí jiných povolených operací pak z tohoto mezivýsledku a nulté premisy ∃x:K(x) lze odvodit hledaný čtvrtý výrok.

Formální systémy

K sepsání seznamu povolených operací v predikátové logice se ještě dostanu v některém z příštích dílů; v tuto chvíli je to nepříliš podstatné. Podstatná je ale idea, že logická dedukce má strukturu operací s řetězci znaků, které (ty řetězce) sice je možno interpretovat jako tvrzení přirozeného jazyka, ale které (ty operace) nezávisí na této interpretaci. Logika je příklad formálního systému. Základem formálního systému je jeho abeceda, což je množina symbolů, z kterých postupně budeme sestavovat řetězce. Ve výše uvedených příkladech jsme konstruovali řetězce predikátové logiky s užitím symbolů ∃, ∀, ⇒, ∧, :, (, ), x, K, S a Z. Tyto symboly jsou součástí abecedy predikátové logiky (ta obsahuje i další symboly, které se v příkladech výše nevyskytují). Symboly abeced formálních systémů budu vždy psát tučně. Řetězce těchto symbolů pak tvoří výrazy formálního jazyka.

Lze si představit formální systém, který připouští jakékoli řetězce (a zanedlouho jeden takový zavedeme), ale většina formálních systémů podrobuje své řetězce určitým omezením, která tvoří gramatiku formálního jazyka. Ve výrokové logice například nemůže znak ⇒ stát na začátku výroku, počet závorek ( musí být roven počtu ) atd. Řetězec ⇒)Kx::Z gramatice nevyhovuje, jinak řečeno, není dobře formovaným výrazem. Některé dobře formované výrazy mají status teorému. Má-li formální systém vhodnou interpretaci, dobře formované výrazy odpovídají smysluplným tvrzením přirozeného jazyka, zatímco teorémy by měly odpovídat pravdivým tvrzením. Tak tomu samozřejmě je v logice: příkladem teorému je výraz A⇒A (s interpretací „jestliže platí A, pak platí A“; tato interpretace je pouze částečná, protože jsem nechal neinterpretovaný symbol A, nicméně pravdivost je zřejmá i tak), zatímco příkladem dobře formovaného výrazu, který není teorémem, je A∧¬A („platí A a zároveň neplatí A“). Formální systémy se ale obejdou i bez interpretace, a v tom případě teorémy jsou prostě určitou podmnožinou dobře formovaných výrazů. K definitivnímu určení formálního systému je tudíž potřeba určit způsob, jak odlišit teorémy od neteorémů.

Hledanými posledními přísadami do formálního systému jsou axiomy a odvozovací pravidla. Axiomy jsou výrazy, které získávají čest být teorémem zdarma, v rámci definice formálního systému. Odvozovací pravidla jsou potom přísně specifikované postupy, jak z teorémů vytvářet další teorémy. Jeden z axiomů výrokové logiky je A⇒(B⇒A). Příkladem odvozovacího pravidla je modus ponens, formulovaný následovně: pokud X je teorém a zároveň X⇒Y je teorém, pak Y je teorém. (Všimněte si, že X a Y zde nejsou jednotlivé symboly z abecedy výrokové logiky, ale libovolné řetězce; proto je nepíšu tučně, ale kurzívou.) Kdybychom měli ještě jeden axiom, konkrétně A, mohli bychom modus ponens užít k odvození teorému (B⇒A).

Ačkoli různé verze a nadstavby logiky jsou nejdůležitějšími příklady formálních systémů (a vlastně i důvodem, proč nás vlastně formální systémy zajímají), pro ilustraci základních ideí se příliš nehodí. Jedním důvodem je jejich relativní složitost, a druhým je existence interpretace. Logiku užíváme dnes a denně pro řešení bežných problémů života, a máme k tomu vyvinuté efektivní intuitivní myšlení. To ale svádí k různým zkratkovitým manipulacím a posuzování výrazů formální logiky na základě jejich interpretace. Pro běžné aplikace (kam spadá vše od úvah typu „soused je katolík, každý katolík je křesťan, tudíž soused je křesťan“ až po dokazování Banachovy věty o pevném bodě) je to naprosto dostatečné. Chceme-li ale zkoumat logiku samotnou, musíme se držet striktně formálních postupů, a to vyžaduje určitý tréning. Z toho důvodu Hofstadter v úvodu své knihy zavádí poměrně jednoduchý formální systém, který nemá žádnou očividnou interpretaci.

Systém MIU
Abeceda systému MIU sestává, jak by se nakonec podle názvu dalo čekat, ze tří symbolů: M, I a U. Jak jsem již avizoval o tři odstavce výše, tento systém nemá žádná gramatická pravidla: libovolný řetězec sestávající ze znaků M, I a U, například M nebo třeba UUIMUUMU, je dobře formulovaným výrazem. Odvozovací pravidla jsou tři:

1. Končí-li teorém na I, můžeme na konec přidat U a získáme nový teorém. Tedy je-li XI teorém, pak XIU je teorém. (Například, z UII odvodíme UIIU.)
   
2. Máme-li teorém začínající na M, můžeme to, co následuje, zdvojit. Tedy je-li MX teorém, MXX je teorém. (Například, z MMUUI odvodíme MMUUIMUUI.)
   
3. Když v libovolném teorému nahradíme podřetězec III symbolem U, získáme nový teorém. Tedy je-li XIIIY teorém, je i XUY teorém. (Například, z UMUIIIU odvodíme UMUUU.)
   

No a konečně, zbývá zadat axiomy. Lépe řečeno axiom, protože je pouze jeden: MI

Použitím prvního a druhého pravidla můžeme z axiomu odvodit okamžitě dva teorémy: MIU a MII. Možnosti odvozování tím ale samozřejmě nekončí, můžeme postupovat ve více krocích a konstruovat libovolně dlouhé teorémy. Kupříkladu můžeme odvodit teorém MIUUIUU, a to třeba takto:

1. MI (axiom)
   
2. MII (z 1. s užitím pravidla II)
   
3. MIIII (z 2. s užitím pravidla II)
   
4. MIIIIU (z 3. s užitím pravidla I)
   
5. MIUU (z 4. s užitím pravidla III)
   
6. MIUUIUU (z 5. s užitím pravidla II)
   

Všechny řetězce získané v mezikrocích jsou samozřejmě také teorémy.

Samozřejmě můžeme strojově aplikovat zadaná odvozovací pravidla v libovolném pořadí a vršit nekonečný seznam teorémů; půvabu v této činnosti moc není. O poznání zajímavější se věc stane v momentě, kdy si začneme klást otázky typu: „je MIUUIUU teorém?“ Pro MIUUIUU odpověď známe, ale zkuste to na moment zapomenout. Jak byste postupovali? Evidentně můžete zkoušet odvozovat různé teorémy a doufat, že narazíte na MIUUIUU. Takovou činnost lze aplikovat systematicky: nejdřív vyzkoušíte všechna jednokroková odvození, pak dvoukroková, tříkroková a tak dále, a mezi pětikrokovými nakonec narazíte na výše uvedené a vyprodukujete hledaný řetězec. Takový postup by byl ovšem velmi zdlouhavý, protože počet n-krokových odvození roste geometricky s n. A co hůře, na začátku nevíte, že nejkratší [*] odvození MIUUIUU má pět kroků. Mohlo by jich mít sedmdesát, nebo třeba milion.

Stejně jako matematikové při dokazování matematických vět slepě systematicky neprohledávají všechna možná odvozování a stejně jako šachisté při hledání nejlepší hry strojově neprocházejí všechny varianty tahů povolených v pravidlech, i pro odvozování v systému MIU si lze vypěstovat cit. Mělo by to být výrazně jednodušší, než vypěstovat si cit pro šachy nebo matematiku, protože MIU je výrazně jednodušší než šachy a matematika. Svůj cit pro systém MIU si můžete vyzkoušet při řešení problému, který Hofstadter předkládá svým čtenářům: Je MU teorém? K odpovědi se dostanu v dalším díle — jestli si chcete zkusit problém vyřešit samostatně, máte na to dost času.