středa 27. dubna 2011

Interpretace formálních systémů


Toto je druhý 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ředchozí díl - příští díl.

V minulém čísle jsme zavedli formální systém, který operoval s řetězci sestávajícími ze znaků M, I a U. Některé z těchto řetězců mají status teorému. Na počátku obsahovala množina teorémů jediný řetězec (který nazýváme axiomem), konkrétně MI. Množinu teorémů jsme ale mohli rozmnožovat tak, že jsme ze stávajících teorémů vyráběli nové pomocí specifikovaných odvozovacích pravidel. Množina teorémů se tak může rozrůstat donekonečna, a tedy teorémů je nekonečně mnoho (zda je výraz teorémem samozřejmě nezávisí na tom, jestli již jej někdo odvodil, ale pouze na tom, jestli jej odvodit lze).

Množina teorémů je nekonečně velká, ale v žádném případě není každý výraz teorémem. Asi každý čtenář minulého dílu si všimnul, že všechny teorémy začínají na M. Odvozovací pravidla nejsou schopna počáteční M „zabít“: první dvě pravidla vedou k přidávání znaků na konec výrazu a třetí ubírá trojice III. Pokud všechny axiomy mají M na počátku, jakože mají (tedy vlastně bych měl napsat „axiom má“, když je pouze jeden), tak všechny teorémy musí taktéž mít M na začátku. Podobně je patrné, že žádný teorém nebude mít M uprostřed nebo na konci. Můžeme tak s jistotou říct, že kupříkladu řetězce UUIU nebo MIM nejsou teorémy. Jak to ale je s řetězcem MU, na jehož status jsem se ptal v závěru minulého dílu? Ukazuje se, že ani MU není teorémem, i když uvidět to je o něco složitější, než v případech výrazů UUIU a MIM. Klíčové pozorování se týká počtu I uvnitř teorémů: odvození pravidlem I tento počet nechává beze změny, pravidlo II počet I zdvojnásobuje a pravidlo III jej snižuje o 3. Označme písmenem z zbytek po dělení počtu íček třemi. Pravidla I a III nechávají viditelně z beze změny. Jednoduchá úvaha prozradí, co se děje při odvozování za pomoci II. pravidla: je-li z = 0 pro původní teorém, je i z = 0 pro nově odvozený teorém; má-li původní teorém z = 1, nový má z = 2; a nakonec, má-li původní teorém z = 2, nový má z = 1. Jediný počáteční teorém má z = 1, a proto všechny teorémy budou mít buď z = 1 (pokud jejich odvození z počátečního axiomu zahrnuje sudý počet užití II. pravidla) nebo z = 2 (když odvození zahrnuje lichý počet užití tohoto pravidla). Výraz MU ale má z = 0, a tak nemůže být teorémem.

Předchozí úvahy mají jedno společné: dívají se na systém zvnějšku, s užitím dedukce, která není svázána třemi striktními pravidly systému MIU. Stroj, který by „dedukoval“ pouze v rámci systému MIU, by nikdy nezjistil, že MU není teorémem. Jediné, co tento stroj může dělat, chce-li zjistit, jestli MU je teorém, je aplikovat odvozovací pravidla na stále rostoucí množinu teorémů a doufat, narazí na MU. Pokud by se tak stalo (teď už víme, že k tomu dojít nemůže, ale připusťme to hypoteticky — nebo si představme na místě MU jiný řetězec, jehož teorémovost nám není známa), stroj by si „byl jist“, že výraz je teorémem. Při tomto postupu si ale nikdy nemůže být jist tím, že MU teorémem není, protože nikdy nemůže vyzkoušet všech nekonečně mnoho postupů odvozování a vyloučit tak, že žádný z nich nakonec nevyprodukuje MU.

K úvaze o rozdílné povaze teorémů a neteorémů se ještě vrátíme, ale předtím zavedu další Hofstadterův systém, který oproti systému MIU obsahuje dvě složky navíc: gramatiku a interpretaci.

Systém PR

Abeceda systému PR obsahuje tři znaky: P, R a -. Na rozdíl od předchozího systému, ve kterém jakýkoli řetězec byl přípustným výrazem, máme zde gramatické pravidlo: řežezec systému PR je dobře formovaný, obsahuje-li právě jedno P a právě jedno R, R leží vpravo od P, a nakonec ani P, ani R nestojí na kraji řetězce nebo těsně vedle sebe. Tudíž například -----P-R- nebo --P--R-- jsou dobře formované výrazy, zatímco R-P nebo -P-PP---R- nikoli. Dále máme k dispozici jediné odvozovací pravidlo:

  1. Je-li XPYRZ teorém, pak XPY-RZ- je také teorém.

Kupříkladu kdybychom věděli, že ----P-R- je teorém, pak bychom totéž mohli říct i o ----P--R--.

Skutečnost, že existuje pouze jedno odvozovací pravidlo, je svým způsobem vyvážena tím, že existuje nekonečně mnoho axiomů. Jinak řečeno, místo konečného systému axiomů máme k dispozici tzv. axiomové schéma, které zní takto: Každý dobře definovaný výraz tvaru XP-RX- je axiom. Podřetězec X zde může být libovolný (podmínka dobré definovanosti celého výrazu ve skutečnosti vede k tomu, že X stojí za úvahu jen pokud neobsahuje P ani R), a tak je axiomů nepřeberné množství. Nejjednodušším axiomem je zjevně -P-R--.

Pro názornost si teď můžete zkusit odvodit teorém --P---R-----; řešení je v poznámce [1].

Minule bylo řečeno, že interpretace formálního systému je návod, jak přiřadit symbolům či podřetězcům dobře definovaných výrazů vyjádření přirozeného jazyka, přičemž by mělo platit, že pravdivým výrokům přirozeného jazyka odpovídají teorémy formálního systému. Můžeme teď zkusit interpretovat systém PQ. Což tedy zkusit tuto interpretaci:

  1. Každou maximální nepřerušenou řadu pomlček nahradíme číslovkou označující její délku. To jest - překládáme jako „jedna“, -- překládáme jako „dvě“ atd. Přívlastkem maximální chci říct, že musíme vždy vzít nejdelší nepřerušený řetězec mezer: z výrazu ---P-R-- nelze sestrojit částečný překlad „jednadva“P„jedna“R„dva“, ale pouze „tři“P„jedna“R„dva“.
  2. Symbol P nahradíme řetězcem „ plus “.
  3. Symbol R nahradíme řetězcem „ rovná se “.

Teorému --P---R----- pak odpovídá interpretace „dva plus tři rovná se pět“, což je zcela jistě pravdivý výrok. Po vyzkoušení několika dalších teorémů se ukáže, že jejich interpretace jsou také pravdivé — nakonec jste si pravděpodobně všimnuli, že ve všech teorémech je počet pomlček vlevo od R stejný, jako počet pomlček vpravo od R, a odtud je jen krůček k poznání, že uvedená interpretace je skutečně správná. Zdá se tedy, že systém PR lze použít pro popis sčítání kladných celých čísel. Gramatika systému zde pomáhá k tomu, aby po interpretaci vznikl smysluplný výrok: interpretace všech dobře formovaných výrazů jsou korektní české věty. Pozor ovšem na to, že to nefunguje opačně, tj. ne všechny smysluplné české věty o sčítání lze zapsat jako výrazy systému PR. Například „dva plus tři se rovná jedna plus čtyři“ je smysluplná věta, dokonce pravdivá, ale řetězec --P---R-P---- není dobře formovaný výraz systému PR. To pochopitelně neznamená, že nemůžeme vhodným způsobem systém PR rozšířit, aby umožňoval i výrazy tohoto typu. Jakmile ale jednou stanovíme pravidla formálního systému, musíme se jich strinktně držet, i když nám interpretace napovídá možnost jejich obejití.

Již od časů Eukleida bylo formální odvozování ideálem matematického důkazu, a dnešní matematika je vystavěna jako formální systém. Pro důkazy běžných tvrzení není potřeba klesat až na úroveň manipulací s řetězci znaků, a pro formulaci matematických vět se tak užívá upravená verze normálního jazyka. Víme ale, že v případě potřeby lze matematická tvrzení redukovat na řetězce určitého formálního systému, a jejich důkazy na posloupnost přesně specifikovaných elementárních kroků. Dokazovat složitější tvrzení na úrovni formálních systémů by bylo stejně nepohodlné jako tvořit webové stránky v assembleru, obojí ale je v principu možné.

Systém PR není zrovna nejlepším nástrojem pro formální popis sčítání, ale to neznamená, že nefunguje. Mohli bychom jej proto použít pro důkazy jednoduchých aritmetických tvrzení typu „37+62=99“. Matematikové používají k formalizaci aritmetiky o něco složitější systémy, ale duch v nich prováděných odvození je podobný, čtenář si tak může již nyní učinit určitou představu o tom, oč vlastně šlo ve slavném Russellově a Whiteheadově důkazu tvrzení „1+1=2“ (bez jasné představy o povaze formálních systémů jsem míval značné potíže pochopit, co je na „1+1=2“ možné dokazovat).

S formálním dokazováním tvrzení přirozeného jazyka je spjat filosofický problém. Na začátku tvorby libovolného formálního systému, který později zamýšlíme interpretovat, se snažíme zformalizovat nějakou sadu pravdivých tvrzení a najít několik málo pravidel, pomocí kterých lze tuto sadu rozšiřovat. Ukáže-li se, že rozšířená sada obsahuje pouze pravdivé výroky, uznáme nakonec, že systém plní svou funkci. Jak si ale můžeme být jisti, že všechny teorémy systému mají pravdivou interpretaci? A pokud si tím nemůžeme být jisti, jak můžeme fakt, že nějaký výraz je teorémem zvoleného systému, považovat za důkaz toho, že jeho interpretace je pravdivý výrok? Co když odvodíme teorém, jehož interpretace se bude jevit intuitivně nepravdivou? Máme věřit intuici a odvrhnout systém, nebo naopak důvěřovat systému a ignorovat intuici? Věc je komplikována tím, že pravdivost převážné většiny formulovatelných výroků není nijak intuitivně zřejmá, a pro její posouzení se musíme obrátit k víceméně formálnímu odvozování. Zůstaneme-li u jednoduchých výrazů pro sčítání: abychom zjistili, zda výrok „3775489 + 254563 = 4030052“ je pravdivý, musíme na levou stranu rovnosti aplikovat naučený algoritmus zvaný sčítání, který se znaky řetězce operuje přesně daným způsobem (nebo tuto povinnost delegovat na kalkulačku). Zdá se, jakoby formální systém, zde vtělený do postupů, které se každý naučí ve druhé třídě, v podobných případech pravdivost výroku definoval. A přesto, můžeme si snadno vymyslet formální systémy generující nepravdivé výroku — ba dokonce by asi nebylo tak těžké zařídit, aby takový nepravdu generující systém měl axiomy a odvozovací pravidla, na kterých by na první pohled nebylo vidět nic závadného.

Poučení z předchozího odstavce je, že, kdyby nic jiného, je jednodušší a bezpečnější mluvit o teorémech a neteorémech, než o pravdách a nepravdách. Pro teorémy ale nemusí platit všechna omezení, která očekáváme u pravdivého výroku. Zejména, obsahuje-li náš systém znak ¬ interpretovaný jako negace, ze skutečnosti, že ¬X je teorém ještě neplyne, že X teorém není, a naopak též ne. Může se stát, že nějaký dobře formovaný výraz X z počátečních axiomů nelze vyvodit, a zároveň ani nelze vyvodit ¬X. Výraz X je potom v rámci tohoto systému nerozhodnutelný, a systém obsahující nerozhodnutelné dobře formované výrazy se nazývá neúplným. Nebo se může stát i to, že naopak odvodíme jak X, tak ¬X. Jestliže k tomu dojde, říkáme, že daný systém je nekonsistentní. Nekonsistence ovšem neznamená, že náš systém nelze užívat jako formální systém; z formální stránky je vše v pořádku, nekonsistence je problematická pouze kvůli zvolené interpretaci. (Na druhou stranu, aspoň pro standardní verze logiky má nekonsistence destruktivní následky, protože umožňuje snadno odvodit každý výraz jako teorém, a systém, ve kterém je každý dobře formovaný výraz teorémem, zjevně nenaskýtá velký praktický užitek.)

Jak neúplnost, tak i nekonsistence se zdají být vadou na kráse formálních systémů. Dlouholetý ideál matematiků byl vytvořit teorii, ve které by každý matematický výrok byl dokazatelně buď pravdivý nebo nepravdivý; přeloženo do formálnějšího jazyka, kde by pro každé dobře formované X bylo buď X samotné, nebo jeho negace ¬X, teorémem. Gödel ukázal, že tohoto cíle nelze dosáhnout. V dalších dílech se na tuto nemožnost podíváme detailněji.


Poznámky:
1. Jediný možný postup:

  1. --P-Q--- (axiom, vyhovuje schématu XP-RX-)
  2. --P--Q---- (z 1. pomocí pravidla I.)
  3. --P---Q----- (z 2. pomocí pravidla I.)

Žádné komentáře:

Okomentovat