Abstrakt

Text je ur!en jako dopl"kov# k p$edná%ce Matematická logika a Para-digmata programování 4.

1

Matematická logika - poznámky k p!edná"kám

Radim B!lohlávek

14. srpna 2006

1 Co je (matematická) logika?Co je logika? Logika je v!dou o správném usuzování. V logice jde o to, abyusuzování m!lo správnou formu bez ohledu na obsah. Uva"ujeme-li nap#. tvr-zení “pr$í” a “jestli"e pr$í, (pak) jsou silnice mokré”, pak z nich (intuitivn! zcelasamoz#ejm!) lze odvodit tvrzení “silnice jsou mokré”. Uva"ujme jinou dvojicitvrzení, nap#. “Petr má hlad” a “Jestli"e má Petr hlad, (pak) se (Petr) sna"ísehnat n!co k jídlu”. Z t!chto tvrzení plyne tvrzení “Petr se sna"í sehnat n!cok jídlu”. V uveden%ch p#íkladech vypl%valo z dvojice tvrzení dal$í tvrzení. Uve-dené dvojice tvrzení m!ly zcela jist! jin% obsah (“pr$í” znamená zcela jist! n!cojiného ne" “Petr má hlad”). Zp&sob, jak%m jsme odvodili t#etí tvrzení byl v$akv obou p#ípadech stejn%; #íkáme, "e usuzování m!lo stejnou formu. Tuto formuje mo"né znázornit symbolicky takto: z tvrzení, které má formu “A”, a tvrzení,které má formu “A B” (“jestli"e A, pak B”), plyne tvrzení “B”.Uvedené rysy jsou pro moderní logiku charakteristické, proto je zopakujme:

logika studuje formy usuzování bez ohledu na obsah a má (proto) symbolick%charakter (jednotlivá tvrzení ozna'ujeme symboly-písmeny, nap#. v%$e uvedenésymboly A a B; zp&soby spojení tvrzení ve slo"it!j$í tvrzení ozna'ujeme sym-boly, nap#. v%$e uvedené “ ”). Pro uvedené rysy b%vá moderní logika ozna-'ována jako logika formální, pop#. symbolická. Je pochopitelné, "e symbolick%charakter umo"(uje logice snadn!ji odhlédnout od obsahu a soust#edit se naformy usuzování.

Co je matematická logika? U'iníme-li studium forem usuzování p#edm!temna$eho zájmu, vzniká p#irozen! otázka, jak%ch metod p#i tomto studiu pou"ívat.Rozhodneme-li se pou"ívat metod matematiky, hovo#íme o matematické logice.Studiem logiky matematick%mi prost#edky lze dosáhnout hlubok%ch v%sledk&,n!které uká"eme v tomto textu. V na$em textu budeme pojednávat práv! o ma-tematické logice.

Logika: matematická a nematematická? Dosp!li jsme ke stru'né charak-teristice toho, co nás bude zajímat p#edev$ím, tedy matematické logiky. Otázkounyní z&stává, co dal$ího krom!matematické logiky se ve sv!t! logiky skr%vá. N!-kdy b%vá uvád!no, "e logika se d!lí na matematickou logiku a filozofickou logiku.

2

Toto d!lení má své historické d&vody, které zde nem&"eme podrobn! rozvád!t.V sou'asné dob!, zdá se, je v$ak toto rozd!lení um!lé, nep#irozené a p#ekonané.Na vysv!tlenou pouze stru'n! uve)me: Otázky po správn%ch formách usuzovánísi jist! v té 'i oné podob! kladli lidé velmi dávno. Za zakladatele logiky je pova-"ován Aristotelés (384-322 p#. n. l.). Od té doby byly otázky logiky p#edm!temzájmu mnoha u'enc&, bylo nastoleno mnoho otázek a témat. V!t$ina z nich mápovahu fundamentálních otázek po podstat! lidského usuzování a je tedy svoupovahou filozofická. Teprve koncem 19. a za'átkem 20. století do$lo k v%raznématematizaci logiky. P#i této matematizaci $lo p#edev$ím o formalizaci usuzo-vání v matematice a v tzv. exaktních v!dách, ne lidského usuzování obecn!.Matematick%mi prost#edky tak byly studovány pouze vybrané aspekty usuzo-vání a vznikl dojem, "e ostatní aspekty usuzování (nap#. vliv 'asu ve tvrzeníchobsahujících odkaz na 'as jako “N!kdy v minulosti pr$elo”, tvrzení obsahujícímodality jako “je mo"né, "e pr$í”) se matematick%mi prost#edky nedají studo-vat. Studium t!chto “ostatních aspekt&” bylo p#isuzováno tzv. filozofické logice.Postupn! se v$ak docházelo k tomu, "e matematické metody byly pou"íványi ke studiu zmín!n%ch “ostatních aspekt&”, a ukázalo se, "e d!lení logiky namatematickou filosofickou je v!cn! neopodstatn!né.

Logika: klasická a neklasická? Klasickou logikou se rozumí logika, ve kterép#edpokládáme, "e tvrzení mohou nab%vat dvou pravdivostních hodnot (pravdaa nepravda), ve které tvrzení mohou b%t spojována ve tvrzení slo"it!j$í spoj-kami “není pravda, "e . . . ”, “. . . a. . . ”, “. . . nebo. . . ”, “jestli"e . . . , pak. . . ”, “. . . ,práv! kdy" . . . ” a kvantifikátory “pro ka"dé x . . . ” a “existuje x, pro které . . . ”a ve které pravdivostní hodnoty slo"en%ch tvrzení závisí na pravdivostních hod-notách skládan%ch tvrzení zp&sobem, kter% zná 'tená# nejspí$ ji" ze st#ední$koly (viz dále). Jiná logika se pova"uje za neklasickou (tvrzení mohou mít vícehodnot nebo je mo"né pou"ívat i jiné spojky nebo mají spojky jin% v%znamapod.).

Logika: !istá a aplikovaná? Aplikovanou logikou se n!kdy rozumí studiumproblém&, které vznikají p#i pokusu pou"ít logiku na tu 'i onu oblast, kterámá oproti situaci, kdy nás zajímá usuzování v&bec, svá specifika. Tato specifikaumo"(ují #adu dodate'n%ch (zjednodu$ujících) p#edpoklad&, díky kter%m se vespecifick%ch oblastech metodami logiky dosahuje pozoruhodn%ch v%sledk&. *is-tou logikou se v této souvislosti rozumí logika v$eobecná, zab%vající se formamiusuzování bez ohledu na konkrétní oblasti pou"ití. Je z#ejmé, "e i toto d!lení jespí$e orienta'ní, vyjad#ující vícemén! motivace a cíle.

Jak" je vztah logiky a informatiky? Stru'n! #e'eno, bohat% a r&znorod%.DOPLNIT

• Automatické dokazování.

• Logické programování.

• Logika program&.

3

• P#ibli"né usuzování.

• Anal%za dat.

Logika: v"roková a predikátová? V na$em pojednání se budeme nejd#ívezab%vat tzv. v%rokovou logikou, poté tzv. predikátovou logikou. Aby bylo jasno,#ekn!me u" te), "e nejde “o dv! r&zné logiky”. Predikátová logika je roz$í#enímv%rokové logiky (v%sti"n!ji #e'eno zjemn!ním v%rokové logiky). Bylo by tedymo"né v%rokovou logiku vynechat a zab%vat se rovnou predikátovou logikou.Proto"e je v$ak v%roková logika jednodu$$í a proto"e nám navíc umo"ní ilustro-vat základní problémy logiky v dostate'né mí#e, za'neme z didaktick%ch d&vod&logikou v%rokovou. O tom, jak% je p#esn! vztah v%rokové a predikátové logiky,se zmíníme pozd!ji.

2 V!roková logika1

2.1 . . . k v!rokové logice

V%rokem intuitivn! chápeme v%pov!) (tvrzení), u které má smysl uva"ovat o jejípravdivosti. Tedy nap#. “Pr$í.” je v%rok, “Byl jsem v obchod! a koupil jsem siknihu.” je v%rok, “2+2=6” je v%rok, ale “kniha v obchod!” není v%rok, “2+2”není v%rok. V%roková logika b%vá naz%vána logikou v%rokov%ch spojek; p#itomspojkami se myslí spojky jako “a”, “nebo”, “jestli"e, . . . pak . . . ”, “ne” (tj. “nenípravda, "e . . . ”) apod.2

N!které v%roky jsou pravdivé (nap#. “2+2=4”), n!které jsou nepravdivé(nap#. “2+2=6”). O tvrzení, které je pravdivé, #ekneme, "e má pravdivostníhodnotu 1 (pravda); o tvrzení, které je nepravdivé, #ekneme, "e má pravdivostníhodnotu 0 (nepravda).U n!kter%ch tvrzení má smysl uva"ovat o jejich pravdivosti (jsou tedy v%-

roky), nap#. “*lov!k s v%$kou 180cm je vysok%”, p#esto se v$ak zdráháme #íci,"e dané tvrzení je pravdivé nebo, "e není pravdivé (je nepravdivé). Pravdivostníhodnota, kterou bychom mu p#i#adili, by byla n!kde mezi 0 a 1, nap#. #ekneme-li, "e “*lov!k vysok% 180cm je vysok%” má pravdivostní hodnotu 0.8, #íkámetím, "e je pravdivé ve stupni 0.8, tj. "e je skoro pravdivé. V následujícím seomezíme na (tvrzení, které mohou mít jen) dv! pravdivostní hodnoty (0 a 1).Poznamenejme pouze, "e studiem více pravdivostních hodnot se zab%vá tzv.fuzzy logika (ta je v sou'asné dob! intenzívn! zkoumána).U n!kter%ch tvrzení závisí pravdivostní hodnota na 'ase, nap#. “Za t%den

bude pr$et.” Takov%mi tvrzeními se zab%vá tzv. logika 'asu (temporální logika).

1Té! v"rokov" po#et nebo v"rokov" kalkul.2V$imn%me si, !e pojem spojka zde pou!íváme v $ir$ím v"znamu ne! b"vá b%!né: spoj-

kou chápeme jazykov" v"raz, jeho! pou!itím na v"roky dostaneme nov" v"rok. Nap&. v"rok“Jestli!e pr$í, pak je mokro.” vznikl pou!itím spojky “jestli!e. . . , pak . . . ” na v"roky “pr$í”a “je mokro” apod.

4

Ta má pro informatiku zásadní v%znam. My se s ní v$ak nesetkáme (resp. se-tkáme se jen okrajov!) a budeme faktor 'asu ignorovat, tj. budeme se zab%vattvrzeními, jejich" pravdivost na 'ase závislá není.Posledním omezení (tj. zjednodu$ení), které p#ijmeme, se t%ká v%rokov%ch

spojek. Podle v%$e uvedeného, je spojkou nejen “ne” (tj. “není pravda, "e . . . ”nap#. v tvrzení “Není pravda, "e pr$í”), ale také “nutn!” (tj. “nutn! platí, "e. . . ” nap#. v tvrzení “Nutn! platí, "e pr$í”), “mo"ná” (tj. “je mo"né, "e . . . ”nap#. v tvrzení “Je mo"né, "e pr$í”), “ví se” (tj. “ví se, "e . . . ” nap#. v tvr-zení “Ví se, "e pr$í”) apod. Takové spojky je mo"né zkoumat (spojky “nutn!”a “mo"ná” zkoumá tzv. modální logika, spojky “ví se” apod. zkoumá tzv. epis-temická logika), my to v$ak d!lat nebudeme a omezíme se jen na tzv. spojkyklasické.

Poznámka 2.1 V$imn!me si, "e u" te) jsme u'inili #adu zjednodu$ujících p#ed-poklad&.

V$imn!me si, "e v p#irozeném jazyce existují tvrzení, která znamenají tosamé, ale jsou r&zná: nap#. dvojice tvrzení “Nepr$í.” a “Není pravda, "e pr$í”nebo trojice tvrzení “Mo"ná pr$í.”, “Je mo"né, "e pr$í.” a “Mo"ná je pravda, "epr$í.”Jak jsme zmínili v%$e, úkolem logiky je zkoumat usuzování a související pro-

blémy, av$ak bez ohledu na obsah toho, co je (o 'em je) usuzováno. Odhlédneme-li u usuzování od obsahu, zbyde forma (nap#. u v%$e uvedeného odvození tvrzení“silnice jsou mokré” ze dvou tvrzení “pr$í” a “jestli"e pr$í, (pak) jsou silnicemokré” zbyde po odhlédnutí od obsahu (abstrakce od obsahu) forma tohotoodvození, kterou je mo"né zachytit pomocí: z “A” a “A B” lze odvodit “B”).V tomto smyslu jde tedy v logice o formu usuzování.Chceme se tedy soust#edit usuzování o v%rocích, p#itom nás nezajímá ob-

sah, ale pouze forma usuzovaného. Na jedné stran! tím v jistém smyslu ztratíme,nebo+ na$e rozli$ovací schopnost odhlédnutím od obsahu klesne (v%roky, pop#.úsudky se stejnou formou, ale r&zn%m obsahem, pro nás budou nerozli$itelné).Na druhé stran!, soust#ed!ním se pouze na formu nám umo"ní objevit zákoni-tosti, kter%mi se #ídí usuzování nad jak%mikoli v%roky, tedy v%roky s libovoln%mobsahem. V%sledky, které získáme, budeme tedy moci pou"ít na libovolné v%-roky. Dal$í v%hodou odlhlédnutí od obsahu je bezesporu fakt, "e zbavíme-li senepodstatného (v na$em p#ípad! obsahu), budeme lépe vid!t podstatné (v na-$em p#ípad! zákonitosti usuzování).Je d&le"ité upozornit na to, "e nám jde o dv! v!ci: Za prvé, chceme studovat

formy usuzování a související aspekty. Za druhé, chceme na$e úvahy zp#esnit tak,abychom ke studiu forem usuzování mohli pou"ít matematické metody. *tená#si jist! uv!domil, "e zatím jsme se pohybovali na intuitivní (a tedy nep#esné,matematick%mi metodami neuchopitelné) úrovni. Tak nap#íklad, #ekli jsme, "ev%rok je v%pov!), u které má smysl uva"ovat o její pravdivosti. Nedefinovalijsme p#esn!, co rozumíme spojením “v%pov!), u které má smysl uva"ovat o jejípravdivosti” a nechali jsme toto na 'tená#ov! intuitivním porozum!ní. V dal$ímp#istoupíme k vybudování formálního systému v%rokové logiky.

5

2.2 Základní syntaktické pojmy

Chceme-li zkoumat formy usuzování o v%rocích bez ohledu na jejich obsah,bude u"ite'né ozna'ovat v%roky pomocí symbol& (to jsme ostatn! ji" u'inili,kdy" jsme pou"ili A a B pro ozna'ení v%rok& p#i ukázce odhlédnutí od obsahu).N!které v%roky vznikly z jin%ch pomocí spojek, jiné spojky neobsahují (nap#.“Pr$í.”), a jsou tedy v tomto smyslu ned!litelné (atomické). Atomické v%rokybudeme ozna'ovat speciálními symboly, kter%m budeme #íkat v!rokové symboly.Spojky, kter%mi se v%roky spojují ve slo"ené v%roky, budeme ozna'ovat symbolyv!rokov!ch spojek. Tak budeme moci zapisovat formu v%rok&: nap#. ozna'ují-lisymboly p a q po #ad! v%roky “pr$í” a “silnice jsou mokré” a ozna'uje-lispojku “jestli"e . . . , pak . . . ”, v%rok “jestli"e pr$í, pak silnice jsou mokré” jezapsán v%razem p q. Navíc, zapomeneme-li na obsahy v%rok& ozna'en%chpomocí p a q, reprezentuje v%raz p q formu v%roku. Abychom mohli poho-dln! a p#ehledn! zapisovat slo"ené v%roky, budeme pou"ívat pomocné symboly(v!t$inou závorky r&zn%ch druh&). Dostali jsme se k tomu, co se naz%vá jazykv%rokové logiky:

Definice 2.2 Jazyk v!rokové logiky se skládá z

• v!rokov!ch symbol" p, q, r, . . . , pop#. s indexy, p1, p2; p#edpokládáme,"e máme neomezen! mnoho (spo'etn! mnoho) v%rokov%ch symbol&;

• symbol" v!rokov!ch spojek (negace), (implikace), pop#. dále(konjunkce), (disjunkce), (ekvivalence);

• pomocn!ch symbol" (, ), [, ], atd. (r&zné druhy závorek).

Ne" p#istoupíme k dal$í definici, musíme objasnit tu 'ást definice jazyka v%-rokové logiky, která se t%ká spojek (ta je v Definici 2.2 nejednozna'ná). V zásad!jde o to, "e n!které spojky je mo"né nahradit jin%mi. Tak nap#íklad v%rok “Pr$ía je zima.” je pravdiv%, práv! kdy" je pravdiv% v%rok “Není pravda, "e nepr$ínebo není zima.” To platí pro jakékoli v%roky. V%rok tvaru “A a B” má stejnoupravdivostní hodnotu jako v%rok “Není pravda, "e neplatí A nebo neplatí B”.Je tedy vid!t, "e spojku “a” (pou"itou v prvním v%roku) lze nahradit pomocíspojek “ne” a “nebo” (pou"it%ch ve druhém v%roku). M&"eme tedy postupovattak, "e n!které spojky zvolíme za základní a dal$í budeme pova"ovat za odvo-zené (to zatím vidíme intuitivn!, za okam"ik uvidíme, jak to provést korektn!).To má své v%hody, které pln! doceníme a" v následujícím textu (v%hody jsoup#edev$ím technické: budeme mít krat$í definice a krat$í d&kazy).Shr(me tedy: Jde nám o spojky “ne”, “a”, “nebo”, “jestli"e . . . , pak . . . ”,

“. . . , práv! kdy" . . . ”. Pracovat s nimi m&"eme dvojím zp&sobem. Za prvé, m&-"eme je (resp. jim odpovídající symboly v jazyce) v$echny pova"ovat za základní.Za druhé, m&"eme vybrat jen jistou skupinu spojek, která sta'í pro vyjád#eníostatních spojek, a tuto skupinu pova"ovat za základní; ostatní spojky pak m&-"eme pova"ovat za odvozené ze základních (v tomto p#ípad! sta'í mít v jazycejen symboly základních spojek; symboly ostatních spojek m&"eme pou"ívat, alechápeme je jako definované pomocí symbol& pro základní spojky—to za chvíli

6

uvidíme). První postup je p#irozen!j$í (nebo+ "ádnou spojku neup#ednost(u-jeme), druh% je technicky v%hodn!j$í (nebo+ pracujeme s men$ím mno"stvímspojek). My zvolíme druh% postup. Je d&le"ité zmínit, "e oba postupy jsouekvivalentní (to my v$ak neuvidíme, proto"e první zp&sob ignorujeme; zvídav%'tená#m&"e první zp&sob domyslet, pop#. najít v literatu#e; podotkn!me pouze,"e #íkáme-li, "e oba postupy jsou ekvivalentní, myslíme tím, "e v$echna tvrzení,ke kter%m dosp!jeme na$ím zp&sobem, jsou (v odpovídající podob!) platná ip#i pou"ití prvního zp&sobu; DODELAT, nejspí$ do cvi'ení). Správn! by tedyv definici symbol& pro v%rokové spojky m!lo b%t p#i na$em p#ístupu uvedeno

• symbol" v!rokov!ch spojek (negace), (implikace);

Uvedení symbol& dal$ích spojek má za úkol stru'n! vyjád#it práv! vysv!tlenousituaci.P#istupme k dal$í definici.

Definice 2.3 Nech+ je dán jazyk v%rokové logiky. Formule daného jazykav%rokové logiky je definována následovn!:

• ka"d% v%rokov% symbol je formule (tzv. atomická formule);

• jsou-li ! a " formule, jsou i ! a (! ") formule.

P#íklad 2.4 Formulemi jsou tedy jisté kone'né posloupnosti symbol& jazykav%rokové logiky. Nap#. posloupnosti p, q1, p, (p q), ( p (q r)) jsouformule, naproti tomu posloupnosti pp, ((p , p nejsou formule. Posloupnost( p (q r)) je formule, proto"e: r je formule (atomická), tedy i r jeformule, co" spolu s tím, "e q je formule, dává, "e (q r) je formule; dále jep a tedy i p formule, a tedy kone'n! i ( p (q r)) je formule.

Zavedeme nyní symboly , , , jak jsme ohlásili v%$e. Jsou-li, ! a "posloupnosti symbol&, pak posloupnosti (! "), (! "), (! ") jsou zkratkyza následující posloupnosti:

(! ") je zkratkou za (! "),

(! ") je zkratkou za ( ! "),

(! ") je zkratkou za ((! ") (" !).

Vezm!me nap#. posloupnost ((p q) r). Ta je zkratkou za posloupnost((p q) r). Proto"e je dále (p q) zkratkou za (p q), je p&vodníposloupnost ((p q) q) zkratkou za posloupnost ( (p q) r),která jej ji" formulí. Podobn! je (p (q r)) zkratkou za formuli ( p (q r)) a ((p q) r) je zkratkou za ( ( (p q)) r). Uv!dommesi dále, "e proto"e (! ") je zkratkou za ((! ") (" !)), je takézkratkou za ((! ") (" !)). Jak je z práv! uvedeného z#ejmé,chápeme vztah “b%t zkratkou za” mezi posloupnostmi znak& za tranzitivní: je-li A zkratkou za B a B zkratkou za C, je A zkratkou za C. N!které posloupnostisestavené ze symbol& jazyka v%rokové logiky a symbol& , a jsou zkratkami

7

za posloupnosti, které ji" neobsahují , , ani ; n!které posloupnosti jsouzkratkou za posloupnosti, které jsou formulemi. Lze lehce ukázat, "e posloupnostA je zkratkou za formuli v%rokové logiky (tj. obsahuje jen spojky a ), práv!kdy" je formulí v%rokové logiky podle definice, která p#ipou$tí i , a jakosymboly spojek (DO CVI*ENÍ). Posloupnosti, které jsou zkratkami formulí,nejsou samy o sob! formule, pro jednoduchost jim v$ak formule #íkat budeme.Tedy #ekneme nap#íklad “formule (p q)”, p#esto"e bychom m!li správn! #íct“formule, její" zkratkou je (p q)”.

Poznámka 2.5 (1) Formule v%rokové logiky tedy odpovídají v%rok&m, repre-zentují formu v%rok&.(2) V$imn!me si, "e správn! bychom m!li #íkat “formule daného jazyka J

v%rokové logiky”. My v$ak v p#ípad!, "e jazyk J je z#ejm% z kontextu, pop#. neníd&le"it%, budeme #íkat pouze “formule v%rokové logiky” nebo jen “formule”.

Poznámka 2.6 (konvence o p#ehledn$j%ím zápisu formulí) Jak zná 'te-ná# z aritmetiky, je pro zjednodu$ení zápisu a 'tení u"ite'né vynechávat závorkytam, kde neutrpí jednozna'nost 'tení formule (nap#. místo (p q) m&"emeklidn! psát jen p q). Dále se dohodn!me na prioritách symbol& spojek a sym-bol& , a : od nejv!t$í po nejmen$í je to , , , , . To nám umo"nívynechávat závorky. Tak nap#. místo (p (q r)) m&"eme psát jen p (q r),místo (p ((p q) r)) jen p p q r apod. ('tená# jist! konvenceo vynechávání závorek zná, proto je nebudeme rozvád!t).

Poznámka 2.7 Formule jsou tedy jisté #et!zce nad abecedou (ozna'me ji ,)sestávající z v%rokov%ch symbol&, symbol& spojek (tj. a ) a pomocn%chsymbol& (tj. závorek; uva"ujme nyní pouze “kulaté” závorky “(” a “)”). Mno"inaFml v$ech formulí (daného jazyka v%rokové logiky)je tedy jazykem nad abecedou,. Tento jazyk je mo"né chápat jako jistou algebru, a to následovn!. Definujmena mno"in! ,! v$ech #et!zc& nad , unární operaci f a binární operaci fp#edpisem

f (u) = u

f (u, v) = (u v)

pro ka"dé u, v ! ,!. Je tedy nap#. f (p1p2 q ) = p1p2 q ,f (p q) = (p q), f ( , p (q ) = ( p (q ), f ((p p), q) =((p p) q). Je-li P mno"ina v$ech v%rokov%ch symbol&, pak Fml je práv!nosi'em podalgebry algebry ",!, f , f # generované mno"inou P . Skute'n!, . . .(DODELAT, je mo"né pou"ít princip strukturální indukce)

Formule byly definovány tzv. induktivním (nebo rekurzívním) zp&sobem.Krom! toho, "e takov% zp&sob nám umo"nil kone'n%m zp&sobem definovat ne-kone'nou mno"inu (mno"ina formulí je nekone'ná), umo"(uje nám navíc ele-gantn! dokazovat tvrzení tvaru “Ka"dá formule má vlastnost V”. Lehce lzetoti" nahlédnout, "e platí následující tvrzení.

V$ta 2.8 (d&kaz strukturální indukcí pro formule) Nech# V je vlastnostformulí. Nech# platí, $e

8

• ka$d! v!rokov! symbol má vlastnost V;

• mají-li formule ! a " vlastnost V, pak vlastnost V mají i formule ! a(! ").

Pak vlastnost V má ka$dá formule.

D̊ukaz. Pou"ijeme princip strukturální indukce z V!ty 7.1. Nech+ A, B a C (vizV!tu 7.1) jsou po #ad! algebry ",!, f , f #, "Fml, f , f # a mno"ina P v$echv%rokov%ch symbol& (viz Poznámku 2.7). Dokazované tvrzení je p#ím%m d&-sledkem V!ty 7.1 a faktu, "e "Fml, f , f # je podalgebra generovaná mno"inouP . !

(K UVAZE: zavest spec. znaceni pro mnozinu symbolu jazyka)

P#íklad 2.9 Uka"me si pou"ití d&kazu strukturální indukcí na jednoduchémp#íklad!. Chceme dokázat, "e po'et lev%ch závorek je v ka"dé formuli rovenpo'tu prav%ch závorek. To tvrzení je tém!# z#ejmé. Nic to v$ak nem!ní nafaktu, "e je t#eba ho dokázat; dal$í tvrzení t%kající se formulí ji" nebudou takz#ejmá. D&kaz strukturální indukcí pou"ijeme následovn!: Vlastnost V , o kterouzde jde, je “mít stejn% po'et lev%ch a prav%ch závorek”. To, "e ka"d% v%rokov%symbol má vlastnost V je z#ejmé, nebo+ v%rokov% symbol nemá "ádné závorky(tedy má 0 lev%ch a 0 prav%ch). Mají-li formule ! a " vlastnost V , tj. mají-listejn% po'et lev%ch i prav%ch závorek, pak vlastnost V mají i formule ! a(! "). Opravdu, ozna'íme-li pomocí l(A) a r(A) po'et lev%ch a prav%chzávorek v posloupnosti A, pak pomocí induk'ního p#edpokladu (tím je tvrzení,"e l(!) = r(!) a l(") = r(")) dostáváme l( !) = l(!) = r(!) = r( !) apodobn! l(! ") = l(!) + l(") + 1 = r(!) + r(") + 1 = r(! ").

P#íklad 2.10 (cvi'ení) Doka"te strukturální indukcí, "e nahradíme-li ve for-muli v%rokové symboly formulemi, dostaneme op!t formuli (p#itom jeden v%ro-kov% symbol m&"eme na r&zn%ch místech nahradit r&zn%mi formulemi). Stejnétvrzení platí, nahrazujeme-li podformule dané formule formulemi (p#itom pod-formulí dané formule je formule, která je nachází v dané formuli jako pod#et!zec;tj. nap#. formule (p q) p má podformule sebe samu, (p q), p a q).

2.3 Základní sémantické pojmy

Zatím jsme se v!novali jen tzv. syntaktické stránce v%rokové logiky. Víme, coje to jazyk v%rokové logiky, co jsou to formule. Zatím v$ak nevíme, co to jepravdivá formule apod. Formule jsou jisté posloupnosti symbol& jazyka, samy osob! v$ak nemají "ádn% v%znam. P#i#azení v%znamu syntaktick%m objekt&m jezále"itostí tzv. sémantiky. Práv! sémantikou v%rokové logiky se v dal$ím budemev!novat.

Definice 2.11 (Pravdivostní) ohodnocení je libovolné zobrazení v%roko-v%ch symbol& daného jazyka v%rokové logiky do mno"iny {0, 1}, tj. libovolnézobrazení e p#i#azující ka"dému v%rokovému symbolu p hodnotu e(p) ! {0, 1}.

9

Poznámka 2.12 (1) 0 a 1 reprezentují pravdivostní hodnoty nepravda a pravda.(2) V%znam ohodnocení e m&"eme chápat následovn!: V%rokové symboly

ozna'ují v%roky. Zadáme-li ohodnocení e, pak v%rokov% symbol p ozna'uje v%-rok, kter% má pravdivostní hodnotu e(p). Na to lze nahlí"et dv!ma zp&soby.Za prvé, v%rok ozna'en% symbolem p známe a pova"ujeme jej za pravdiv% (ne-pravdiv%). Pak polo"íme e(p) = 1 (e(p) = 0). Za druhé, pravdivostní hodnotuv%roku ozna'eného symbolem p neznáme. Polo"íme-li pak e(p) = 1 (e(p) = 0),omezujeme se na situace, kdy v%rok ozna'en% symbolem p je pravdiv% (nap#.kdy" nás zajímá, co vypl%vá z pravdivosti zmi(ovaného v%roku apod.).

Je-li dáno ohodnocení e, m&"eme #íci, co je to pravdivostní hodnota for-mule. Pravdivostní hodnota libovolné formule je pravdivostním ohodnocenímjednozna'n! ur'ena a je definována následovn!.

Definice 2.13 Nech+ je dáno ohodnocení e. Pravdivostní hodnota formule !p#i ohodnocení e, ozna'ujeme ji $!$e, je definována následovn!:

• $p$e = e(p) pro v%rokov% symbol p;

• $ !$e = 1 pokud $!$e = 0, $ !$e = 0 pokud $!$e = 1; a $(!")$e = 1, pokud $!$e = 0 nebo $"$e = 1, $(! ")$e = 0 jinak.

Je-li $!$e = 1 ($!$e = 0), #íkáme, "e formule ! je p#i ohodnocení e pravdivá(nepravdivá). Uv!domme si, "e nemá smysl #íci “formule ! je pravdivá” nebo“nepravdivá” (musíme #íci, p#i jakém ohodnocení!).

Poznámka 2.14 Lehce je vid!t (ov!#te si), "e $(! ")$e = 1, práv! kdy"$!$e = 1 a $"$e = 1 (a tedy $(! ")$e = 0 jinak, tj. pokud $!$e = 0 nebo$"$e = 0); $(! ")$e = 1, práv! kdy" $!$e = 1 nebo $"$e = 1 (a tedy$(! ")$e = 0 jinak, tj. pokud $!$e = 0 i $"$e = 0); $(! ")$e = 1, práv!kdy" $!$e = $"$e.

ALTERNATIVN-: zadávání pravdivostních funkcí logick%ch spojek tabul-kou:

a ¬a0 11 0

% 0 10 1 11 1 0

Definice 2.15 Formule se naz%vá tautologie ( kontradikce ), je-li p#i ka"-dém ohodnocení pravdivá (nepravdivá). Formule se naz%vá splnitelná , je-lip#i n!jakém ohodnocení pravdivá.

Je-li ! tautologie, pí$eme také |= !, pop#. $!$ = 1. Zjistit pravdivostníhodnotu formule p#i daném ohodnocení je snadné, lze to provést p#ímo z definice.Zjistit, zda je formule tautologií, kontradikcí, pop#. splnitelná, v$ak dle definiceznamená zjistit její pravdivostní hodnotu (v nejhor$ím p#ípad!) pro v$echnaohodnocení. Díky následujícímu tvrzení to v$ak není nutné.Je-li ! formule v%rokové logiky, pí$eme také !(p1, . . . , pn), chceme-li zd&raz-

nit, "e v$echny v%rokové symboly vyskytující se v ! jsou mezi p1, . . . , pn (tj."ádn% jin% v%rokov% symbol ne" n!kter% z p1, . . . , pn se v ! nevyskytuje).

10

Lemma 2.16 Platí-li pro ohodnocení e a e", $e e(p1) = e"(p1), . . . , e(pn) =e"(pn), pro ka$dou formuli !(p1, . . . , pn) platí $!$e = $!$e! .

P#íklad 2.17 Doka"te p#edchozí lemma strukturální indukcí (lemma je tém!#z#ejmé, procvi'íte si v$ak strukturální indukci).

Jinak #e'eno, pravdivostní hodnota formule závisí jen na tom, jaké hodnotyp#i#azuje dané ohodnocení v%rokov%m symbol&m, které se ve formuli vyskytují.Pro n v%rokov%ch symbol& p1, . . . , pn existuje práv! 2n r&zn%ch ohodnocení sym-bol& p1, . . . , pn (ka"dému pi se p#i#azuje 0 nebo 1). Tyto úvahy jsou základemtzv. tabulkové metody pro zji$t!ní pravdivostních hodnot formule: Tabulka proformuli, která obsahuje n v%rokov%ch symbol&, má 2n #ádk&, ka"d% #ádek od-povídá pravdivostnímu ohodnocení, na konec ka"dého #ádku (tj. do posledníhosloupce) zapí$eme pravdivostní hodnotu formule p#i odpovídajícím ohodnocení(viz p#edná$ky). Formule je tautologií (kontradikcí, splnitelnou), práv! kdy"jí odpovídající tabulka pravdivostních hodnot má v posledním sloupci samé 1(samé 0, aspo( jednu 1).

P#íklad 2.18 Nap#. p p je tautologie, p p je kontradikce, p q jesplnitelná (která není tautologií).

Definice 2.19 Formule " sémanticky plyne z formule ! (zna'íme ! |= "),jestli"e " je pravdivá p#i ka"dém ohodnocení, p#i kterém je pravdivá !. Pokud "sémanticky plyne z ! a naopak, #íkáme, "e ! a " jsou sémanticky ekvivalentní.Obecn!ji, " sémanticky plyne z mno"iny T formulí (zna'íme T |= "), je-li "pravdivá p#i ka"dém ohodnocení, p#i kterém je pravdivá ka"dá formule z T .

Poznámka 2.20 Práv! zavedené pou"ití symbolu |= je v souladu s d#íve zave-den%m |= ! pro ozna'ení faktu, "e ! je tautologie. Skute'n!, chápeme-li |= vesmyslu sémantického vypl%vání a chápeme-li dále |= ! jako & |= !, pak |= !znamená, "e pro ka"dé ohodnocení e platí, "e je-li p#i e pravdivá ka"dá formulez & ("ádná taková ale není), pak je p#i e pravdivá také !. To v$ak znamená, "epro ka"dé ohodnocení e je formule ! pravdivá.

Ke ka"dé formuli v%rokové logiky existuje s ní (sémanticky) ekvivalentní for-mule, která je ve tvaru úplné konjunktivní normální formy (úplné disjunktivnínormální formy); viz p#edná$ky (literál je v%rokov% symbol nebo jeho negace;úplná elementární konjunkce (disjunkce) na danou mno"inou V v%rokov%ch sym-bol& je konjunkce (disjunkce) literál&, ve které se ka"d% v%rokov% symbol z Vvyskytuje práv! v jednom literálu; úplná disjunktivní (konjunktivní) normálníforma (nad V ) je disjunkce (konjunkce) úpln%ch elementárních konjunkcí (dis-junkcí) (nad V ); konstrukce ÚDNF dané formule !: z tabulky pravdivostníchhodnot ! se vyberou #ádky, pro které je formule pravdivá a pro ka"d% takov%#ádek se vytvo#í úplná elementární konjunkce takto: pro ka"d% v%rokov% symbolp formule ! se vytvo#í odpovídající literál, p#itom má-li p v ohodnocení p#íslu$-ném tomuto #ádku hodnotu 1, je tím literálem p#ímo p, má-li hodnotu 0, je tímliterálem p; takto vybrané literály se spojí konjunkcí; takto vytvo#ené kon-junkce se spojí disjunkcí — zd&vodn!te, pro' takto skute'né vznikne formule

11

ekvivalentní p&vodní formuli !; duáln! se vytvo#í úplná disjunktivní normálníforma).

P#íklad 2.21 Zjist!te, zda formule " sémanticky plyne z !: (a) ! je (p q) r," je p (q r); (b) ! je (p q) r, " je p (q r). .e$ení: V prvnímp#ípad! ano, ve druhém ne.

P#íklad 2.22 (1) P#esv!d'te se, "e je-li " |= ! a ! |= #, pak " |= #. [#e$ení:jednoduchou úvahou: máme ukázat " |= #; nech+ e je ohodnocení p#i kterémje " pravdivá; dle p#edpokladu " |= ! je p#i e pravdivá také !, a tedy dlep#edpokladu ! |= # je p#i e pravdivá také #, co" jsme m!li ukázat].(2) Doka"te, "e pro libovolnou mno"inu T formulí a formule !," platí

T,! |= " práv! kdy" T |= ! ".

To je sémantická podoba tzv. v!ty o dedukci (viz pozd!ji). P#itom T,! znamenáT ' {!} (tato dohoda se v logice pou"ívá 'asto). [D&kaz je velmi snadn%, sta'ísi rozmyslet, co máme dokázat: #e$ení: P#edpokládejme T,! |= " a doka"meT |= ! ". Máme tedy dokázat, "e je-li e ohodnocení, p#i kterém jsou pravdivév$echny formule z T , je p#i e pravdivá i formule ! ". Kdyby ale p#i e nebylapravdivá formule ! ", musela by b%t p#i e ! pravdivá a " nepravdivá (zdefinice pravdivostních hodnot implikace). Je-li ale p#i e pravdivá ! i v$echnyformule z T , pak je dle p#edpokladu T,! |= " pravdivá i ", co" je spor s tím,"e " je nepravdivá. Naopak, p#edpokládejme T |= ! " a doka"me T,! |= ".Máme dokázat, "e je-li e ohodnocení, p#i kterém je pravdivá ! i v$echny formulez T , je p#i n!m pravdivá i ". Dle p#edpokladu je ov$em p#i e pravdivá i ! "a proto"e je p#i e pravdivá i !, je p#i e pravdivá i ", co" jsme m!li dokázat.]

2.4 Axiomatick! systém v!rokové logiky

Idea axiomatického systému: V ka"dodenním "ivot! se dobíráme dal$ích v!cínásledovn!: Vyjdeme z toho, co víme nebo co p#edpokládáme a pou"itím usu-zování (i v b!"ném "ivot! #íkáme “logicky správného usuzování”) odvozujeme zp#edpoklad& nové a nové záv!ry. Snaha p#ijít na kloub tomu, jak vlastn! 'lov!kusuzuje, provází 'lov!ka po staletí. Uv!domme si, "e zejména z pohledu infor-matiky je otázka, jak 'lov!k usuzuje, zcela zásadní. P#edstava, "e do po'íta'e“nasypeme” to, co víme nebo p#edpokládáme (o n!jaké oblasti, která nás za-jímá), a "e po'íta' nám pomocí algoritmizovaného (automatizovaného) postupuusuzování nabídne záv!ry, je toti" velmi lákavá (i kdy" se o tom v tomto textunedozvíme, podotkn!me, "e tato problematika pat#í mezi podrobn! studovanéotázky teoretické informatiky, které mají aplikaci v um!lé inteligenci, tzv. logic-kém programování; jak jist! 'tená# uzná, tyto otázky mají sv&j p&vab a zcelazásadní charakter i z hlediska filozofického (mohou po'íta'e myslet?)).Otázka po podstat! usuzování, které v b!"ném "ivot! naz%váme logicky

správn%m, je základní otázkou matematické logiky. V logice postupujeme p#iformalizaci v%$e uvedeného následovn!:

12

To, co víme nebo p#edpokládáme, se naz%vá axiomy, pop#. p#edpoklady(p#edpokládáme v"dy v%roky, tj. tvrzení, a ty jsou v logice reprezentovány for-mulemi, axiomy jsou tedy formule). Elementární úsudkov% krok je realizovánpomocí tzv. odvozovacího (inferen'ního) pravidla (to je tvaru “z formulí tvarutoho a toho odvo) formuli tu a tu”). Záznam odvozování, proveden% tak, "eza sebe napí$eme tvrzení (formule), ke kter%m se postupn! dobíráme tak, "eza'neme p#edpoklady (axiomy) a pokra'ujeme tvrzeními (formulemi), které zp#edchozích tvrzení (formulí) plynou pomocí elemenntárních úsudkov%ch krok&(odvozovacích pravidel), naz%váme d&kaz. Tvrzení pova"ujeme za zd&vodnitelné(dokazatelné) z dané mno"iny p#edpoklad& (axiom&, pop#. dal$ích dodate'n%chp#edpoklad&), pokud k n!mu existuje d&kaz. Takto navr"en% formální systémpotom naz%váme axiomatick%m systémem.V následujícím uvedeme jeden konkrétní axiomatick% systém v%rokové logiky

a prozkoumáme jeho vlastnosti. Axiomatick% systém má axiomy a odvozovacípravidla.Ná$ axiomatick% systém má za axiomy jakékoli formule, které jsou n!kterého

z následujících tvar& (tzv. axiomov%ch schémat):

! (" !) (1)

(! (" #)) ((! ") (! #)) (2)

( " !) (! "). (3)

Ná$ axiomatick% systém má dále jedno odvozovací pravidlo naz%vané modusponens (MP, pravidlo odlou'ení), které #íká

z formulí ! a ! " odvo) ".

.ekneme, "e formule je axiomem, jestli"e vznikne z n!kterého z axiomo-v%ch schémat (1)–(3) nahrazením symbol& !,",# po #ad! n!jak%mi formulemi$1, $2, $3. Tedy nap#. (p p) ( p (p p)) je axiom, nebo+ vzniknez (1) nahrazením ! a " po #ad! formulemi (p p) a p.

Definice 2.23 D"kaz formule ! z mno"iny T formulí je libovolná posloupnost!1, . . . ,!n, pro kterou platí, "e !n = ! a ka"dá !i

• je axiomem

• nebo je formulí z T

• nebo plyne z p#edchozích formulí d&kazu pomocí odvozovacího pravidlaMP (tj. existují j, k < i (1 ( j ( n, 1 ( k ( n) tak "e !k je formule!j !i).

Formule se naz%vá dokazatelná z T , existuje-li d&kaz této formule z T (za-pisujeme T ) !, pop#. jen ) !, je-li T prázdná mno"ina).

Poznámka 2.24 (1) Máme tedy p#esn% pojem d&kazu v na$em axiomatickémsystému (pojem d&kazu se tak p#ená$í z úrovn! intuice na p#esnou formálníúrove().

13

(2) Máme dva pojmy vypl%vání formule z mno"iny formulí: sémantické vy-pl%vání (T |= !) a syntaktické vypl%vání (T ) !). Jak spolu souvisí, uvidímepozd!ji (viz v!ta o úplnosti).(3) Speciáln! máme dva pojmy platnosti formule: |= ! ozna'uje platnost !

v sémantickém smyslu (pravdivost), ) ! ozna'uje platnost ! v syntaktickémsmyslu (dokazatelnost).

Pojem d&kaz je matematick% objekt (formální pojem), se kter%m lze praco-vat jako s ka"d%m jin%m matematick%m objektem. Uka"me to na následujícímpozorování.

Pozorování 2.25 Pro ka$dou mno$inu T formulí a formule !," platí, $e zT ) ! " a T ) ! plyne T ) ".

D̊ukaz. Máme tedy dokázat, "e jsou-li z T dokazatelné formule ! " a !, pakje z T dokazatelná i formule ". Jsou-li v$ak z T dokazatelné formule ! " a !,znamená to, "e existuje d&kaz (tj. posloupnost formulí spl(ující podmínky toho,aby byla d&kazem) #1, . . . ,#n formule ! " z T (tj. #n je formulí ! ") a"e existuje d&kaz $1, . . . , $m formule ! z T (tj. $m je formulí !). Nyní v$ak sta'ívzít posloupnost #1, . . . ,#n, $1, . . . , $m,"—ta je toti" d&kazem formule " z T .Abychom se o tom p#esv!d'ili, sta'í ov!#it podmínky z definice pojmu d&kaz.Vezm!me libovolnou formuli uva"ované posloupnosti. Pak je to bu) formule#i (pro n!jaké i) nebo formule $j nebo formule ". V prvním p#ípad! (je to#i) uva"ujme takto: proto"e posloupnost #1, . . . ,#n je d&kazem, je #i axiomemnebo je formulí z T nebo plyne z n!jak%ch p#edchozích #j ,#k pomocí MP. Vedruhém p#ípad! uva"ujme podobn!. Ve t#etím p#ípad! plyne uva"ovaná formule(je to ") pomocí MP z formulí #n (co" je ! ") a $m (co" je !). Vidíme tedy,"e posloupnost #1, . . . ,#n, $1, . . . , $m," je d&kazem " z T , tj. T ) ". !

Definice 2.26 Mno"ina T formulí se naz%vá sporná (nekonzistentní), jestli"ez ní je dokazatelná ka"dá formule. Není-li T sporná (tj. existuje formule, kteránení z T dokazatelná), naz%vá se bezesporná (konzistentní).

Uka"me n!které dokazatelné formule a p#íklady d&kaz&.

V$ta 2.27 Pro ka$dou formuli ! platí ) ! ! (tj. formule ! ! je dokaza-telná v na%em axiomatickém systému).

D̊ukaz. Máme ukázat, "e existuje d&kaz (z prázdné mno"iny T ), jeho" poslednímprvkem je ! !. D&kazem je nap#. posloupnost formulí

! ((! !) !) [1. formule d&kazu, tato formule je axiomem dle (1)](! ((! !) !)) ((! (! !)) (! !)) [2. formule d&kazu,

tato formule je axiomem dle (2)](! (! !)) (! !) [3. formule d&kazu, tato formule vypl%vá z

p#edchozích dvou pomocí MP]

14

! (! !) [4. formule d&kazu, tato formule je axiomem dle (1)]! ! [5. formule d&kazu, dokazovaná formule, vypl%vá ze dvou p#edchozích

formulí pomocí MP]. !

Následující v!ta umo"(uje mimo jiné zkracovat d&kazy.

V$ta 2.28 (o dedukci) Pro ka$dou mno$inu T formulí a formule !," platí

T,! ) " práv& kdy$ T ) ! ".

D̊ukaz. “*”: P#edpokládáme-li T ) ! ", je tím spí$e T,! ) ! ". Pou"itímMP okam"it! dostáváme T,! ) ".“+”: Nech+ T,! ) ", tj. existuje d&kaz "1, . . . ,"n formule " z T,! ("n = ").

Indukcí doká"eme, "e T ) ! "i platí pro i = 1, . . . , n, z 'eho" plyne po"ado-van% vztah (je speciálním p#ípadem pro i = n). Vezm!me tedy i ! {1, . . . , n} ap#edpokládejme, "e pro ka"dé j < i je T ) ! "j (induk'ní p#edpoklad). Do-ká"eme, "e T ) ! "i. Podle definice d&kazu mohou nastat pouze následujícíp#ípady:

• "i je axiom nebo formule z T . Pak je posloupnost formulí

"i (! "i) [axiom typu (1)]

"i [podle p#edpokladu axiom nebo formule z T ]

! "i [pou"ití MP]

d&kazem formule ! "i z T .

• "i je formulí !. Pak T ) ! "i plyne z V!ty 2.27.

• "i plyne z p#edchozích formulí "j ,"k = "j "i (j, k < i) pomocí MP. Dleinduk'ního p#edpokladu existuje d&kaz %, . . . ,"j z T a d&kaz &, . . . ,"j

"i z T . P#idáme-li k posloupnosti %, . . . ,"j ,&, . . . ,"j "i formule

(! ("j "i)) ((! "j) (! "i)) [axiom typu 3]

(! "j) (! "i) [pou"ití MP]

! "i [pou"ití MP],

dostaneme d&kaz formule ! "i z T .

D&kaz je hotov. !

Poznámka 2.29 V situacích, kdy máme ukázat, "e platí T ) ! (tj., "e z T jedokazatelné !), budeme postupovat dv!ma zp&soby (jde nám te) zejména o to,jak p#ehledn! zapisovat argumenty prokazující T ) !).První zp&sob: Budeme postupn! vypisovat formule (spolu se zd&vodn!ním

a komentá#em), které tvo#í, tak jak jsou uvedeny za sebou, d&kaz formule ! zT . Tímto zp&sobem postupujeme v d&kazu V!ty 2.27.Druh% zp&sob: Tvrzení T ) ! doká"eme tak, "e uvedeme posloupnost po-

stupn! zd&vod(ovan%ch tvrzení tvaru Ti ) !i, p#i'em" posledním bude dokazo-vané tvrzení ) ! (tj. Ti = & a !i = !). Tímto zp&sobem postupujeme v d&kazuV!ty 2.31.

15

P#íklad 2.30 Uka"me pou"ití v!ty o dedukci. Uka"me, "e jestli"e T ) ! "a T ) " #, pak T ) ! # (tomuto tvrzení #íkáme princip tranzitivityimplikace). Skute'n!, máme T,! ) " (dle v!ty o dedukci aplikované na T )! "), dále T,! ) # (pou"itím MP), a kone'n! T ) ! # (v!ta o dedukcipou"itá na T,! ) #).

Následují u"ite'né dokazatelné formule a vztahy.

V$ta 2.31 Pro formule !," platí

• ) ! (! "),

• ) ! !,

• ) ! !,

• ) (! ") ( " !),

• ) ! ( " (! "))

D̊ukaz. Uvedená tvrzení jsou tvaru ) !. Ka"dé z nich doká"eme tak, "e uvedemeposloupnost postupn! zd&vod(ovan%ch tvrzení tvaru Ti ) !i, p#i'em" poslednímbude dokazované tvrzení ) ! (tj. Ti = & a !i = !).

“) ! (! ")”:) ! ( " !) [axiom (1): formule ! ( " !) je instancí

axiomu (1); ) " platí pro ka"d% axiom "]( " !) (! ") [axiom (3)]) ! (! ") [princip tranzitivity implikace pou"it% na v%$e uvedená

tvrzení].

“) ! !”:) ! ( ! !) [práv! dokázané tvrzení: pou"ití práv! dokázaného

tvrzení pro ! := !, " := !]! ) ( ! !) [v!ta o dedukci: pou"ití v!ty o dedukci pro T := &,

! := !, " := ( ! !)]( ! !) ( ! !) [axiom (3)]

! ) ! ! [MP (resp. Pozorování 2.25) pou"ité na p#edchozí dv!tvrzení]

! ) ! [v!ta o dedukci a fakt, "e ! ! je ekvivalentní !, ! )!]

) ! ! [v!ta o dedukci]

“) ! !”:) ! ! [p#edchozí tvrzení]) ( ! !) (! !) [axiom (3)]) ! ! [MP]

“) (! ") ( " !)”:) ! !, ) " " [p#edchozí tvrzení]

16

(! ") ) ( ! ") [princip tranzitivity implikace (dvakrát)]( ! ") ( " !) [axiom (3)](! ") ) ( " !) [MP]) (! ") ( " !) [v!ta o dedukci]

“) ! ( " (! "))”:!,! " ) " [MP]! ) (! ") " [v!ta o dedukci]! ) ((! ") " ( " (! "))) [p#edchozí tvrzení]! ) " (! ")) [MP]) ! " (! ")) [v!ta o dedukci]

!

Jsou-li ! formule, p1, . . . , pn po dvou r&zné v%rokové symboly a !1, . . . ,!n

formule, ozna'íme symbolem !(p1/!1, . . . , pn/!n) formuli, která vznikne z for-mule ! nahrazením v$ech v%skyt& symbol& p1, . . . , pn po #ad! formulemi !1, . . . ,!n.Je z#ejmé, "e !(p1/!1, . . . , pn/!n) je skute'n! formule.

V$ta 2.32 (o nahrazení) Pro libovolné formule !,!1, . . . ,!n a libovolné podvou r"zné v!rokové symboly p1, . . . , pn platí, $e z ) !(p1, . . . , pn) plyne )!(p1/!1, . . . , pn/!n).

D̊ukaz. D&kaz je jednoduch%. P#edpokládejme, "e ) !. Je-li $1, . . . , $l d&kaz for-mule ! (tj. $l = !), sta'í dokázat, "e $1(p1/!1, . . . , pn/!n), . . . , $l(p1/!1, . . . , pn/!n)je také d&kazem (to ov!#íme), a sice d&kazem formule !(p1/!1, . . . , pn/!n) (to jez#ejmé, proto"e $l = !). Zb%vá tedy ukázat, "e $1(p1/!1, . . . , pn/!n), . . . , $l(p1/!1, . . . , pn/!n)je d&kaz. Musíme ov!#it, "e uvedená posloupnost formulí spl(uje podmínky de-finice d&kazu. Uva"ujme libovoln% 'len $i(p1/!1, . . . , pn/!n) této posloupnosti.Proto"e p&vodní posloupnost $1, . . . , $l je d&kazem, nastávají pro $i následujícídv! mo"nosti.První: $i je axiom. Pak je ale axiomem také $i(p1/!1, . . . , pn/!n) (pro'?).Druhá: $i vznikne pou"itím MP na n!jaké $j , $k, j, k < i. Pak ale vznikne

$i(p1/!1, . . . , pn/!n) pou"itím MP na $j(p1/!1, . . . , pn/!n) a $k(p1/!1, . . . , pn/!n)(pro'?).Vidíme tedy, "e ka"d% 'len $i(p1/!1, . . . , pn/!n) je bu) axiomem nebo vznikne

pou"itím MP na p#edcházející 'leny, a tedy uvedená posloupnost je d&kazem. !

Poznámka 2.33 V!ta 2.32 tedy #íká, "e je-li ! dokazatelná formule, její" v$echnyv%rokové symboly jsou mezi p1, . . . , pn, pak nahradíme-li v$echny v%skyty sym-bol& pi formulemi !i, takto vzniklá formule !(p1/!1, . . . , pn/!n) je také dokaza-telná. V$imn!me si, "e platí i obecn!j$í tvrzení: Jsou-li q1, . . . , qk ! {p1, . . . , pn}v%rokové symboly, které se vyskytují v ! (ale nemusí to b%t v$echny, ! m&"e ob-sahovat i jiné ne" qj), pak nahradíme-li v$echny v%skyty prom!nn%ch q1, . . . , qk

po #ad! formulemi !1, . . . ,!n a ozna'íme-li takto vzniklou formuli ", pak zdokazatelnosti ! plyne dokazatelnost ". Pro' tomu tak je? [nápov!da: Ve for-muli !(p1/!1, . . . , pn/!n) mohou b%t n!které !i rovny p#ímo pi, a tedy jako byprobíhala substituce jen za n!které pi]

17

V$ta 2.34 (o ekvivalenci) Vznikne-li formule " a formule ! nahrazením je-jích podformulí !1, . . . ,!n po 'ad& formulemi "1, . . . ,"n, pak

!1 "1,"1 !1, . . . ,#n !n,"n !n ) ! ".

Z ) ! tedy plyne !1 "1,"1 !1, . . . ,#n !n,"n !n ) ".

D̊ukaz. Viz p#edná$ky. !

V$ta 2.35 (o d&kazu sporem) Pro teorii T a formule ! a " je T ) !, práv&kdy$ T, ! ) (" ").

D̊ukaz. “+”: P#edpokládejme T ) !. Máme) ! (! (" ")) [V!ta 2.31]T, ! ) (! (" ")) [v!ta o dedukci]T, ! ) (" ") [MP na p#edchozí vztah a na p#edpoklad T ) !].

“*”: P#edpokládejme T, ! ) (" "). MámeT ) ! (" ") [v!ta o dedukci]) [ ! (" ")] [(" ") !] [axiom (3)]T ) (" ") ! [MP]) " " [V!ta 2.27]T ) ! [MP]. !

V$ta 2.36 (o d&kazu rozborem p#ípad&) Pro teorii T a formule !, ", #platí T,! " ) # práv& kdy$ T,! ) # a T," ) #.

D̊ukaz. P#edpokládejme T,! " ) #, tj. T, ! " ) #. Máme ! (! ") (V!ta 2.31), pou"itím MP tedy T,! ) ! ", co" dále s pou"itímp#edpokladu T, ! " ) # dává T,! ) #. Fakt T," ) # dostaneme obdobn!pou"itím " ( ! ") (axiom (1)).P#edpokládejme T,! ) # a T," ) #. MámeT ) ! # [v!ta o dedukci]T ) " # [v!ta o dedukci]T ) (! #) ( # !) [V!ta 2.31]T ) # ! [MP]T, ! " ) # # [princip tranzitivity implikace: máme T ) # !,

v p#edpokladu ! ", T ) " #]) # ( # ( # #)) [V!ta 2.31 pou"itá na # a #]) # ( # #) [3, v!ta o dedukci (dvakrát p#esun vlevo, jednou

vpravo)]( # #) # [axiom (3) a MP na p#edchozí dokazatelnost]T, ! " ) # [MP na p#edchozí],'ím" je tvrzení dokázané, nebo+ ! " je zkratkou za ! ". !

18

V$ta 2.37 (o neutrální formuli) Pro teorii T a formule ! a " platí T ) ",práv& kdy$ T,! ) " a T, ! ) ".

D̊ukaz. Podle V!ty o d&kazu rozborem p#ípad& je T,! ! ) ", práv! kdy"T,! ) " a T, ! ) ". Dále v$ak platí, "e T,! ! ) ", práv! kdy" T ) "(nebo+ ! ! je zkratkou za ! !, co" je dokazatelná formule dleV!ty 2.27; pro dokazatelnou % je v"dy T,% ) &, práv! kdy" T ) &), a tím jed&kaz hotov. !

Vid!li jsme formule, které jsou v na$em axiomatickém systému dokazatelné.V následujícím se lehce p#esv!d'íme, "e ka"dá dokazatelná formule je tautologií.Vzniká otázka, zda také naopak je ka"dá tautologie dokazatelná. Uvidíme, "eano (a uvidíme i více). Jin%mi slovy, na$e axiomy a odvozovací pravidlo (obojíje velmi jednoduché) jsou zvoleny tak vhodn!, "e umo"(ují dokázat v$echnytautologie, ale "ádné dal$í formule (tj. formule, které jsou n!kdy nepravdivé).

V$ta 2.38 (o korektnosti) Pro libovolnou mno$inu T formulí a formuli !platí, $e je-li T ) !, pak T |= !. Speciáln& tedy, ka$dá dokazatelná formule jetautologií.

D̊ukaz. Nejprve pro T = &. Ka"d% axiom je tautologie (p#esv!d'te se nap#.tabulkovou metodou). Dále platí, "e jsou-li ! a ! " tautologie, je i " tauto-logie (je ihned vid!t, ov!#te). Indukcí tedy dostáváme, "e ka"d% 'len d&kazu jetautologie. Tedy ka"dá dokazatelná formule je tautologie.Je-li T -= &, pak z T ) ! plyne, "e pro n!jaké "1, . . . ,"n ! T je "1, . . . ,"n )

!. n-násobn%m pou"itím v!ty o dedukci odtud dostaneme ) "1 ("2(· · · ("n !) · · ·)), z 'eho" dle v%$e dokázaného plyne |= "1 ("2 (· · · ("n

!) · · ·)). Nyní n-násobn! pou"ijeme “sémantické verze” v!ty o dedukci (viz P#í-klad 2.21) a dostaneme "1, . . . ,"n |= !, z 'eho" plyne (uv!domte si pro') T |= !.!

P#ed d&kazem v!ty o úplnosti zavedeme následující zna'ení. Pro formuli !a ohodnocení e je

!e =!

! pokud $!$e = 1! pokud $!$e = 0.

Lemma 2.39 Pro libovolnou formuli !, která neobsahuje jiné v!rokové symbolyne$ p1, . . . , pn, platí

pe1, . . . , p

en ) !e.

D̊ukaz. Tvrzení doká"eme indukcí p#es slo"itost formule !.Nech+ ! je v%rokov% symbol p. Pak je tvrzení z#ejmé.Nech+ tvrzení platí pro !. Uka"me, "e pak platí i pro !, tj. "e pe

1, . . . , pen )

( !)e. Rozli$me dva p#ípady, $!$e = 0 a $!$e = 1. Pro $!$e = 0 je !e = !a ( !)e = !. Po"adované tvrzení pe

1, . . . , pen ) ( !)e tedy p#ímo plyne z

19

p#edpokladu. Pro $!$e = 1 je !e = ! a ( !)e = !. Podle p#edpokladuje tedy pe

1, . . . , pen ) ! a máme dokázat pe

1, . . . , pen ) !. To v$ak plyne z

pe1, . . . , p

en ) ! a z ) ! ! (viz V!ta 2.31) pomocí MP.

Nech+ tvrzení platí pro ! a ". Uka"me, "e pak platí i pro ! ", tj. "epe1, . . . , p

en ) (! ")e. Mohou nastat následující p#ípady:

• $!$e = 0: Pak je $! "$e = 1, tedy (! ")e = ! ". Podlep#edpokladu máme pe

1, . . . , pen ) !. Podle V!ty 2.31 je ) ! (! "),

odkud pomocí MP dostaneme po"adované pe1, . . . , p

en ) ! ".

• $"$e = 1: Pak je $! "$e = 1, tedy op!t (! ")e = ! ". Podlep#edpokladu máme pe

1, . . . , pen ) ". Z (1) a MP dostaneme po"adované

pe1, . . . , p

en ) ! ".

• $!$e = 1 a $"$e = 0: Pak $! "$e = 0, tedy (! ")e = (!"). Podle p#edpokladu je pe

1, . . . , pen ) ! a pe

1, . . . , pen ) ". Pou"itím

V!ty 2.31 (poslední uvedená dokazatelnost) a dvojnásobn%mpou"itím MPdostaneme po"adované pe

1, . . . , pen ) (! ").

!

V$ta 2.40 (o úplnosti, slabá verze) Pro libovolnou kone(nou mno$inu T for-mulí a formuli ! platí, $e z T |= ! plyne T ) !. Speciáln&, ka$dá pravdiváformule je dokazatelná.

D̊ukaz. Tvrzení doká"eme nejd#íve pro p#ípad T = &. Nech+ tedy |= !. Proka"dé ohodnocení e tedy platí !e = ! (proto"e podle p#edpokladu je $!$e = 1).Jsou-li p1, . . . , pn v$echny v%rokové symboly z !, je tedy dle Lemma 2.39

pe1, p

e2, . . . , p

en ) !.

Uva"ujme nyní ohodnocení e", které se o e li$í práv! v hodnot!, kterou p#i#azujesymbolu p1. P#edpokládejme, "e e(p1) = 1 a e"(p1) = 0 (p#ípad e(p1) = 0 ae"(p1) = 1 se o$et#í symetricky). Dle Lemma 2.39 je op!t

pe!

1 , pe!

2 , . . . , pe!

n ) !.

Proto"e je v$ak podle p#edpokladu pe2 = pe!

2 , . . . , pen = pe!

n , pe1 = p1 a pe!

1 = p1,dostáváme

p1, pe2, . . . , p

en ) !.

ap1, p

e2, . . . , p

en ) !,

odkud podle V!ty 2.37 máme

pe2, . . . , p

en ) !.

20

Opakovan%m pou"itím práv! provedené úvahy postupn! dostaneme

pe3, . . . , p

en ) !

a" pope

n ) !

a nakonec) !.

Nech+ nyní T = {!1, . . . ,!n}. Podle sémantické verzi v!ty o dedukci dosta-neme z T |= !, "e |= !1 (· · · (!n !)). Odtud podle práv! dokázaného plyne) !1 (· · · (!n !)), odkud dostáváme pomocí v!ty o dedukci !1, . . . ,!n ) !,tj. po"adované T ) !. !

Pro d&kaz tzv. silné verze v!ty o úplnosti (ta se neomezuje na kone'né T )pot#ebujeme následující v!tu.

V$ta 2.41 (o kompaktnosti) (1) Mno$ina T formulí je splnitelná, práv& kdy$je splnitelná ka$dá kone(ná podmno$ina mno$iny T . (2) Pro ka$dou formuli !je T |= !, práv& kdy$ existuje kone(ná S . T tak, $e S |= !.

D̊ukaz. (nebude u zkou$ky po"adován) !

S pou"itím V!ty 2.41 snadno doká"eme následující v!tu.

V$ta 2.42 (o úplnosti, silná verze) Pro libovolnou mno$inu T formulí a for-muli ! platí, $e z T |= ! plyne T ) !.

D̊ukaz. Je-li T |= !, pak dle V!ty 2.41 (2) existuje kone'ná S . T tak, "eS |= !. Podle V!ty 2.40 je S ) !, a z toho samoz#ejm! plyne T ) !. !

Uv!domme si, "e V!ta o úplnosti je velmi netriviální tvrzení: Z toho, "en!jaká formule má p#i v$ech (intuitivn! zcela p#irozen! definovan%ch) mo"n%chohodnoceních pravdivostní hodnotu 1 plyne, "e je dokazatelná pomocí t#í (jedno-duch%ch a intuitivn! p#ijateln%ch) axiom& a jednoho (jednoduchého a intuitivn!p#ijatelného) odvozovacího pravidla. Pojem pravdivého tvrzení, tak jak je for-malizován v rámci v%rokové logiky, je tedy pln! syntakticky charakterizovateln%(a navíc velmi jednoduch%m z&sobem).Následující v!ta ukazuje dal$í vztah dvojice pojm&, jednoho sémantického

(splnitelnost) a druhého syntaktického (bezespornost), které spolu na první po-hled nesouvisí.

V$ta 2.43 Mno$ina T formulí je splnitelná, práv& kdy$ je bezesporná.

21

D̊ukaz. Nech+ je T splnitelná. Pak existuje ohodnocení e, ve kterém jsou prav-divé v$echny formule z T . Kdyby byla T sporná, pak by pro libovolnou formuli !bylo T ) ! a T ) !, a tedy dle korektnosti i T |= ! a T |= !. To znamená, "ep#i ka"dém ohodnocení, p#i kterém jsou pravdivé v$echny formule z T (jednímz nich je e), je pravdivá jak formule !, tak formule !. To je ale pochopiteln!nemo"né.Nech+ T je bezesporná. Pak existuje formule !, pro kterou neplatí T ) !,

tj. (podle úplnosti) neplatí T |= !. To ale znamená, "e existuje ohodnocení,ve kterém není pravdivá !, ale jsou pravdivé v$echny formule z T . Tedy T jesplnitelná. !

3 Predikátová logika

3.1 Syntax predikátové logiky

P#irozen% jazyk je základním prost#edkem, pomocí kterého formulujeme a za-znamenáváme své usuzování. Ji" základní rozbor v!t p#irozeného jazyka odhalín!které jeho v%znamné jednotky/sou'ásti. Pro nás to budou: prom!nné, rela'nísymboly (symboly pro ozna'ování relací), funk'ní symboly (symboly pro ozna-'ování funkcí) v'etn! symbol& pro ozna'ování konstant , symboly pro logickéspojky (jako “a”, “nebo”, “práv! kdy"” atd.), symboly pro kvantifikátory (nap#.“pro ka"d%”, “existuje”) a pomocné symboly.Ve v!tách “Ka"d% slon je savec”, “Pro ka"dé dva body existuje bod, kter%

mezi nimi nele"í”, “Petr je mlad$í ne" Pavel nebo v!k Ji#ího je v!t$í ne" sou'etv!k& Petra a Pavla”, “Sou'et druh%ch mocnin nenulov%ch 'ísel je v!t$í ne" nula”se mluví o jednomístn%m vztazích “b%t slonem”, “b%t savcem”, trojmístnémvztahu “nele"et mezi dv!ma body”, dvojmístném vztahu “b%t v!t$í”, o funkcip#i#azující 'lov!ku jeho v!k, o funkci s'ítání, o funkci mocn!ní, o (konstantních)objektech Petr, Pavel, Ji#í, nula, implicitn! se zde objevují prom!nné (nap#.první tvrzení, formulováno p#esn!ji, #íká “pro ka"dé x platí, "e je-li x slonem, jex savcem”), logické spojky (“nebo”) a kvantifikátory (“pro ka"dé”, “existuje”).

Definice 3.1 Jazyk J predikátové logiky obsahuje (a je tím ur'en)

• (p#edm$tové) prom$nné x, y, z, . . . , x1, x2, . . .; p#edpokládáme, "e jichje nekone'n! mnoho (spo'etn! mnoho, proto"e chceme mít jazyk spo-'etn%);

• rela%ní symboly p, q, r, . . . , r1, r2, . . ., ke ka"dému rela'nímu symbolu rje dáno nezáporné celé 'íslo '(r) naz%vané arita symbolu r; musí existovataspo( jeden rela'ní symbol;

• funk%ní symboly f, g, h, . . . , f1, f2, . . ., ke ka"dému funk'nímu symboluf je dáno nezáporné celé 'íslo '(f) naz%vané arita symbolu f ;

• symboly pro logické spojky (negace) a (implikace) a symbol / prouniverzální kvantifikátor;

22

• pomocné symboly — r&zné typy závorek.

Poznámka 3.2 (1) Místo p#edm!tové prom!nné 'asto #íkáme jen prom!nné.Mno"ina v$ech rela'ních (n!kdy se #íká predikátov%ch) symbol& jazyka J sezna'í R (pop#. RJ ); mno"ina v$ech funk'ních (n!kdy se #íká opera'ních) sym-bol& jazyka J se zna'í F (pop#. FJ ). Je-li r ! R a '(r) = n, pak #íkáme, "e rje n-ární; podobn! pro f ! F . Je-li f ! F 0-ární, naz%vá se f symbol konstanty(nebo+ funkce, která má 0 argument&, musí p#i#azovat v"dy stejnou hodnotu,tj. je konstantní; za#adit cvi'ení na vysv!tlení).(2) Je z#ejmé, "e jazyk je jednozna'n! ur'en sv%mi rela'ními symboly, funk'-

ními symboly a jejich aritami (v$e ostatní mají v$echny jazyky stejné). Trojici"R, J,'# proto naz%váme typ jazyka.(3) Je-li mezi rela'ními symboly symbol 0, naz%váme ho symbol pro rovnost

a cel% jazyk pak jazyk s rovností. Symbol pro rovnost a rovnost má specificképostavení, jak uvidíme dále.

Základní syntaktické jednotky vybudované ze symbol& jazyka jsou termy aformule. Termy jsou v%razy reprezentující funkci aplikovanou na své operandy;formule reprezentují tvrzení o prvcích univerza.

Definice 3.3 Term jazyka typu "R, F,'# je induktivn! definován takto:

(i) ka"dá prom!nná x je term;

(ii) je-li f ! F n-ární a jsou-li t1, . . . , tn termy, pak f(t1, . . . , tn) je term.

Poznámka 3.4 (1) Termy jsou tedy jisté kone'né posloupnosti prvk& danéhojazyka.(2) Je-li f ! F binární, pou"íváme také tzv. infixovou notaci a pí$eme xfy

nebo (xfy) místo f(x, y) (nap#. 2 + 3 místo +(2, 3)); ve slo"en%ch termechpou"íváme závorky (nap#. (2 + 3) · 5).

Definice 3.5 Formule jazyka typu "R, F,'# je induktivn! definována takto:

(i) je-li r ! R n-ární a t1, . . . , tn jsou termy, pak r(t1, . . . , tn) je formule;

(ii) jsou-li ! a " formule, pak !, (! ") jsou také formule;

(iii) je-li ! formule a x prom!nná, pak (/x)! je formule.

Poznámka 3.6 (1) Formule vytvo#ené dle (i) se naz%vají atomické . Je-li r ! Rbinární, pí$eme také t1rt2 nebo (t1rt2) místo r(t1, t2) (tedy nap#. x ( y místo( (x, y)). Obzvlá$t! pí$eme t1 0 t2 místo 0 (t1, t2).(2) Budeme pou"ívat obvyklé konvence, zjednodu$ující 'itelnost formulí: vy-

nechávání závorek, pí$eme . . . (/x, y) . . . místo . . . (/x)(/y) . . . atd.).(3) Podobn! jako ve v%rokové logice, symboly pro ostatní logické spojky ne-

pat#í do jazyka predikátové logiky. Podobn! symbol 1 (existen'ní kvantifikátor)

23

nepat#í do jazyka predikátové logiky. Abychom tyto symboly m!li k dispozici,chápeme

posloupnost ! " jako zkratku za (! "), (4)

posloupnost ! " jako zkratku za ! ", (5)

posloupnost ! " jako zkratku za (! ") (" !), (6)

posloupnost (1x)! jako zkratku za (/x) !. (7)

Posloupnosti obsahující symboly , , a 1 tedy nejsou formulemi, mohou tob%t zkratky za formule (p#íklad. . .). Pro jednoduchost v$ak v!domi si toho, "ea jak%m zp&sobem se dopou$tíme nep#esnosti, budeme t!mto posloupnostem'asto také #íkat formule.

Podobn! jako ve v%rokové logice m&"eme i v predikátové logice provád!td&kazy strukturální indukcí.

V$ta 3.7 (d&kaz strukturální indukcí pro termy) Nech# V je vlastnost term".Nech# platí, $e

• ka$dá prom&nná má vlastnost V;

• mají-li termy t1, . . . , tn vlastnost V a je-li f ! F n-ární, pak vlastnost Vmá i term f(t1, . . . , tn).

Pak vlastnost V má ka$d! term.

V$ta 3.8 (d&kaz strukturální indukcí pro formule) Nech# V je vlastnostformulí. Nech# platí, $e

• ka$dá atomická formule má vlastnost V;

• mají-li formule ! a " vlastnost V, pak vlastnost V mají i formule ! a(! ");

• má-li formule ! V, má vlastnost V formule (/)!.

Pak vlastnost V má ka$dá formule.

P#íklad 3.9 (1) Uva"ujme jazyk J typu "R, F,'#, kde R = {p, d, b, s}, F = &,rela'ní symboly p, d, b jsou unární, s binární. Je to jazyk bez funk'ních sym-bol&, a tedy jedin%mi termy jsou prom!nné. Atomick%mi formulemi jsou p(x),p(y), d(y), b(x), atd. Dal$ími formulemi (ne atomick%mi) jsou nap#. v%razyp(x) p(x), p(x) p(x), (/x)(p(x) d(x) b(x)), (1x)b(x) p(x),(/x)(/y)(b(x) (s(x, y) b(y))).V%razy ((x , p(x, x), p(d(x)), (/x)(s(x, y) p(x)), formulemi nejsou.(2) Uva"ujme jazyk J typu "R, F,'#, kde R = {p,(}, F = {c, 2}, c je nulární

(tj. symbol konstanty), p je unární, ( a 2 jsou binární. Pak v%razy c, x, c 2 c,c2(x2y), atd. jsou termy. V%razy cc, c2p(x), p(x), c22x, termy nejsou. Formulemijsou nap#. c ( x, p(x) (c ( x), (/x)(x ( x 2 x), (/x)(/y)(x 2 y ( y 2 x).

24

Poznámka 3.10 Jazyk predikátové logiky obsahuje symboly r&zn%ch typ& (re-la'ní symboly, funk'ní symboly, symboly spojek). Z nich se dají vytvá#et termya formule, které jsou v ur'itém smyslu “rozumn%mi” #et!zci. Rozumné proto,"e dáme-li rela'ním a funk'ním symbol&m smysl, dají se “rozumn!” 'íst (po-znamenejme, "e p#esn% smysl dostanou rela'ní a funk'ní symboly, a také termya formule, a" vybudujeme sémantiku). Tak nap#íklad, uva"ujme jazyk z P#í-kladu 3.9 (1). Nech+ p, d, b, m ozna'ují po #ad! “mít dostate'n% p#íjem”, “mítvelké dluhy”, “b%t bonitní”, “b%t man"elé”, tj. p(x) znamená “objekt ozna'en%x má dostate'n% p#íjem” atd. Formule (/x)(p(x) d(x) b(x)) pak “#íká”:“pro ka"dé x platí, "e má-li x dostate'n% p#íjem a nemá-li velké dluhy, pak je xbonitní”. Formule (/x)(/y)(b(x) (m(x, y) b(y))) “#íká”: “pro ka"dé x a yplatí, "e je-li x bonitní a jsou-li x a y man"elé, je i y bonitní”.

M&"eme také postupovat obrácen! (to je dobré cvi'ení): K dané v!t! p#i-rozeného jazyka navrhneme jazyk predikátové logiky a napí$eme formuli, kteráodpovídá danému tvrzení (viz cvi'ení).Termy a formule jsou definovány induktivn!. Ka"d% term pou"it% p#i kon-

strukci termu t se naz%vá podterm termu t; ka"dá formule pou"itá v konstrukciformule ! se naz%vá podformule formule !. P#esn!ji: Mno"ina sub(t) v$echpodterm& termu t je definována následovn!: pro prom!nnou x je sub(x) = {x};sub(f(t1, . . . , tn)) = {f(t1, . . . , tn)} ' sub(t1) ' · · · ' sub(tn). Mno"ina sub(!)v$ech podformulí formule ! je definována následovn!: je-li ! atomická, paksub(!) = {!}; sub( !) = { !}' sub(!) a sub(! ") = {! "}' sub(!)'sub("); sub((/x)!) = {(/x)!} ' sub(!).

.íkáme, "e prom!nná se vyskytuje v termu nebo ve formuli, jestli"e je n!-kter%m symbolem termu nebo formule jako"to #et!zce symbol& s tou v%jimkou,"e v%skyty za / se nepo'ítají (tj. prom!nná x nemá v%skyt ve formuli (/x)r(y, z).Mno"inu v$ech prom!nn%ch, které se vyskytují v termu t ozna'ujeme var(t);mno"inu v$ech prom!nn%ch, které se vyskytují ve formuli ! ozna'ujeme var(!).Je-li t term, pí$eme t(x1, . . . , xn), abychom zd&raznili, "e v$echny prom!nné,

které se v t vyskytují, se nacházejí mezi x1, . . . , xn.Prom!nné z var(!) mohou mít ve formuli ! v%skyt dvojího druhu — voln%

a vázan%. Mno"ina free(!) prom!nn%ch, které mají ve ! voln! v!skyt je de-finována následovn!: je-li ! atomická, pak free(!) = var(!); dále free( !) =free(!), free(! ") = free(!) ' free("); a free((/x)!) = free(!) 3 {x}. Mno-"ina bound(!) prom!nn%ch, které mají ve ! vázan! v!skyt je definovánanásledovn!: je-li ! atomická, pak bound(!) = &; dále bound( !) = bound(!),bound(! ") = bound(!) ' bound("); a bound((/x)!) = bound(!) ' {x}.Pí$eme !(x1, . . . , xn), abychom zd&raznili, "e v$echny prom!nné, které mají

ve ! voln% v%skyt, se nacházejí mezi x1, . . . , xn, tj. free(!) . {x1, . . . , xn}.

Poznámka 3.11 Chceme-li napsat formuli nebo term, musíme nejd#íve po-psat jazyk, jeho" formuli nebo term chceme napsat. To je v$ak 'asto pracnéa zbyte'né. Proto zavedeme pojem indukovaného jazyka. Jazyk indukovan!mno"inami F a T #et!zc& je nejmen$í jazyk J typu "R, F,'#, v n!m" #et!zce zF formulemi a #et!zce z T termy (tj. je-li J " jin% takov% jazyk typu "R", F ",'"#,

25

pak R . R", F . F "). Nap#íklad jazykem ur'en%m mno"inami F = ... a T = ...je . . . . Místo jazyk indukovan% mno"inami F a T #et!zc& také #íkáme jazykur'en% formulemi z F a termy z T .

P#íklad 3.12 (Viz p#edná$ky a cvi'ení) Uva"ujme jazyk ur'en% termy t1 =x1 + ((c + x1) + x2), t2 = (c + c) + c and formulemi !1 = (/x)(/y)((big(x)(x ( y)) big(y)), !2 = (c ( x) (/x)(1y)(x + x ( x + y). Pak var(!1) ={x, y}, var(!2) = {x, y}, free(!1) = &, bound(!1) = {x, y}, free(!2) = {x},bound(!2) = {x, y} (prom!nná x má voln% i vázan% v%skyt v !2).

U"ite'n%m pojmem je pojem substituce termu za prom!nnou.

Definice 3.13 Nech+ t a s jsou termy, x prom!nná. V!sledek substitucetermu s za x v t je term t(x/s) definovan% následovn!:

(i) je-li t prom!nná, pak

t(x/s) =!

s pro t = xt pro t -= x;

(ii) pro t = f(t1, . . . , tn), kde f ! F je n-ární a t1, . . . , tn jsou termy, je t(x/s) =f(t1(x/s), . . . , tn(x/s)).

Definice 3.14 Pro formuli !, term s, a prom!nnou x, je v!sledkem substi-tuce s za x ve ! formule !(x/s) definovaná následovn!:

(i) pro ! = r(t1, . . . , tn) je !(x/s) = r(t1(x/s), . . . , tn(x/s));

(ii) ( !)(x/s) = (!(x/s)), (! ")(x/s) = !(x/s) "(x/s);

(iii) ((/y)!)(x/s) = (/y)! pro y = x, ((/y)!)(x/s) = (/y)(!(x/s)) pro y -= x.

P#íklad 3.15 K procvi'ení doka"te strukturální indukcí, "e jsou-li t, s termy,! formule a x prom!nná, je t(x/s) term a !(x/s) je formule.

P#edchozí definice lze snadno roz$í#it na definice substituce termu za term.Substituce termu za prom!nnou m&"e vést k necht!n%m situacím. Uva"ujme

nap#. formuli ! = (/y)(y ( x) která vyjad#uje, "e x je v!t$í ne" jakékoliv y.Substituce y+ y za x vede k !(x/y+ y) = (/y)(y ( y+ y), co" je jist! formule,která vyjad#uje n!co jiného. Abychom zabránili takov%m p#ípad&m, definujemetzv. korektní substituce.

Definice 3.16 Substituce termu t za prom!nnou x ve formuli ! je korektní (tse naz%vá substituovateln! za x v t), jestli"e pro ka"dou y ! var(t) platí, "e"ádná podformule formule !, která je tvaru (/y)", neobsahuje v%skyt x, kter%je voln%m v%skytem x ve !.

P#íklad 3.17 (Viz p#edná$ky a cvi'ení)

26

P"evod v#t p"irozeného jazyka na formule predikátové lo-giky

P#íklad 3.18 Navrhn!te formuli predikátové logiky, která vyjad#uje v!tu “/ádn%plaz s v%jimkou zmije není nebezpe'n%”. .e$ení: V!tu p#eformulujeme do po-doby bli"$í predikátové logice: “Pro ka"dé x platí: jestli"e x je plaz a x není zmije,pak není pravda, "e x je nebezpe'n%”. Nyní navrhneme vhodn% jazyk: unární re-la'ní symboly p, z, n. Vhodnou formulí je nap#. (/x)((p(x) z(x)) n(x)).Pozor: není to jednozna'n% proces (více mo"n%ch návrh& jazyka, více mo"-

n%ch formulí p#i daném návrhu).

3.2 Sémantika predikátové logiky

Jazyk predikátové logiky obsahuje rela'ní, funk'ní (a dal$í) symboly. Ze t!chtosymbol& se skládají termy a formule. Samotné termy a formule nemají "ádn%v%znam, tj. term sám o sob! nemá "ádnou hodnotu, formule sama o sob! nemá"ádnou pravdivostní hodnotu. To je dob#e patrné nap#. u termu x + 0: je doo'í bijící, "e k tomu, aby tento term m!l hodnotu, musí mít n!jakou hodnotuprom!nná x (a dále, musíme interpretovat + a 0, viz následující term 0 + 0).H&#e je to patrné nap#. u termu 0 + 0. *lov!k má nutkání #íci, "e hodnotoutohoto termu je 0. To je ov$em hrubá chyba! Term 0 + 0 je posloupností t#ísymbol&, nic víc; 0 je symbol konstanty (tj. 0-ární funk'ní symbol), + je bi-nární funk'ní symbol (p#ísn! vzato, 0 + 0 je p#ehledn!j$ím zp&sobem zapsan%term +(0, 0), to ale na celé v!ci nic nem!ní). Ne" #ekneme, jak% prvek symbol 0ozna'uje a jakou binární funkci ozna'uje symbol + nemá smysl (nelze!) se ptát,jakou hodnotu má term 0 + 0. Je na$ím zám!rem, aby symboly mohly mít li-bovolnou (smysluplnou) interpretaci. Tím myslíme zhruba následující: Zvolímevhodné univerzum M , tj. mno"inu prvk&, které jsou pro na$e úvahy relevantní(n!kdy se #íká univerzum diskurzu, tj. univerzum rozpravy). V tomto univerzup#i#adíme v%znamy rela'ním a funk'ním symbol&m daného jazyka J prediká-tové logiky, tj. pro ka"d% rela'ní symbol jazyka ur'íme konkrétní relaci v M ,kterou tento rela'ní symbol bude ozna'ovat, a pro ka"d% funk'ní symbol jazykaur'íme konkrétní funkci v M , kterou tento funk'ní symbol bude ozna'ovat. Ta-kovou volbou univerza, relací a funkcí provedeme tzv. interpretaci jazyka (jetedy jasné, "e jeden jazyk má mnoho mo"n%ch interpretací); univerzum spolus relacemi a funkcemi tvo#í tzv. strukturu pro dan% jazyk predikátové logiky(viz dále). Zvolíme-li interpretaci jazyka, zb%vá v termech a formulích je$t!jeden typ symbol&, které dosud nejsou interpretovány—prom!nné. Interpretaciprom!nn%ch zprost#edkovává tzv. ohodnocení, které ka"dé prom!nné jazyka p#i-#adí n!jak% prvek univerza (je op!t jasné, "e p#i dané interpretaci jazyka exis-tuje celá #ada mo"n%ch interpretací prom!nn%ch). Zvolíme-li interpretaci jazyka(tzv. strukturu pro dan% jazyk) a interpretaci prom!nn%ch (tzv. ohodnoceníprom!nn%ch pro dan% jazyk v dané struktu#e), m&"eme se ptát po hodnotáchterm& (hodnotou termu je prvek univerza) a formulí (hodnotou formule je prav-divostní hodnota, tj. 0 nebo 1). Shr(me tedy a zd&razn!me: Termy i formulejsou pouhé #et!zce symbol& bez jakéhokoli v%znamu. Pojmy “hodnota termu”

27

a “(pravdivostní) hodnota formule” nejsou smysluplné, smysluplné jsou pojmy“hodnota termu p#i dané interpretaci jazyka a dané interpretaci prom!nn%ch” a“(pravdivostní) hodnota formule p#i dané interpretaci jazyka a dané interpretaciprom!nn%ch” (neboli “hodnota termu v dané struktu#e p#i daném ohodnocení”a “(pravdivostní) hodnota formule v dané struktu#e p#i daném ohodnocení”).Vra+me se k na$emu p#íkladu, tj. k term&m 0 + 0 a 0 + x. Jsou to termy v

jistém jazyce J (o kterém jsme zatím nemluvili). Jazykem J m&"e b%t nap#.jazyk, kde R = {(}, F = {0,+} a ( je binární, 0 je nulární (tj. symbol kon-stanty) a + je binární. Zvolme jednu interpretaci jazyka J : univerzem M nech+je mno"ina Z v$ech cel%ch 'ísel, binární relací v Z, kterou ozna'uje binární re-la'ní symbol ( nech+ je obvyklá relace “men$í nebo rovno” (ozna'me ji (M),konstantou (tj. nulární funkcí) v Z, kterou ozna'uje nulární funk'ní symbol 0nech+ je 'íslo nula (ozna'me ho 0M), binární funkcí v Z, kterou ozna'uje binárnífunk'ní symbol + nech+ je obvyklé s'ítání (ozna'me ho +M). Zvolme dále in-terpretaci prom!nn%ch: nech+ prom!nn%m x a y jsou po #ad! p#i#azeny hodnotyp!t a minus sto (a dal$ím prom!nn%m hodnoty libovolné). P#i takové interpre-taci je hodnotou termu 0 + 0 'íslo nula (0M +M 0M), hodnotou termu x + 0je 'íslo p!t. Formule 0 ( x je p#i dané interpretaci pravdivá (nebo+ 'íslo, kteréje ozna'eno symbolem 0, tj. 'íslo nula, je v relaci ozna'ené symbolem (, tj. vrelaci “men$í nebo rovno”, s 'íslem ozna'en%m symbolem x, tj. s 'íslem p!t). Zpodobného d&vodu (zatím ov$em zd&vod(ujeme pouze intuitivn!) je pravdiváformule (0 ( x) (y ( y + x); ta je dokonce pravdivá p#i jakékoli interpre-taci prom!nn%ch. Zm!níme-li interpretaci prom!nn%ch tak, "e prom!nné x budep#i#azeno 'íslo minus deset, bude formule 0 ( x nepravdivá.Uvedená interpretace jazyka v$ak není jediná mo"ná. Jinou interpretaci do-

staneme, zm!níme-li na$i p&vodní interpretaci tak, "e symbol 0 bude ozna'ovat'íslo jedna. P#i této interpretaci bude hodnotou termu 0 + 0 'íslo dv!. Zcelajinou interpretaci dostaneme, zvolíme-li za univerzum mno"inu v$ech 'tverco-v%ch reáln%ch matic, a ozna'ují-li symboly (, 0,+ po #ad! relaci rovnosti matic,matici skládající se ze sam%ch nul, a operaci násobení matic.

Definice 3.19 Nech+ J je jazyk typu "R, F,'#. Struktura pro J je trojiceM = "M, RM, FM#, která sestává z neprázdné mno"iny M , mno"iny RM ={rM ! LMn | r ! R, '(r) = n} relací a mno"iny FM = {fM : Mn % M | f !F, '(r) = n} funkcí. Jde-li o jazyk s rovností (tj. R obsahuje 0), po"adujeme,aby 0M byla ekvivalence na M .

Je-li M struktura pro jazyk J s rovností 0 a je-li 0M (relace odpovídající0) identita na M (tj. nejen ekvivalence), naz%vá se M strukturou se striktnírovností. Nebude-li uvedeno jinak, budeme pro jazyk s rovností uva"ovat jenstruktury se striktní rovností.

Poznámka 3.20 (1) Jin%mi slovy, struktura M pro jazyk J typu "R, F,'# jesystém relací a funkcí na jisté mno"in! M ; ke ka"dému n-árnímu rela'nímusymbolu r ! R je ve struktu#e odpovídající n-ární relace rM v M , ke ka"démun-árnímu funk'nímu symbolu f ! F je ve struktu#e odpovídající n-ární funkcefM v M .

28

(2) Nehrozí-li nebezpe'í nedorozum!ní, vynecháváme n!kdy pro jednodu-chost horní indexy a místo rM a fM pí$eme jen r a f .

P#íklad 3.21 (1) Uva"ujme jazyk J z P#íkladu 3.9 (1). Nech+ M je mno"inav$ech lidí z daného regionu (nap#. z *eské republiky). Definujme relace pM,dM, bM, sM následovn!: pM, dM, bM jsou unární relace, tj. podmno"iny M ,definované

pM = {m ! M | m má 'ist% p#íjem vy$$í ne" 17 tis. K'/m!s.},dM = {m ! M | m splácí pravideln! mén! ne" 5 tis. K'/m!s.},bM = {m ! M | m na "ivobytí zb%vá více ne" 8 tis. K'/m!s.}

a sM je binární relace

sM = {"m1, m2# ! M , M | m1 a m2 jsou man"elé.}

Pak pro RM = {pM, dM, bM, sM}, FM = & je M = "M, RM, FM# strukturoupro jazyk J .(2) Jinou strukturu pro stejn% jazyk dostaneme, pozm!níme-li strukturu

uvedenou v (1) tak, "e

pM = {m ! M | m má 'ist% p#íjem vy$$í ne" 40 tis. K'/m!s.},dM = {m ! M | m splácí pravideln! mén! ne" 2 tis. K'/m!s.},bM = {m ! M | m na "ivobytí zb%vá více ne" 35 tis. K'/m!s.}

a sM je binární relace

sM = {"m1, m2# ! M , M | m1 a m2 nejsou man"elé.}

(3) Dal$í strukturu pro stejn% jazyk dostaneme, zvolíme-li M = {a, b, 1, 2},pM = {a, b}, dM = {1, 2}, bM = &, sM = {"a, b#, "1, 2#}.(4) Uva"ujme jazyk J z P#íkladu 3.9 (2). Nech+M = {0, 1,31, 2,32, 3,33, . . .}

je mno"ina v$ech p#irozen%ch 'ísel. Definujme relace pM (unární, tj. podmno"inaM), (M (binární) a funkce cM (nulární, tj. vlastn! prvek z M) a 2M (binární)následovn!:

pM = {m ! M | mje v!t$í nebo rovno nule},(M = {"m1, m2# | m1 je men$í nebo rovno m2},cM = 0 (tj. cM je 'íslo nula),

m1 2M m2 = m1 +m2 (tj. 2M je operace s'ítání).

(5) Jinou strukturu pro jazyk J z P#íkladu 3.9 (2) dostaneme, kdy" zm!nímev%$e uvedenou strukturu tak, "e cM = 0, pop#. je$t! definujeme m1 2M m2 =m1 · m2 (násobení).(6) Dal$í strukturou pro jazyk J z P#íkladu 3.9 (2) je struktura s nosi'em

M = {A | A je 'tvercová matice #ádu 10},

29

kde

pM = {A ! M | A je regulární matice},(M = {"A, B# | aij je nejv%$e rovno bij pro v$echna 1 ( i, j ( n},cM = I (tj. cM jednotková matice),

m1 2Mm2 = m1 +m2 (tj. 2M je operace s'ítání matic).

(6) Dal$í strukturou pro jazyk J z P#íkladu 3.9 (2) je struktura s nosi'emM = {a, b}, pM = {a, b}, (M= {"a, a#, "b, b#, "b, a#}, cM = b a operace 2M jedána tabulkou

2M a ba a bb a a

.

Jak tedy vidíme, k danému jazyku predikátové logiky existuje nekone'n!mnoho struktur (variabilita je dána následujícím: nosi' M m&"e mít libovoln%po'et prvk&, ka"d% rela'ní symbol r m&"e b%t interpretován libovolnou relacírM p#íslu$né arity, ka"d% funk'ní symbol f m&"e b%t interpretován libovolnoufunkcí fM p#íslu$né arity).Nech+ M je struktura pro jazyk J . M-ohodnocení p#edm$tov!ch pro-

m$nn!ch (krátce jenM-ohodnocení, pop#. jen ohodnocení) je zobrazení v p#i-#azující ka"dé prom!nné x prvek v(x) ! M . Jsou-li v a v" ohodnocení a xprom!nná, pí$eme v =x v" pokud pro ka"dou prom!nnou y -= x je v(y) = v"(y),tj. v a v" se li$í nejv%$e v tom, jakou hodnotu p#i#azují prom!nné x.

Definice 3.22 Nech+ v je M-ohodnocení. Hodnota $t$M,v termu t p#i vje definována následovn!:

(i) pro prom!nnou x, $x$M,v = v(x);

(ii) pro t = f(t1, . . . , tn), $t$M,v = fM($t1$M,v, . . . , $tn$M,v).

Poznámka 3.23 Uv!domme si, "e podle Definice 3.22 je p#i dan%ch M a vka"dému termu p#i#azena práv! jedna hodnota $t$M,v. To lze nahlédnout po-u"itím V!ty 3.7, vezmeme-li za V vlastnost “hodnota $t$M,v je jednozna'n!definována”.

Lemma 3.24 Hodnota $t$M,v nezávisí na hodnotách p'i'azen!ch ohodnoce-ním v prom&nn!m, které se v t nevyskytují, t.j. pro ka$dá M-ohodnocení v1, v2spl)ující v1(x) = v2(x) pro ka$dé x ! var(t) je $t$M,v1 = $t$M,v2.

D̊ukaz. Strukturální indukcí. !

Poznámka 3.25 (jen na okraj) Podle Definice 3.22 a Lemma 3.24 indukujeka"d% term t(x1, . . . , xn) tzv. termovou funkci tM: pro m1, . . .mn ! M je

tM(m1, . . . , mn) = $t$M,v,

kde v je M-ohodnocení, pro které v(x1) = m1, . . . , v(xn) = mn.

30

P#íklad 3.26 term, $t$M,v, termova funkce

Definice 3.27 Pravdivostní hodnota $!$M,v formule ! p#iM-ohodnocenív je definována následovn!:

(i) pro atomické formule:

$r(t1, . . . , tn)$M,v =!1 pokud "$t1$M,v, . . . , $tn$M,v# ! rM,0 pokud "$t1$M,v, . . . , $tn$M,v# -! rM.

(ii) pro formule ! a " je

$ !$M,v =!1 pokud $!$M,v = 0,0 pokud $!$M,v = 1.

$! "$M,v =!1 pokud $!$M,v = 0 nebo $"$M,v = 1,0 jinak.

(iii) pro formuli ! a prom!nnou x je

$(/x)!$M,v =!1 pokud pro ka"dé v" takové, "e v" =x v, je $!$M,v! = 1,0 jinak.

Je-li $!$M,v = 1 ($!$M,v = 0), #íkáme, "e formule ! je pravdivá (neprav-divá) ve struktu#e M p#i ohodnocení v. Uv!domte si, "e #íct “formule ! jepravdivá” nemá smysl; musíme #íci, v jaké struktu#e a p#i jakém ohodnocení!/e b!"n! #íkáme nap#. “(formule) (/x, y)x ( x + y je pravdivá”, je zp&sobenotím, "e implicitn! n!jakou strukturu p#edpokládáme, v!t$inou 'íselnou (nap#.celá 'ísla s b!"n%mi relacemi a operacemi).

Poznámka 3.28 Tedy: $r(t1, . . . , tn)$M,v = 1, práv! kdy" n-tice "$t1$M,v, . . . , $tn$M,v#prvk& $ti$M,v z M pat#í do rM. Dále, v%znam spojek negace a implikace jestejn% jako ve v%rokové logice. K v%znamu /: Za prvé, definice #íká, "e (/x)! jeve struktu#eM p#i v pravdivá, práv! kdy" je ve struktu#eM pravdivá formule !p#i ka"dém ohodnocení v", které v$em prom!nn%m r&zn%m od x p#i#azuje stejnéprvky jaké jim p#i#azuje v. To je práv! zam%$len% v%znam kvantifikátoru /. Zadruhé, snadno se vidí, "e

$(/x)!$M,v = min{$!$M,v! | v" =x v}.

(2) Snadno se p#esv!d'íme, "e

$! "$M,v = $!$M,v 4 $"$M,v,

$! "$M,v = $!$M,v 5 $"$M,v,

$! "$M,v = $!$M,v 6 $"$M,v,

31

dále pak (ov!#te!)

$(1x)!$M,v = max{$!$M,v! | v" =x v}.

Poznámka 3.29 Stejn! jako u ohodnocení term& si uv!domme, "e podle De-finice 3.27 je p#i dan%ch M a v ka"dé formuli p#i#azena práv! jedna hodnota$!$M,v. To lze nahlédnout pou"itím V!ty 3.8, vezmeme-li za V vlastnost “hod-nota $!$M,v je jednozna'n! definována”.

Lemma 3.30 Hodnota $!$M,v nezávisí na hodnotách p'i'azen!ch ohodnoce-ním v prom&nn!m, které se ve ! nevyskytují, t.j. pro ka$dáM-ohodnocení v1, v2spl)ující v1(x) = v2(x) pro ka$dé x ! var(!) je $!$M,v1 = $!$M,v2.

D̊ukaz. Strukturální indukcí. !

P#íklad 3.31 Consider the L-structure L-structure M from Example ?? (1).Let v be an M-valuation such that v(x) = 2, v(y) = 10, v(z) = 110. Then forterms t1 = (x + y) + x and t2 = c + x we have $t1$M,v = 14, $t2$M,v = 3;for formulas !1 = (x ( y), !2 = (y ( x), !3 = big(x), !4 = big(z), !5 =(/x)(/y)((big(x) (x ( y)) big(y)), !6 = (/x)(big(x + c) big(x)) wehave $!1$M,v = 1, $!2$M,v = 0, $!3$M,v = 0, $!4$M,v = 0.1, $!5$M,v = 1,$!6$M,v = 0.99. Note that the truth values of !5 and !6 do not depend on v(Lemma 3.30).

Podle Definice 3.27 a Lemma 3.30 indukuje ka"dá formule !(x1, . . . , xn) (tj.formule s voln%mi prom!nn%mi mezi x1, . . . , xn) n-ární relaci !M v M : prom1, . . .mn ! M je

"m1, . . . , mn# ! !M práv! kdy" $!$M,v = 1, (8)

kde v je M-ohodnocení, pro které v(x1) = m1, . . . , v(xn) = mn.

P#íklad 3.32 formule, $!$M,v, indukovana relace

Definice 3.33 Formule ! se naz%vá tautologie ve struktu#e (pravdivá vestruktu#e)M, jestli"e $!$M,v = 1 pro ka"déM-ohodnocení v. Formule ! se na-z%vá tautologie M (v"dy pravdivá), jestli"e je to tautologie v ka"dé struktu#eM.

! je tedy tautologie, jestli"e pro libovolnou strukturu M a libovolné ohod-nocení v je $!$M,v = 1.

Definice 3.34 Teorie v jazyce J predikátové logiky je libovolná mno"ina Tformulí tohoto jazyka. Struktura M jazyka J se naz%vá model teorie T(pí$emeM |= T , pop#. $T $M = 1 ), jestli"e ka"dá formule z T je pravdivá vM.

32

Poznámka 3.35 Pojem teorie je zcela p#irozen%. B!"n! se #íká “S tvojí teoriínesouhlasím” apod. P#itom teorií rozumíme soubor tvrzení, které daná osobazastává. Soubor tvrzení v predikátové logice p#edstavuje mno"ina formulí.

P#íklad 3.36 Uva"ujme jazyk J typu "R, F,'#, kde R = {r}, F = & a '(r) =2. Struktury pro J jsou M = "M, {rM}, &#, kde rM je binární relace na M (tj.struktury jsou vlastn! binární relace na M). Struktura M je modelem teorieT = {(/x)r(x, x), (/x, y)(r(x, y) r(y, x))}, práv! kdy" je relace rM reflexivnía symetrická.

Definice 3.37 Mno"ina S formulí sémanticky plyne z mno"iny T formulí(pí$eme T |= S; pí$eme také T |= !, jestli"e S = {!}, podobn! kdy" T = {!}),jestli"e ka"d% model T je modelem S.

Tedy T |= S, práv! kdy" v ka"dé struktu#e, ve které jsou pravdivé v$echnyformule z T , jsou také pravdivé v$echny formule z S.

P#íklad 3.38 Formule

" = (/x, y, z, w)((r(x, y) r(y, z) r(z, w)) r(x, w))

sémanticky plyne z formule

! = (/x, y, z)((r(x, y) r(y, z)) r(x, z)),

tj. ! |= ". Obrácené vypl%vání, tj. " |= !, neplatí. Viz p#edná$ka.

3.3 Axiomatick! systém predikátové logiky

Axiomy jsou formule následujících tvar&: formule tvaru (1)–(3) a dále

(/x)! !(x/t) (9)

je-li t substituovateln% za x

(/x)(! ") (! (/x)") (10)

nemá-li x ve ! voln% v%skyt.

(9) se naz%vá axiom substituce, (10) se naz%vá axiom distribuce.V p#ípad! logiky s rovností máme je$t! axiomy rovnosti :

x 0 x (11)

x 0 y y 0 x (12)

x 0 y y 0 z x 0 z (13)

x1 0 y1 · · · xn 0 yn f(x1, . . . , xn) 0 f(y1,0, yn) (14)

pro ka"d% n-ární f ! F

x1 0 y1 · · · xn 0 yn r(x1, . . . , xn) r(y1,0, yn) (15)

pro ka"d% n-ární r ! R.

33

Odvozovací pravidla jsou modus ponens (viz v%$e) a pravidlo generalizace(G, zobecn!ní), které #íká

z ! odvo) (/x)!.

Poznámka 3.39 V$imn!me si, "e v$echny axiomy jsou tautologie (snadno sevidí, ale pozd!ji p#esto dokázat). Dále si v$imn!me, "e omezení u axiom& (9) a(10) jsou podstatná (tj. bez nich by se nejednalo o tautologie). Skute'n!, je-li !formule (/y)r(x, y), t prom!nná y, pak (10) je formule (/) (/y)r(x, y)(/y)r(y, y), která není tautologií (nap#. není spln!na v "ádné struktu#e M saspo( dv!ma prvky, ve které rM je reflexivní relace). Dále, jsou-li ob! ! i "formulí r(x), je (10) formulí (/x)(r(x) r(x)) (r(x) (/x)r(x)), co" nenítautologie (nap#. není spln!na ve struktu#eM s aspo( dv!ma prvky, ve které jerM jednoprvková mno"ina).

Definice 3.40 D"kaz formule ! z mno"iny T formulí je libovolná posloupnost!1, . . . ,!n, pro kterou platí, "e !n = ! a ka"dá !i

• je axiomem

• nebo je formulí z T

• nebo plyne z p#edchozích formulí d&kazu pomocí odvozovacího pravidlaMP (tj. existují j, k < i (1 ( j ( n, 1 ( k ( n) tak "e !k je formule!j !i) nebo odvozovacího pravidla G (tj. existuje j < i tak, "e !i jeformulí (/x)!j).

Formule se naz%vá dokazatelná z T , existuje-li d&kaz této formule z T (za-pisujeme T ) !, pop#. jen ) !, je-li T prázdná mno"ina).

Poznámka 3.41 Stejn! jako ve v%rokové logice máme dva pojmy vypl%váníformule z mno"iny formulí: sémantické vypl%vání (T |= !) a syntaktické vypl%-vání (T ) !). Máme také dva pojmy platnosti formule: |= ! ozna'uje platnost! v sémantickém smyslu (pravdivost), ) ! ozna'uje platnost ! v syntaktickémsmyslu (dokazatelnost).

Formule se naz%vá v!rokov& dokazatelná z T , existuje-li její d&kaz z T , vekterém se vyskutují pouze axiomy typ& (1)–(3) a odvozovací pravidlo MP. Tse naz%vá v!rokov& sporná, jestli"e ka"dá formule je z T v%rokov! dokazatelná.Formule ! a " se naz%vají dokazateln! ekvivalentní z T , je-li T ) ! ".

Lemma 3.42 Nahradíme-li v tautologii v!rokové logiky v!rokové symboly li-bovoln!mi formulemi predikátové logiky, dostaneme formuli predikátové logiky,která je v!rokov& dokazatelná.

D̊ukaz. (podrobn!ji p#edná$ky) Je-li ! ona tautologie, pak dle v!ty o úplnostipro v%rokovou logiku je dokazatelná. Nahradíme-li v jejím d&kazu ve v%rokovélogice v%rokové symboly zmín!n%mi formulemi predikátové logiky, dostanemed&kaz v predikátové logice, prokazující, "e v%sledná formule je v%rokov! doka-zatelná. !

34

P#íklad 3.43 Proto"e p p a p ( p q) jsou tautologie v%rokové logikyjsou formule (/x)x ( y (/x)x ( y a y ( x + y ( y ( x + y x 0 0)(v%rokov!) dokazatelné formule predikátové logiky.

V$ta 3.44 (o dedukci) Pro formuli ! bez voln!ch prom&nn!ch a mno$inu Tformulí platí

T,! ) " práv& kdy$ T ) ! ".

D̊ukaz. Analogicky jako pro v%rokovou logiku, viz p#edná$ky. !

P#íklad 3.45 Uka"me, "e po"adavek, aby ! nem!la volné prom!nné, je pod-statn%. [#e$ení: Nech+ ! je r(x) (r je unární rela'ní symbol), " nech+ je (/x)r(x),T nech+ je prázdná mno"ina; pak u"itím pravidla generalizace dostaneme T,! )", ov$em T ) ! " neplatí. Kdyby to platilo, pak by dle v!ty o korektnosti(kterou uvedeme za chvíli) bylo T |= ! ", tj. r(x) (/x)r(x) by byla tauto-logií, co" neplatí (nap#. neplatí ve struktu#e s mno"inou p#irozen%ch 'ísel jakouniverzem, kde r je interpretován jako mno"ina 'ísel v!t$ích ne" 5 (nebo jakákolimno"ina r&zná od mno"iny v$ech p#irozen%ch 'ísel)).]

3.3.1 Dal%í tvrzení, která jsou analogiemi tvrzení z v"rokové logiky

V!ta o dedukci platná pro predikátovou logiku (V!ta 3.44) je typick%m p#íkla-dem #ady tvrzení, která mají z na$eho pohledu (znalc& v%rokové logiky) násle-dující charakter. Jsou analogiemi nám znám%ch tvrzení z v%rokové logiky. Li$íse v$ak od nich jednak tím, "e v nich tvrdíme n!co o jin%ch objektech (nap#. tvr-zení se t%kají formulí predikátové logiky, nikoli formulí v%rokové logiky), jednaktím, "e obsahují dodate'né p#edpoklady, které jsou v p#ípad! v%rokové logikyzbyte'né. Jde zejména o následující: v!ta o d&kazu sporem, v!ta o d&kazu roz-borem p#ípad&, v!ta o neutrální formuli, v!ta o ekvivalenci. Dobr%m cvi'enímje zformulovat si uvedené v!ty pro p#ípad predikátové logiky a dokázat je (ana-logicky jako ve v%rokové logice, jen je t#eba dát pozor na n!které p#edpoklady,tak jako tomu bylo u v!ty o dedukci).

3.3.2 Tvrzení o formulích s kvantifikátory

Dal$í #adou tvrzení o predikátové logice jsou tvrzení o kvantifikátorech. Tatotvrzení pochopiteln! nemají analogie ve v%rokové logice. Za'neme následujícímu"ite'n%m tvrzením.

V$ta 3.46 (o uzáv$ru) Pro ka$dou teorii T a formuli ! platí

T ) ! práv& kdy$ T ) (/x)!.

Tedy, formule je dokazatelná, práv& kdy$ je dokazateln! její libovoln! uzáv&r.

35

D̊ukaz. P#edpokládejme T ) !. Pak T ) (/x)! díky G (podrobn!ji, je-li . . . ,!d&kaz ! z T , je . . . ,!, (/x)! d&kazem (/x)! z T ).P#edpokládejme T ) (/x)!. Proto"e (/x)! ! je axiom (9), kde t = x, je

) (/x)! !, tedy T ) ! pou"itím MP. !

V$ta 3.47 Pro formule !," platí

) (/x)(! ") ((/x)! (/x)") (16)

) (/x)(! ") ((1x)! (1x)") (17)

) (/x)(! ") (! (/x)") (18)

není-li x volná ve !

) (/x)(! ") ((1x)! ") (19)

není-li x volná v "

) (1x)(! ") (! (1x)") (20)

není-li x volná ve !

) (1x)(! ") ((/x)! ") (21)

není-li x volná v "

) (/x)(/y)! (/y)(/x)! (22)

) (1x)(1y)! (1y)(1x)! (23)

) (1x)(/y)! (/y)(1x)! (24)

D̊ukaz. !

Dal$í tvrzení — viz p#edná$ky. Ke zkou$ce je t#eba znát principy práce skvantifikátory a um!t provád!t jednoduché úvahy o kvantifikátorech v tom roz-sahu, jak bylo probíráno zejm. na cvi'ení (o distribuci kvantifikátor&, o zám!n!po#adí kvantifikátor& a implikace, kvantifikace a negace, o zám!n! po#adí kvan-tifikátor&).Na p#edná$kách jsme uvedli dal$í tvrzení, uvád!jící dokazatelné formule pre-

dikátové logiky: o distribuci kvantifikátoru, o rovnosti, o zám!n! po#adí kvanti-fikátor& a implikace, o zám!n! po#adí kvantifikátor&.

3.4 Úplnost predikátové logiky

Cílem je dostat se k v!t! o úplnosti (tj. “dokazatelné = v"dy pravdivé”) propredikátovou logiku; nejd#íve uvedeme v!tu o korektnosti. Úplnost poté uká"ememetodou tzv. henkinovsk%ch roz$í#ení teorií.

V$ta 3.48 (o korektnosti) Pro libovolnou teorii T a libovolnou formuli ! ja-zyka teorie T platí, $e

z T)! plyne T |=!.

36

D̊ukaz. Na stejném principu jako pro v%rokovou logiku (podrobn!ji viz p#ed-ná$ky). !

Poznámka 3.49 Jednoduch%m d&sledkem je fakt: sporná teorie nemá model.Toti", kdyby byla T sporná, pak pro ka"dou formuli ! by platilo T ) ! i T ) !.Dle V!ty o korektnosti by muselo b%t v ka"dém modelu teorie T pravdivé ! i

!, co" není mo"né.

P#istoupíme nyní k d&kazu v!ty o úplnosti. Nejprve uvedeme n!kolik po-mocn%ch tvrzení (sama o sob! jsou v$ak zajímavá).

Definice 3.50 Teorie S je roz&í#ením teorie T , jestli"e jazyk S obsahujejazyk T a je-li ka"d% axiom teorie T dokazateln% v S. Roz$í#ení S teorie Tse naz%vá konzervativní , jestli"e ka"dá formule jazyka teorie T , která jedokazatelná v S, je dokazatelná také v T . Teorie jsou ekvivalentní , jestli"ejsou jedna druhé roz$í#ením.

Poznámka 3.51 Snadno se uká"e, "e je-li S roz$í#ením T , je ka"dá formuledokazatelná v T dokazatelná také v S.

V$ta 3.52 (o konstantách) Je-li S roz%í'ení T takové, $e jazyk S obsahujenové konstanty c1, . . . , cn, které jsou od sebe r"zné, ale S neobsahuje nové axi-omy. Pak pro ka$dou formuli ! jazyka teorie T platí

T)! práv& kdy$ S)!(x1/c1, . . . , xn/cn).

D̊ukaz. Tvrzení doká"eme nejd#ív pro jednu konstantu (tj. pro n = 1); pak hoindukcí roz$í#íme na více konstant. P#edpokládejme tedy n = 1 a pro jednodu-chost pi$me c místo c1.“+”: P#edpokládejme T)!. Nech+ . . . ,! je d&kaz ! z T . V teorii S lze

tento d&kaz prodlou"it o formule (/x)! (G na !), (/x)! !(x/c) (axiom (9)),!(x/c) (MP na p#edchozí formule). Tedy

. . . ,!, (/x)!, (/x)! !(x/c),!(x/c)

je d&kaz z S, a proto S)!.“*”: Nech+ S)!(x/c), tj. nech+ existuje d&kaz !1, . . . ,!k formule !(x/c) z S

(tj. !k = !(x/c)). Vezm!me prom!nnou y, která se v tomto d&kazu nevyskytuje(tj. nevyskytuje se v "ádné z !i). Indukcí uká"eme, "e !1(c/y), . . . ,!k(c/y) jed&kaz z T .P#edpokládejme tedy (induk'ní p#edpoklad), "e !1(c/y), . . . ,!i#1(c/y) je

d&kaz z T a uka"me, "e i !1(c/y), . . . ,!k(c/y) je d&kaz z T . Proto"e !1, . . . ,!k

je d&kaz z S, mohou nastat následující p#ípady.

• !i je n!kter% z axiom& (??–??): Snadno se vidí, "e pak je !i(c/y) také axi-omem. Je ov$em t#eba ov!#it, "e v p#ípad! axiom& (??)–(??) jsou spln!nyp#edpoklady (to se snadno uká"e; ov!#te).

37

• !i je formule z S: Podle p#edpoklad& jsou formule z S a z T stejné (RE-FORMULATE), tedy !i je i formulí z T . Potom ale !i neobsahuje kon-stantu c, a tedy !i je toto"ná s !i(c/y).

• !i vypl%vá z p#edchozích formulí pomocí odvozovacího pravidla MP neboG: Pokud !i vypl%vá z !j a !k (j, k < i) pomocí MP (tj. nap#. !j = !k

!i), pak !j(c/y) je !k(c/y) !i(c/y) a tedy !i(c/y) vypl%vá pomocí MPz !j(c/y) je !k(c/y). Pokud !i vypl%vá z !j (j < i) pomocí G (tj. !i je(/x)!j), pak !i(c/y), co" je [(/x)!j ](c/y), je rovna (/x)[!j(c/y)], nebo+podle p#edpokladu je y r&zná od x, a tedy !i(c/y) vypl%vá z !j(c/y)pomocí G.

Ukázali jsme tedy T)[!(x/c)](c/y). Proto"e [!(x/c)](c/y) je formule !(x/y),máme T)!(x/y). Je vid!t, "e x je substituovatelná za y ve formuli !(x/y). Protoplatí, "e prodlou"íme-li d&kaz . . . ,!(x/y) z T na posloupnost

. . . ,!(x/y), (/y)!(x/y), (/y)!(x/y) [!(x/y)](y/x), [!(x/y)](y/x),

dostali jsme d&kaz formule [!(x/y)](y/x) z T (postupn! pou"itím G, axiomu(??), MP). Uv!domíme-li si, "e [!(x/y)](y/x) je formulí !, vidíme T)!.Nyní tvrzení snadno roz$í#íme na c1, . . . , cn: Zatím jsme dokázali, "e za uve-

den%ch podmínek platí T)! práv! kdy" S)!(x/c). Ozna'íme-li T " teorii S (tj.její jazyk obsahuje c1) a jako S" teorii, která vznikne z S p#idáním c2 do jazyka,dostaneme pou"itím dokázaného tvrzení na formuli " = !(x1/c1), "e T ")",práv! kdy" S")"(x2/c2), tj. máme S)!(x1/c1), práv! kdy" S")!(x1/c1, x2/c2).Zárove( máme T)!, práv! kdy" S)!(x1/c1), tedy celkem T)!, práv! kdy"S")!(x1/c1, x2/c2). Opakovan%m pou"itím této úvahy nakonec dostaneme po-"adované tvrzení. !

Poznámka 3.53 Speciáln! tedy je za podmínek V!ty 3.52 S konzervativní roz-$í#ení T .

Definice 3.54 Formule ! je variantou formule ", jestli"e existuje posloup-nost ! = $1, $2, . . . , $n = " formulí tak, "e pro ka"dé i < n vznikne formule$i+1 z formule $i nahrazením jedné podformule formule $i, která je tvaru (/x)#(pop#. (1x)#) formulí (/y)#(x/y) (pop#. (1y)#(x/y)), kde prom!nná y je sub-stituovatelná za x v # a není volná v #.

V$ta 3.55 (o variantách) Je-li " varianta !, pak )! ".

D̊ukaz. Viz p#edná$ky. !

Následuje u"ite'né (a zajímavé) tvrzení.

Lemma 3.56 Pro teorii T , formuli ! a libovoln! uzáv&r ! formule ! je

T ) ! práv& kdy$ T, ! je sporná.

38

D̊ukaz. Nech+ T ) !. Dle V!ty 3.46 je T ) !. Nech+ " je libovolná formule.Doká"eme T, ! ) ". Máme

) ! ( ! ") [pou"ití Lemma 3.42 na tautologii p ( p q)v%rokové logiky]

T ) ! " [MP]T, ! ) " [MP],co" znamená, "e T, ! je sporná.Naopak, nech+ je T, ! sporná. Pak mámeT, ! ) ! [ze spornosti T, !]T ) ! ! [v!ta o dedukci]) ( ! !) ! [pou"ití Lemma 3.42 na tautologii ( p p) p

v%rokové logiky]T ) ! [MP]T ) ! [v!ta o uzáv!ru (V!ta 3.46)]. !

Definice 3.57 Teorie T se naz%vá henkinovská 3, jestli"e pro ka"dou formuli!(x) se v jazyce teorie T vyskytuje konstanta c tak, "e formule (1x)! !(x/c)je dokazatelná v T . Konstanta c se naz%vá henkinovská konstanta , (1x)!!(x/c) se naz%vá henkinovská formule p#íslu$ná formuli !.

V$ta 3.58 (o henkinovské konstant$) Je-li !(x) formule jazyka teorie T aje-li S roz%í'ení T vzniklé p'idáním (henkinovské) konstanty c! a (henkinovské)formule (1x)! !(x/c), pak S je konzervativním roz%í'ením teorie T .

D̊ukaz. Ozna'me R teorii vzniklou z T p#idáním c! (tj. S vznikne p#idáním(1x)! !(x/c) k R). Nech+ pro formuli " jazyka teorie T platí S ) ", tj.R, (1x)! !(x/c) ) ". Abychom prokázali konzervativnost roz$í#ení S, mu-síme dokázat T ) ". Zvolme prom!nnou y, která se nevyskytuje v "ádné z ! a". Podle V!ty o dedukci máme

R ) [(1x)! !(x/c!)] "

a podle V!ty o konstantách (uvá"íme-li, "e {[(1x)! !(x/y)] "}(y/c!) je[(1x)! !(x/c!)] ") dále

T ) [(1x)! !(x/y)] ",

z 'eho" pou"itím G dostaneme

(/y)[(1x)! !(x/y)] ",

odtud dále (podle pravidel práce s kvantifikátory)

(1y)[(1x)! !(x/y)] ",

3L. Henkin, . . .

39

odtud dále (podle pravidel práce s kvantifikátory)

[(1x)! (1y)!(x/y)] ",

odkud dostanemeT ) "

pou"itím MP na p#edcházející dokazatelnost. Toti", platí ) (1x)! (1x)! adle V!ty o variantách je tedy ) (1x)! (1y)!(x/y) (m&"eme tedy aplikovatMP). !

V$ta 3.59 (o henkinovském roz%í#ení) Ke ka$dé teorii existuje henkinov-ská teorie, která je jejím konzervativním roz%í'ením.

D̊ukaz. Nech+ T0 je v%chozí teorie. K té sestrojíme henkinovské roz$í#ení násle-dovn!. Nejprve sestrojíme posloupnost teorií T1, T2, . . . následovn!.Konstrukce Ti+1zTi: Jazykem Ti+1 bude jazyk Ti obohacen% o henkinovské

konstanty v$ech formulí jazyka Ti s jednou volnou prom!nnou (na$ím cílem jetoti" “odstranit nehenkinovskost” Ti); axiomy Ti+1 jsou axiomy Ti a henkinov-ské axiomy p#íslu$né ke v$em formulím jazyka Ti s jednou volnou prom!nnou.Tvrdíme, "e ka"dá Ti+1 je konzervativním roz$í#ením Ti. Musíme tedy uká-

zat, "e je-li " formule jazyka Ti, pro kterou Ti+1 ) ", pak Ti ) ". Nech+ je tedyTi+1 ) " a nech+ "1, . . . ,"n je p#íslu$n% d&kaz. Uva"ujme v$echny konstantyc!1 , . . . , c!k , které se vyskytují v d&kazu "1, . . . ,"n, ale nepat#í do jazyka Ti.Uva"ujme dále teorie S0, S1, . . . , Sk takové, "e S0 = Ti, Si+1 vznikne z Si roz$í-#ením o c!i+1 a p#íslu$n% henkinovsk% axiom. Pak je "1, . . . ,"n je d&kazem " zSk, a tedy podle V!ty o henkinovské konstant! je Sk#1 ) ", z 'eho" postupnouaplikací V!ty o henkinovské konstant! dostaneme Sk#2 ) ", . . . , S0 ) ", tj.Ti ) ".Proto"e "ádná z Ti je$t! nemusí b%t henkinovská (roz$í#ením jazyka toti"

mohou vzniknout nové formule, které poru$ují henkinovskost), uva"ujme dáleT =

"i=1,2,... Ti. P#ímo z konstrukce T plyne, "e je to henkinovská teorie

(ov!#te). Navíc je konzervativním roz$í#ením p&vodní T0, nebo+ je-li " n!jakáformule jazyka T0 a !1, . . . ,!n je d&kaz " z T , pak je to také d&kaz " z n!-jakého Ti (pro dostate'n! velké i), a tedy z konzervativnosti Ti plyne, "e " jedokazatelná z T0. !

Definice 3.60 Teorie T se naz%vá úplná , jestli"e je berzesporná a jestli"epro ka"dou uzav#enou formuli ! je bu) T ) !, nebo T ) !.

V$ta 3.61 (o zúpl'ování teorií) Ke ka$dé bezesporné teorii existuje její roz-%í'ení se stejn!m jazykem, které je úplnou teorií.

D̊ukaz. P#edpokládejme pro jednoduchost, "e mno"ina v$ech uzav#en%ch for-mulí daného jazyka je spo'etná (co" nap#íklad platí, je-li spo'etn% dan% jazyk;

40

není-li mno"ina v$ech formulí spo'etná, m&"eme ji tzv. dob#e uspo#ádat a postu-povat odpovídajícím principem indukce), tj. v$echny uzav#ené formule m&"emeuspo#ádat do posloupnosti !1,!2, . . .. Nech+ T je daná bezesporná teorie. Proi = 1, 2, . . . budeme sestrojovat teorie Ti 7 T , které budou bezesporn%mi roz$í-#eními teorie T . Polo"me navíc T0 = T .Konstrukce pro dané i: P#edpokládejme, "e pro j < i máme sestrojeny Tj 7

T , které jsou bezesporn%mi roz$í#eními teorie T . Ozna'me

S =#

j<i

Tj.

Platí, "e S je bezesporn%m roz$í#ením T . Skute'n!, kdyby byla S sporná, existo-val by z S d&kaz "1, . . . ,"n n!jaké v"dy nepravdivé formule !. Pak ale existujej" < i tak, "e ve$keré p#edpoklady z S, které jsou prvky d&kazu "1, . . . ,"n,pat#í do Tj! , tedy "1, . . . ,"n je d&kazem z Tj! , co" není mo"né, proto"e podlep#edpokladu je Tj! bezesporná.Je-li S ' {!i} bezesporná, polo"me Ti = S ' {!i}. V tom p#ípad! je Ti

bezesporné roz$í#ení T .Je-li S ' {!i} sporná, polo"me Ti = S ' { !i}. Proto"e je S ' {!i} sporná,

je podle Lemma 3.56 S ) !i (p#i aplikaci Lemma 3.56 si uv!domte, "e !i jeuzav#ená a "e S ' {!i} je sporná, práv! kdy" je sporná S ' { !i}). Proto"eje S bezesporná, je bezesporná i Ti = S ' { !i}.Hledan%m roz$í#ením T " je pak T " =

"i=1,2,... Ti. Bezespornost T " se uká"e

podobn! jako bezespornost S v%$e; úplnost T " je z#ejmá z jeho konstrukce. !

Definice 3.62 (kanonická struktura) Kanonická struktura MT teorie Tje dána následovn!:

• univerzem MT je mno"ina v$ech uzav#en%ch term& (tj. neobsahujícíchprom!nné) jazyka T ;

• pro n-ární rela'ní symbol r ! R je relace rMT definována p#edpisem

"t1, . . . , tn# ! rMT práv! kdy" T ) r(t1, . . . , tn);

• pro n-ární funk'ní symbol f ! F je funkce fMT definována p#edpisem

fMT (t1, . . . , tn) = f(t1, . . . , tn).

Poznámka 3.63 V$imn!me si, "e v definici kanonické struktury je pou"it ele-gantní trik: K dané teorii je definována struktura, tj. sémantick% pojem, která jev$ak sestavena jen ze syntaktick%ch prvk& a pojm&. Nosi'em kanonické struk-tury je mno"ina v$ech uzav#en%ch term&, tedy term&, které neobsahují pro-m!nné. Aby tedy kanonická struktura v&bec existovala, je nutné, aby jazyk danéteorie obsahoval symboly konstant. Funkce fMT jsou definovány jednodu$e: proprvky t1, . . . , tn univerza (jsou to uzav#ené termy) je v%sledkem aplikace defino-vané funkce fMT na t1, . . . , tn #et!zec f(t1, . . . , tn), co" je uzav#en% term, tedy

41

prvek univerza. Konstrukce relací rMT je d&mysln!j$í. Vyu"ívá se p#i n!m (ne-triviální) pojem dokazatelnosti. n-tice "t1, . . . , tn# je v relaci rMT , práv! kdy" jeformule r(t1, . . . , tn) dokazatelná v teorii T .

V$ta 3.64 (o kanonické struktu#e) Je-li T úplná henkinovská teorie, pakMT je modelem T .

D̊ukaz. Doká"eme nejd#íve následující tvrzení (ozna'ne ho (8)): pro ka"douuzav#enou instanci !" formule ! je T ) !", práv! kdy" $!"$MT = 1 (uzav#enáinstance formule ! je ka"dá taková formule !", která vznikne z ! aplikací n!jakékorektní substituce, tj. n!které prom!nné se nahradí termy, p#itom !" je samauzav#enou formulí; " tedy ozna'uje n!jaké korektní nahrazení prom!nn%ch termy,které z ! ud!lá !"). Z toho speciáln! plyne, "e pro ka"dou uzav#enou formuli !je T ) !, práv! kdy" $!$MT = 1 (nebo+ uzav#ená formule je uzav#enou instancísama sebe).Dále m&"eme p#edpokládat, "e ka"dá formule z T je uzav#ená. Skute'n!, je-li

$ uzáv!rem ", je S ' {"} ) !, práv! kdy" S ' {$} ) ! (doká"e se podobnouúvahou jako V!ta o uzáv!ru). Tedy T dokazuje stejné formule jako teorie, kteráz T vznikne nahrazením formulí s voln%mi prom!nn%mi jejich uzáv!ry.Z toho pak plyne, "eMT je modelem T následovn!. Je-li ! uzav#ená formule

z T , pak je T ) !, a tedy $!$MT = 1 (! je pravdivá vMT ) podle (8).Zb%vá dokázat tvrzení (8): Tvrzení doká"eme strukturální indukcí p#es !.Je-li ! atomická, tj. ! je tvaru r(t1, . . . , tn), pak tvrzení plyne p#ímo z defi-

nice rMT (a z toho, "e $!$MT = 1 znamená "t1, . . . , tn# ! rMT ).P#edpokládejme, "e tvrzení platí pro ! a " a doka"me, "e platí také pro !,

! " a (1x)!.!: Máme ( !)" = (!"), tedy T ) (!") práv! kdy" (z bezespornosti a

úplnosti T ) není T ) !", co" podle p#edpokladu platí práv! kdy" $!"$MT = 0,co" je práv! kdy" $ (!")$MT = 1.

! ": Uv!domme si následující: (a) (! ")" = !" ""; (b) $!"

""$MT = 1 práv! kdy" $!"$MT = 1 implikuje $""$MT = 1; (c) z T ) !" ""

plyne, "e T ) !" implikuje T ) "". Z toho plyne (promyslete!), "e sta'í ov!#it,"e neplatí-li T ) !" "", pak neplatí, "e T ) !" implikuje T ) "". To ale platí.Toti", neplatí-li T ) !" "", pak z úplnosti T plyne T ) (!" ""), tedyT ) !" "", tedy T ) !" a T ) "". Z bezespornosti a úplnosti T plyne, "eneplatí T ) "".(1x)!: Je-li T ) (1x)!, pak z henkinovskosti teorie T dostaneme pou"itím

MP, "e T ) !(x/c). Z p#edpokladu, "e tvrzení platí pro ! (!(x/c) je uzav#enouinstancí !), dostaneme $!(x/c)$MT = 1, tedy z definice je $(1x)!$MT = 1.Naopak, není-li T ) (1x)!, pak z úplnosti T je T ) (1x)!, tedy T ) (/x) !.Pro ka"d% uzav#en% term t máme dále ) (/x) ! !(x/t) (nebo+ dot'enádokazatelná formule je axiom (9)), pou"itím MP tedy dostaneme T ) !(x/t),a proto"e tvrzení platí pro !, dostáváme $ !(x/t)$MT = 1. Proto"e univer-zum MT obsahuje pouze uzav#ené termy, platí pro ka"dé ohodnocení e (uv!do-mme si, "e jedinou volnou prom!nnou formule ! je x), "e $ !$MT ,e = 1,

42

tedy $(/x) !$MT ,e = 1, a tedy $(1x)!$MT ,e = 0, co" bylo t#eba dokázat.D&kaz (8) je hotov. !

Definice 3.65 (kanonická struktura s rovností)MT / 0MT — viz p#edná$ky

V$ta 3.66 (o kanonické struktu#e s rovností) Je-li T úplná henkinovskáteorie s rovností, pak MT / 0MT je modelem T .

D̊ukaz. Nebude u zkou$ky po"adován. !

Poznámka 3.67 Nech+ teorie S je roz$í#ením teorie T . Mají-li S a T stejn%jazyk, je z#ejm! ka"d% model teorie S také modelem teorie T . Je-li jazyk teorieS bohat$í ne" jazyk teorie T , tj. RT 9 RS nebo FT 9 FS , kde RT , FT a RS , FS

ozna'ují po #ad! rela'ní a funk'ní symboly jazyka teorie T a S, je z ka"déhomodeluMS teorie S mo"né vytvo#it modelMT teorie T vypu$t!ním p#íslu$n%chrelací a funkcí, tj.MT =MS, RMT = {rMS | r ! RT }, FMT = {fMS | f ! FT }.Zjednodu$en! v$ak m&"eme i v tomto p#ípad! #íkat, "e ka"d% model teorie S jetaké modelem teorie T .

V$ta 3.68 (o úplnosti) (1) Ka$dá bezesporná teorie má model. (2) Pro ka$-dou teorii T a ka$dou formuli ! platí, $e

je-li T |= !, pak T ) !.

D̊ukaz. (1) Nech+ T je bezesporná teorie. Dle V!ty 3.59 existuje její henkinovskéroz$í#ení T ", které je jejím konzervativním roz$í#ením. Proto"e T " je konzerva-tivní roz$í#ení, plyne z bezespornosti T , "e T " je také bezesporná (kdyby byla T "

sporná, platilo by pro jakoukoli formuli ! jazyka teorie T , "e T " ) ! i T " ) !. Zkonzervativnosti by dále plynulo, "e T ) ! i T ) !, a tedy T by byla sporná).Dle V!ty 3.61 existuje roz$í#ení T "" teorie T ", které má stejn% jazyk jako teorieT " a je úplnou teorií. Proto"e je T " henkinovská teorie, je henkinovská i T "". DleV!ty 3.64, pop#. V!ty 3.66 (pokud se jedná o jazyk s rovností), existuje modelteorie T "". Ten je v$ak také modelem teorie T (viz Poznámku 3.67).(2) Ozna'me ! libovoln% uzáv!r formule !. Kdyby neplatilo T ) !, pak

by teorie T, ! byla dle Lemma 3.56 bezesporná. Podle (1) by tedy T, !m!la model M. V M je pravdivá !, tedy je v n!m nepravdivá !. Proto"e vestruktu#e je formule pravdivá, práv! kdy" je v ní pravdiv% její uzáv!r, je v Mnepravdivá formule !.M je tedy modelem teorie T , ve kterém neplatí !, co" jespor s p#edpokladem T |= !. !

Teorie T je mno"ina formulí. Podteorie S dané teorie je její podmno"ina (tj.S . T ).

V$ta 3.69 (o kompaktnosti) Teorie má model, práv& kdy$ ka$dá její kone(nápodteorie má model.

43

3.5 Prenexní tvar, dokazatelnost v predikátové logice vs.v!roková dokazatelnost

Toto nebylo v p#edná$kách (!), u zkou$ky nebude obsah sekce 3.5 po"adován.Následující v%sledky jsou mimo jiné v%znamné pro logické základy tzv. au-

tomatizovaného dokazování. Prenexní tvar jej jistou normální formou formule,Hilbert-Ackermannova a Herbrandova v!ta p#evád!jí pro ur'ité p#ípady doka-zatelnost (slo"it!j$í pojem) na v%rokovou dokazatelnost (jednodu$$í pojem).Teorie se naz%vá otev#ená, jsou-li v$echny její axiomy otev#ené formule. In-

stance dané formule je formule, která z dané formule vznikne korektní substitucíterm& za prom!nné.

V$ta 3.70 (Hilbert-Ackermannova) Otev'ená teorie T je sporná, práv& kdy$existuje kone(ná teorie S se stejn!m jazykem jako T , která má za axiomy pouzeinstance axiom" rovnosti a instance axiom" teorie T a která je v!rokov& sporná.

D̊ukaz. Nebude u zkou$ky po"adován. !

Definice 3.71 Formule je v prenexním tvaru , je-li ve tvaru (Q1x1) . . . (Qnxn)!,kde Qi je bu) / nebo 1, xi jsou navzájem r&zné prom!nné a formule ! je ote-v#ená (tj. neobsahuje kvantifikátory) ; (Q1x1) . . . (Qnxn) se naz%vá prefix, !jádro.

P#íklad 3.72 Formule (/x)(/y)(1z)(/u)(r(x, y, u) ( f(y)) je v prenexním tvaru;formule (/x)(1y)(r(y) (/x)s(y)) ani (/x)(/y)(1x)r(x, y) nejsou.

V$ta 3.73 (o prenexním tvaru) Ke ka$dé formuli ! existuje formule " vprenexním tvaru tak, $e ) ! ".

D̊ukaz. Pro ka"dou formuli ! = !0 sestrojíme pomocí postupn%ch úprav po-sloupnost vzájemn! ekvivalentních formulí !0,!1, . . . ,!n tak, !i je ekvivalentnís !i+1 a !n je v prenexním tvaru. Úpravy jsou takové, "e p#evád!jí kvantifiká-tory na za'átek formule. Snadno se vidí, "e lze uva"ovat jen následující p#ípady:Není-li !i v prenexním tvaru, obsahuje podformuli tvaru (Qx)# nebo

(Qx)# " nebo # (Qx)" (Q je n!kter% kvantifikátor). Tuto podformulinahradíme ve !i s ní ekvivalentní formulí a dostaneme !i+1. Nech+ k Q je Q"

ten druh% kvantifikátor (tj. /" je 1 a 1" je /).Podformuli tvaru (Qx)# nahradíme (Q"x) #.U podformule tvaru (Qx)# " (pop#. # (Qx)") nejprve p#ejmenujeme

prom!nné tak, aby (Qx)# a " (pop#. # a (Qx)") neobsahovaly spole'né pro-m!nné. P#ejmenováním získaná formule (Qy)#" "" (pop#. #" (Qy)"")je ekvivalentní s (Qx)# " (pop#. # (Qx)"). Formule (Qy)#" ""

(pop#. #" (Qy)"") je dále dle v!tu o zám!n! po#adí kvantifikátoru a im-plikace ekvivalentní formuli (Q"y)(#" "") (pop#. (Qy)(#" "")). Podformuli(Qx)# " nahradíme formulí (Q"y)(#" ""), podformuli # (Qx)" nahra-díme (Qy)(#" ""). !

D&kaz p#edchozí v!ty má konstruktivní charakter:

44

P#íklad 3.74 P#evedte formuli (/y)[(/z)(1x)r(x, y) (/x) (/y)s(x, y)] doprenexního tvaru. Nejprve p#esuneme negaci a získáme (/y)[(/z)(1x)r(x, y)(/x)(1y) s(x, y)]. V podformuli [(/z)(1x)r(x, y) (/x)(1y) s(x, y)] prove-deme p#ezna'ení dostaneme [(/z)(1x)r(x, y) (/x")(1y") s(x", y")]. Provede-ním úprav v této formuli dostaneme s ní ekvivalentní formuli (1z)(/x)(/x")(1x")[r(x, y)s(x", y")]. Celkem je tedy p&vodní formule ekvivalentní formuli (/)(1z)(/x)(/x")(1x")[r(x, y)s(x", y")], která ji" je v prenexním tvaru.

Nech+ ! je uzav#ená formule v prenexním tvaru. Indukcí budeme defino-vat formuli !S (tzv. skolemovskou variantuformule !); ta bude stále v pre-nexní form!, nebude obsahovat existen'ní kvantifikátory, ale bude mo"ná ob-sahovat nové funk'ní symboly (p&jde tedy o formuli nad roz$í#en%m jazykem).Neobsahuje-li ! existen'ní kvantifikátory, je !S p#ímo formule !. P#edpoklá-dejme, "e ! obsahuje existen'ní kvantifikátory, "e je ve tvaru (/x1) . . . (/xn)(1y)"a "e #S je ji6 definováno pro ka"dou formuli #, která má mén! existen'ních kvan-tifikátor& ne" !. Formulí !S bude formule [(/x1) . . . (/xn)"(y/f(x1, . . . , xn))]S ,kde f je nov% n-ární funk'ní symbol.Formule !S je tedy tvaru (/x1 . . . xn)", kde " neobsahuje kvantifikátory. "

pak naz%váme otev'enou skolemovskou variantou formule ! a zna'íme !OS .

P#íklad 3.75 Sestrojte skolemovskou variantu formule (/x)(1y)(/z)(/u)(1v)(/w)[r(x, y)(g(z, v) ( h(u, w))]. [#e$ení: je to nap#. formule (/x, z, u, w)[r(x, f1(x)) (g(z, f2(x, z, u)) (h(u, w))], kde f1, f2 jsou nové funk'ní symboly.]

V$ta 3.76 (Herbrandova) Pro uzav'enou formuli ! v prenexním tvaru je )!, práv& kdy$ existuje kone(ná v!rokov& sporná teorie T , která obsahuje pouzeinstance formule ( !)OS a instance axiom" rovnosti.

D̊ukaz. Nebude u zkou$ky po"adován. !

4 Úvod do fuzzy logikyPro! pot#ebujeme fuzzy logiku? Co je základní motivací.

• Klasická logika nesta'í p#i modelování tzv. vágních tvrzení, nap#. “Petrje velk%.”, “Teplota je vysoká”. Uvedená tvrzení 'asto intuitivn! pova"u-jeme za ani úpln! nepravdivá, ani úpln! pravdivá, tj. za tvrzení, jejich"pravdivostní hodnota le"í mezi 0 a 1, nap#. je to 0.9 (skoro pravda), 0.5nap&l pravda, 0.1 (skoro nepravda).

• S vágními tvrzeními se setkáme tém!# p#i ka"dém popisu reálného sv!ta.Jde tedy o netriviální a $irokou oblast.

• Jako první se uvedenou problematikou z pohledu mo"n%ch aplikací zab%valLotfi A. Zadeh (dnes stále aktivní jako profesor na University of Californiav Berkley) v nesmírn! vlivné práci “Fuzzy sets. Information and Control(1965)”.

45

• Fuzzy logika je dnes bohat! rozvinutá jak po stránce komer'n! úsp!$n%chaplikací (zejm. fuzzy regulátory), tak po stránce teoretick%ch základ&.

Problém volby struktur pravdivostních hodnot, základní po(adavky.

• Mno"inu pravdivostních hodnot budeme zna'it L. P#irozen! po"adujeme,aby 0, 1 ! L (0 ozna'uje “(úplná) nepravda”, 1 ozna'uje “(úplná) pravda”).Po"adujeme, aby L byla 'áste'n! uspo#ádána relací (.

• P#íklady. L = [0, 1]; L = {0, 1} (klasická logika); L je kone'n% #et!zec(nap#. podmno"ina [0, 1]); L = {0, 1}, {0, 1} s uspo#ádáním po slo"kách(pak "a, b# reprezentuje nap#. názor dvou expert&, první #íká a, druh% b,to je p#irozen% p#íklad nelineárn! uspo#ádané struktury pravdivostníchhodnot).

• Dal$í po"adavky: Musí existovat operace na L modelující logické spojky(zejm. : pro konjunkci, % pro implikaci, ). Tyto operace by m!ly mítp#irozené vlastnosti odpovídající vlastnostem po"adovan%m po logick%chspojkách.

• Uka"me si, jak lze tímto zp&sobem dojít k jedné ze základních struk-tur pravdivostních hodnot ve fuzzy logice, k tzv. reziduovan%m svaz&m.Za'n!me po"adavky, které by m!la spl(ovat operace :. Je-li symbolspojky konjunkce, pak p#irozen! chceme, aby se pravdivostní hodnota$! "$ konjunkce formulí ! a " dala vypo'ítat pomocí operace : zpravdivostní hodnoty $!$ formule ! a pravdivostní hodnoty $"$ formule". Chceme tedy mít $! "$ = $!$ : $"$. Dále je p#irozené po"ado-vat, aby : byla komutativní (tj. aby platilo a: b = b: a; chceme toti",aby pravdivostní hodnota formule ! " byla stejná jako pravdivostníhodnota formule " !, ozna'íme-li a = $!$, b = $"$, pak vlastn!chceme a: b = $!$ :$"$ = $! "$ = $" !$ = $"$ : $!$ = b: a,tedy chceme komutativitu :). Z podobného d&vodu chceme, aby : bylaasociativní. Dal$ím po"adavkem je a: 1 = a (nebo+ chceme, aby pro“úpln!” pravdivou formuli ( , tj. $($ = 1, a libovolnou formuli ! pla-tilo $! ($ = $!$). Operace : by dále m!la b%t monotónní, tj. m!loby platit, "e z a1 ( a2 a b1 ( b2 plyne a1: b1 ( a2: b2 (chceme toti",aby pravdivostní hodnota konjunkce rostla s pravdivostními hodnotamikonjungovan%ch formulí). Dal$í po"adavek, kter% v$ak nerozvedeme dodetail&, se t%ká vztahu operací : a %. Lze ukázat, "e chceme-li, aby i vefuzzy logice “dob#e fungovalo” pravidlo modus ponens, vede to na po"ada-vek, aby platilo, "e a: b ( c práv! kdy" a ( b % c. Posledním po"adavkemje, aby v L existovala vzhledem k uspo#ádání ( infima i suprema libovol-n%ch podmno"in (tj. aby existovala

$K a

%K pro libovolnou K . L).

Tento po"adavek plyne z toho, "e chceme p#irozen%m zp&sobem definovatpravdivostní hodnoty formulí (/x)! a (1x)!. Uka"me to na jednoduchémp#íklad!: M!jme tvrzení !i (i ! I), ka"dé z nich nech+ má pravdivostní

46

hodnotu $!i$. Co by m!lo b%t pravdivostní hodnotou tvrzení “pro ka"déi ! I platí !i”? P#irozen% argument #íká, "e by to m!la b%t nejmen$í zev$ech $!i$ a pokud tato neexistuje, pak by to m!lo b%t infimum

$i$I $!i$.

Podobn! dojdeme od tvrzení “existuje i ! I tak, "e platí !i” k po"adavkuexistence suprem.

Reziduované svazy a t-normy V%$e uvedené po"adavky na strukturu prav-divostních hodnot vedou k následující definici.

Definice 4.1 Úpln! reziduovan! svaz je struktura L = "L,4,5,:,%, 0, 1#,kde

(1) "L,4,5, 0, 1# je úpln% svaz (s nejmen$ím prvkem 0 a nejv!t$ím prvkem 1),

(2) "L,:, 1# je komutativní monoid (tj. : je binární operace na L, která jekomutativní, asociativní a platí a: 1 = a),

(3) :,% jsou binární operace na L (naz%vané “násobení” a “reziduum”) spl-(ující a: b ( c práv! kdy" a ( b % c (tzv. podmínka adjunkce).

V$imn!me si, "e úplné reziduované svazy vyhovují v%$e formulovan%m po"a-davk&m. Ka"d% po"adavek se zde objevuje jako jedna z podmínek, které musíúpln% reziduovan% svaz spl(ovat. To v$ak neplatí beze zbytku: nap#. se v definicireziduovaného svazu neobjevuje po"adavek, aby : byla monotónní. Monotón-nost : v reziduovaném svazu v"dy platí (lze to dokázat z ostatních podmínek).Uvedeme p#íklady úpln%ch reziduovan%ch svaz&, které se nej'ast!ji pou"ívají.Mezi nej'ast!ji pou"ívané struktury pravdivostních hodnot pat#í ty, které

mají za nosi' reáln% interval [0, 1] s p#irozen%m uspo#ádáním, tedy a 4 b =min(a, b), a5b = max(a, b). Na nich se pou"ívají t#i páry adjungovan%ch operací: a%: 0Lukasiewiczovy operace (a: b = max(a+ b31, 0), a % b = min(13a+b, 1)), Gödelovy operace (a: b = min(a, b), a % b = 1 pro a ( b a = b jinak),sou'inové operace (a: b = a · b, a % b = 1 pro a ( b a = b/a jinak).Dal$í d&le"itou mno"inou pravdivostních hodnot je {a0 = 0, a1, . . . , an = 1}

(a0 < · · · < an) se dv!ma páry adjungovan%ch operací: ak : al = amax(k+l#n,0)a ak % al = amin(n#k+l,n) (první); ak : al = amin(k,l) a ak % al = an proak ( al a ak % al = al jinak (druhá, ta vznikne restrikcemi Gödelov%ch operacína mno"inu {a0 = 0, a1, . . . , an = 1}).Je-li L = {0, 1}, : je operace klasické konjunkce a % je operace klasické

implikace, pak p#íslu$n% reziduovan% svaz (ve které je uspo#ádání dáno vztahem0 ( 1) je svazem pravdivostních hodnot klasické logiky (a je to a" na jin%mzp&sobem definované operace dvouprvková Booleova algebra). Obecn!ji platí,"e Booleovy algebry jsou “vlastn!” reziduované svazy. P#esn!ji, p#ipome(m!,"e Booleova algebra je (resp. b%vá tak nej'ast!ji definována) svaz s 0 a 1 (0 jenejmen$í a 1 nejv!t$í prvek svazu), kter% je distributivní (tj. platí a4(b5c) = (a4b)5(a4c)) a komplementární (tj. existuje unární operace " zvaná komplementacespl(ující a 4 a" = 0 a a 5 a" = 1). Nyní platí, "e je-li B = "B,4,5," , 0, 1#Booleova algebra, pak definijeme-li L := B, a: b := a 4 b, a % b := a" 5 b,

47

je L = "L,4,5,:,%, 0, 1# reziduovan% svaz spl(ující a: b = a 4 b a a"" = a.Naopak, je-li L = "L,4,5,:,%, 0, 1# reziduovan% svaz spl(ující a: b = a 4 b aa"" = a, pak definujeme-li B := L a a" := a % 0, je B = "B,4,5," , 0, 1# Booleovaalgebra. Vidíme tedy, "e reziduované svazy jsou bohaté struktury zahrnujícínap#. Booleovy algebry (ale také dal$í v%znamné algebraické struktury jakonap#. Heytingovy algebry, MV-algebry, algebry tzv. lineární logiky a dal$í).

Definice 4.2 t-norma je operace : : [0, 1] , [0, 1] % [0, 1], která je komu-tativní, asociativní, monotónní a spl(ující x: 1 = 1. t-norma se naz%vá zlevaspojitá (spojitá), jsou-li ob! funkce a: · a ·: a zleva spojité (spojité).

V%$e uvedené operace : (0Lukasiewicz, Gödel (minimum) a sou'in) jsou t-normy, dokonce spojité (ov!#te!).

V$ta 4.3 "[0, 1],min,max,:,%, 0, 1# je úpln! reziduovan! svaz, práv& kdy$ :je zleva spojitá t-norma a % je dáno vztahem

a % b = sup{c | a: c ( b}.

Ov!#te, "e uveden% vztah mezi % a : v p#ípad! 0Lukasiewicz, Gödel (mini-mum) a product (sou'in) platí.Tak nap#íklad v%$e uvedené 0Lukasiewicz, Gödel (minimum) a product (sou-

'in) jsou spojité t-normy. Platí, "e ka"dou spojitou t-normu lze ze t#í v%$euveden%ch získat jednoduchou konstrukcí.V reziduovaném svazu definujmeme n!které odvozené operace. Mezi nejd&-

le"it!j$í pat#í tzv. bireziduum (6) a negace (¬) definované následovn!:

a 6 b = (a % b) 4 (b % a)

a¬a = a % 0.

Odvo)te formule pro 6 a ¬ pro p#ípady 0Lukasiewicz, Gödel a sou'in.

V"roková fuzzy logika: dv$ pojetí syntaxe, zejména ale neohodnocenásyntaxe; sémantika. Existuje mnoho tzv. fuzzy logik. Ka"dá fuzzy logika jedána n!jakou t#ídou L struktur pravdivostních hodnot. T#ída L je dána n!ja-k%mi dodate'n%mi po"adavky kladen%mi na logické spojky (resp. operace naL). Tak nap#íklad chceme-li, aby platilo ¬¬a = a (tzv. zákon dvojí negace),omezíme se na t#ídu L pravdivostních hodnot definovanou L = {L | L je úpln%reziduovan% svaz spl(ující ¬¬a = a}. Dal$ím po"adavkem m&"e b%t, aby Lbyla lineárn! uspo#ádaná apod. Z v%$e uvedeného je patrné, "e po"adujeme-li¬¬a = a a a: b = a 4 b, pak L sestává práv! z úpln%ch Booleov%ch algeber.Po"adujeme-li navíc, aby mno"iny pravdivostních hodnot byly lineárn! uspo-#ádané, obsahuje L jedinou strukturu pravdivostních hodnot—dvouprvkovouBooleovu algebru, tj. strukturu pravdivostních hodnot klasické logiky.V dal$ím se budeme zab%vat základními pojetími fuzzy logiky.

48

Neohodnocená syntaxe. Nech+ L je tedy n!jaká t#ída struktur pravdi-vostních hodnot, nap#. L je t#ída v$ech reziduovan%ch svaz& na [0, 1] se spojitout-normou :. Jazyk fuzzy logiky s neohodnocenou syntaxí obsahuje na rozdílod jazyka klasické v%rokové logiky tyto symboly spojek: , , , , dále sym-boly n!kter%ch pravdivostních hodnot, nap#. , (a m&"eme chtít pro ka"déa ! [0, 1]). Je-li L ! L struktura pravdivostních hodnot, pak L-ohodnocení e jelibovolné zobrazení z mno"iny v$ech v%rokov%ch symbol& do mno"iny L v$echpravdivostních hodnot, tj. pro v%rokov% symbol p je e(p) ! L chápána jakopravdivostní hodnota tvrzení, které je ozna'eno p.Formule jsou definovány jako obvykle (ka"d% v%rokov% symbol je formule;a (a obecn! ) jsou formule; jsou-li !," formule, pak (! "), (! "),(! "), (! ") jsou formule).Pravdivostní hodnota formule ! p#i ohodnocení e se definuje následovn!:

$p$e = e(p); $ $=0 a $ $e = 1 (a obecn! $ $e = a) jsou formule; $! "$e =$!$e :$"$e, $! "$e = $!$e % $"$e, $! "$e = $!$e 4 $"$e, $! "$e =$!$e 5 $"$e.Formule ! se naz%vá: L-tautologie, pokud $!$e = 1 pro ka"dé L-ohodnocení

e; L-tautologie (pop#. pouze tautologie, pokud je L z#ejmá z kontextu), pokudje to L-tautologie pro ka"dou L ! L.

P#íklad 4.4 P#esv!d'te se, "e je-li L jednoprvková, jejím" jedin%m prvkem Lje dvouprvková Booleova algebra, pak v%$e uvedené pojmy se shodují s odpo-vídajícími pojmy z klasické logiky (speciáln!: pojem pravdivostní hodnota for-mule; tautologie v klasické logice jsou práv! L-tautologie). Tedy klasická logika“vznikne” z obecné fuzzy logiky vhodnou parametrizací (volbou L).

P#íklad 4.5 Uva"ujte L uvedené v%$e (0Lukasiewicz, minimum, sou'in). Na-pi$te p#íklady formulí, zadejte r&zná ohodnocení e, ur'ete pravdivostní hod-noty t!chto formulí. Najd!te formule, které jsou tautologiemi klasické logiky,ale nejsou L-tautologiemi pro 0Lukasiewicz, minimum, sou'in.

P#i tomto p#ístupu je mo"né zcela obdobn!, jak jsme provedli ve v%rokovélogice, zavést pojem d&kazu a pojem dokazatelné formule (z dané teorie; teorieje mno"ina formulí; pravidlo modus ponens je stejné jako ve v%rokové logice,tj. “z ! a ! " odvo) "”). V!ta o korektnosti úplnosti má pak následujícítvar: Formule ! je L-tautologií, práv! kdy" je dokazatelná z p#íslu$n%ch axiom&(jejich podoba je závislá na L; zde nebudeme rozvád!t).Ohodnocená syntaxe. To je jin% p#ístup, z hlediska celkového pojetí fuzzy

p#ístupu je p#irozen!j$í. Pracujeme zde s jednou pevnou strukturou L pravdi-vostních hodnot. Ohodnocená formule je dvojice "!, a#, kde ! je formule podledefinice v%$e (tj. jako u neohodnocené syntaxe) a a je pravdivostní hodnota. Na-místo s formulemi se pracuje s ohodnocen%mi formulemi. Pak teorie je mno"inaohodnocen%ch formulí a to, "e "!, a# pat#í do teorie, #íká, "e formuli ! pova"u-jeme za pravdivou aspo( ve stupni a. Podobn! axiomy jsou ohodnocené formule.Poznamenejme, "e místo teorie jako"to mno"iny ohodnocen%ch formulí je mo"néuva"ovat teorie jako fuzzy mno"iny (neohodnocen%ch) formulí ("e "!, a# pat#í do

49

teorie jako"to mno"iny ohodnocen%ch formulí je stejné jako "e formule ! pat#ído teorie jako"to fuzzy mno"iny formulí ve stupni a); podobn! místo mno"inyaxiom& jako ohodnocen%ch formulí m&"eme uva"ovat fuzzy mno"inu axiom&jako"to (neohodnocen%ch) formulí.D&kaz z teorie je pak posloupnost ohodnocen%ch formulí spl(ujících podobné

podmínky jako d&kaz v neohodnoceném pojetí. Speciáln! pravidlo modus po-nens #íká “z "!, a# a "! ", b# odvo) "", a: b#”. Podrobn!ji, d&kaz z mno"inyA axiom& a z teorie T je posloupnost

"!1, a1#, . . . , "!n, an#

spl(ující pro ka"dé i = 1, . . . , n, "e bu) (1) "!i, ai# je axiom (pat#í do A) nebo (2)"!i, ai# je p#edpoklad (pat#í do T ) nebo (3) "!i, ai# vznikl aplikací odvozovacíhopravidla na p#edchozí prvky d&kazu. Kon'í-li takov% d&kaz ohodnocenou formulí"!, a#, #íkáme mu d&kaz ! ve stupni a. M&"e se stát (a je to p#irozené), "e pro! existuje celá #ada d&kaz& kon'ících "!, ai# ('ím v!t$í ai, tím je ten d&kazlep$í; "!, 1# znamená, "e ! je dokázáno “úpln!”, tj. "e jsme dokázali, "e ! jeúpln! pravdivé). Stupe) dokazatelnosti ! z dané teorie je pak definován jakosupremum v$ech ai, pro která existuje d&kaz kon'ící "!, ai#. V!ta o úplnosti,pak #íká, "e stupe( dokazatelnosti dané formule je roven stupni tautologi'nosti(pravdivosti) dané formule. P#itom stupe( tautologi'nosti formule ! je dán jakoinfimum v$ech $!$e pro v$echna mo"ná L-ohodnocení e.

Úvod do predikátové fuzzy logiky (NEBUDE U ZKOU1KY PO/ADO-VÁNO)syntax, sémantika, fuzzy mno"iny a fuzzy relace, zejm. binární fuzzy relace

na mno"in!, zejm. fuzzy ekvivalence (pro modelování podobnosti)

Úvod do aplikací fuzzy logiky Nejúsp!$n!j$ími aplikacemi fuzzy logikyjsou tzv. fuzzy regulátory a tzv. pravidlové fuzzy systémy. Ty nalezly zejména vJaponsku za'átkem 90. let rozsáhlé komer'ní uplatn!ní. Dokumentuje to fakt,"e slovo “fuzzy” bylo v té dob! zvoleno v Japonsku slovem roku.Co je to fuzzy regulátor? Motivace, jednoduch% p#ípad [VIZ P.EDNÁ1KY]

Poznámka 4.6 D&vody úsp!chu: NE - blízkost fuzzy p#ístupu v%chodnímumy$lení; ANO - povaha japonského trhu (vst#ícn% novinkám), p#íznivé okol-nosti (nízká cena senzor&), koncep'ní jednoduchost (umo"nila rychlé vzd!láníin"en%r&)

Mezi nejv%znamn!j$í aplikace pravidlov%ch fuzzy systém& a fuzzy regulátor&pat#í následující:

• spot#ební elektronika (fuzzy pra'ka (tu je mo"né zakoupit i v *R), fuzzymy'ka, fuzzy vysava', fuzzy kamera apod.)

• #ízení metra v Japonsk%ch m!stech (fuzzy regulátor zaji$+uje plynulé roz-jí"d!ní a br"d!ní, lep$í ne" 'lov!k)

50

• #ízení velké pr&myslové helikoptéry ovládané hlasem (prof. Michio Su-geno); tuto úlohu se klasick%mi metodami nepoda#ilo vy#e$it

• #ízení velk%ch pr&myslov%ch systém& (nap#. pece)

Obecn!ji lze #íci, "e hlavní aplikace fuzzy logiky tvo#í fuzzy rela'ní mode-lování (pravidlové fuzzy systémy jsou p#íkladem), tj. modelování pomocí fuzzyrelací. Krom! zmín!n%ch pravidlov%ch fuzzy systém& se jedná o

• rozhodování;

• information retrieval a vyhledávání;

• shlukování, rozpoznávání.

Pro omezen% rozsah textu se nestihneme v!novat zajímavé oblasti apli-kací fuzzy logiky, kterou je fuzzy logické programování. Jde o roz$í#ení kla-sického logického programování o principy fuzzy modelování (zejména: data-báze fakt& m&"e obsahovat fakt s n!jak%m stupn!m pravdivosti, nap#. faktjeUsporny(octavia19TDI) se stupn!m 0.9, fakt jeUsporny(octavia14MPI) sestupn!m 0.3). Problematika se rozvíjí.

5 Úvod do modální logikyZákladní motivace. Klasická logika nemá prost#edky k formalizaci tvrzeníobsahujících modality, nap#. “je mo"né, "e . . . ”, “je nutné, "e . . . ”. Roz$í#eníklasické logiky, kde toto je mo"né, se naz%vá modální logika. Modální logikana$la uplatn!ní ve formalizaci znalostních systém& a systém&, které pracují s'asem (tzv. temporální logika, viz dále).Základy syntaxe a sémantiky modální logiky Zam!#íme se na v%ro-

kovou modální logiku. Oproti jazyku klasické v%rokové logiky obsahuje jazykmodální logiky navíc unární spojky ! (!! se 'te “je mo"né, "e !”) a ; (;!se 'te “je mo"né, "e !”). Definice formule se p#íslu$n%m zp&sobem roz$í#í (tj.p#idáme pravidlo “je-li ! formule, jsou i !! a ;!” formule).Konkrétní v%znam !! m&"e b%t “je známo, "e !”, “v!#í se, "e !”, “v"dy v

budoucnosti byde platit !” apod.Sémantika modální logiky je zalo"ena na pojmu mo"n% sv!t. Mo"n% sv!t

je obecná kategorie (v jednom mo"ném sv!t! m&"e v dan% okam"ik pr$et, vedruhém ne, apod.), která má #adu interpretací. Mo"né sv!ty mohou b%t 'asovéokam"iky, mohou reprezentovat názory jednotliv%ch expert& (co mo"n% sv!t, toexpert) apod.

Definice 5.1 Kripkeho struktura pro v%rokovou modální logiku je trojiceK = "W, e, r#, kde W -= & je mno"ina mo"n%ch sv!t&, e je zobrazení p#i#azu-jící ka"dému w ! W a ka"dému v%rokovému symbolu p pravdivostní hodnotue(w, p) (p je/není pravdivé ve w), r . W,W je relace dosa"itelnosti ("w, w"# ! rznamená, "e z w je mo"né dostat se do w").

51

Definujeme pravdivostní hodnotu $!$K,w formule ! v K v mo"ném sv!t! wtakto: $p$K,w = e(w, p) (pro v%rokov% symbol); $! 4 "$K,w = 1, práv! kdy"$!$K,w = 1 a $"$K,w = 1 (tedy jako v klasické logice) a podobn! pro ostatnív%rokové spojky; $!!$K,w = 1, práv! kdy" $!$K,v = 1 pro ka"d% v ! W ,pro kter% "w, v# ! r (tj. “je nutné, "e !” znamená, "e ! je pravdivá v ka"démmo"ném sv!t! dosa"itelném z w); $ ; !$K,w = 1, práv! kdy" $!$K,v = 1 pron!jak% v ! W , pro kter% "w, v# ! r (tj. “je mo"né, "e !” znamená, "e ! jepravdivá v n!jakém mo"ném sv!t! dosa"itelném z w).Uka"te, "e !! a ; ! (a duáln!) mají stejné pravdivostní hodnoty. Tedy,

m&"eme za'ít jen s ! a definovat ; jako odvozenou (nebo naopak).

P#íklad 5.2 (1) Pro r = W , W (ka"d% sv!t je dosa"iteln% z ka"dého) sep#íslu$ná logika naz%vá logika znalostí (the logic of knowledge).(2) Platí-li pro n!jaké W " . W , "e r = W , W ", naz%vá se p#íslu$ná logika

logika domn&ní (logic of belief).(3) r je reflexivní, tranzitivní a platí, "e pro ka"dé v, w ! W je "v, w# ! r

nebo "w, v# ! r. Pak se odpovídající logika naz%vá logika (asu (temporálnílogika, temporal logic, tense logic); w ! W se chápou jako 'asové okam"iky.Existují ale i jiné systémy logiky 'asu. Poznamenejme, "e $!!$K,w = 1 pakznamená, "e ! je pravdivá ve v$ech 'asov%ch okam"icích po'ínaje w. Pro r#1

pak $!!$K,w = 1 znamená, "e ! je pravdivá ve v$ech 'asov%ch okam"icích a"po w. Co pak znamená $ ; !$K,w = 1?

Uka"te, "e v p#ípadech (1) a (2) nezávisí $!$K,w na w (tj. je stejná prov$echna w).Dále uka"te, "e pro (1) mají formule !(! ") (!! !"), !! !!!,

;! ! ; !, !! ! pravdivostní hodnotu 1 pro ka"dé K a w.

6 Logické programování a PrologA logic program is a set of axioms, or rules, defining relation-

ships between objects. A computation of a logic program is a de-duction of consequences of the program. A program defines a set ofconsequences, which is its meaning. The art of logic programmingis constructing concise and elegant programs that have the desiredmeaning.Sterling and Shapiro: The Art of Prolog

V této 'ásti se seznámíme se základy logického programování a programova-cího jazyka Prolog. P#edpokládá se znalost základních pojm& predikátové logiky.Pokud ji 'tená# nemá, m&"e 'íst dále, ale n!kter%m pojm&m bude rozum!t jenintuitivn!.

52

6.1 Co je logické programování: základní koncepce a his-torie

Logické programování je jedním z paradigmat programování. Zcela se li$í odostatních paradigmat. Logické programování budeme demonstrovat na p#íklad!jazyka Prolog.Prolog vznikl za'átkem 70. let ve Francii (Marseille). V%znamn%m mezní-

kem byl japonsk% projekt po'íta'& 5. generace, ve kterém byl Prolog vybránjako základní jazyk logického procesoru centrální jednotky po'íta'e. P#esto"ejaponsk% projekt nesplnil zcela o'ekávání, stal se Prolog v%znamn%m jazykemp#edev$ím pro programování úloh um!lé inteligence.Dnes existuje celá #ada implementací Prologu. My se budeme dr"et základ-

ního “jádra”, které je spole'né v!t$in! implementací.Uvidíme, "e programovat v Prologu vy"aduje “odli$n% zp&sob my$lení”.

Proto si budeme p#ed podrobn!j$ím v%kladem jazyka Prolog na p#íkladech ilu-strovat jeho základní rysy.

Program a v"po!et v logickém programování Základní koncepci logic-kého programování vyjad#uje následující dvojice “rovností”:

program = mno"ina axiom&

av%po'et = konstruktivní d&kaz u"ivatelem zadaného cíle,

nebo voln!ji: program je souborem tvrzení, kter%mi programátor (u"ivatel, ex-pert) popisuje ur'itou 'ást okolního sv!ta; v%po'et nad dan%m programem,kter% je iniciován zadáním dotazu, je hledání d&kazu dotazu z daného souborutvrzení.Poznamenejme, "e uvedená koncepce není v&bec nová. Její po'átky sahají a"

k Leibnizovi a jeho projektu tzv. mathesis universalis, tj. univerzálního jazyka,ve kterém bude mo"né zachytit ve$kerou znalost lidstva. Podle Leibnize by pakm!lo b%t mo"né vytvo#it automatick% stroj, kter% pro dané tvrzení (dotaz) zjistí,zda dotaz logicky vypl%vá z daného souboru znám%ch fakt&. Teprve v%sledkylogiky ze za'átku 20. století ukázaly meze a mo"nosti Leibnizovy p#edstavy(podrobn!j$í diskuze je nad rámec tohoto textu; 'tená#e odkazuji nap#. na [6]).P#esto, "e je to koncepce p#irozená, doznala praktické realizace, jak bylo

uvedeno, a" v 70. letech 20. století.Shr(me a dopl(me nyní základní rysy logického programování:

• logick% program je kone'ná mno"ina formulí (tvrzení popisující okolní re-alitu; formule mají speciální tvar)

• v%po'et je zahájen zadáním formule-dotazu (tu zadává u"ivatel)

• cílem v%po'tu je najít d&kaz potvrzující, "e dotaz logicky vypl%vá (jedokazateln%) z logického programu (konstruktivnost)

53

• pokud je takto zji$t!no, "e dotaz z programu vypl%vá, v%po'et kon'í au"ivateli je oznámeno Yes s hodnotami p#ípadn%ch prom!nn%ch, které sev dotazu vyskytují

• pokud není zji$t!no, "e dotaz z programu vypl%vá, v%po'et kon'í a u"iva-teli je oznámeno No

• m&"e se stát, "e v%po'et nesko'í

Základní rysy (pozd!ji se o nich p#esv!d'íme), kter%mi se logické programo-vání zásadn! odli$uje od ostatních programovacích paradigmat:

• programování: programátor specifikuje, co se má vypo'ítat, a ne jak se tomá vypo'ítat a kam ulo"it meziv%sledky

• #ízení v%po'tu: Prolog nemá p#íkazy pro #ízení b!hu v%po'tu ani pro #ízenítoku dat, nemá p#íkazy cykl&, v!tvení, p#i#azovací p#íkaz

• prom!nné: neexistuje rozd!lení prom!nn%ch na vstupní a v%stupní, pro-m!nná m&"e b%t jednou pou"ita jako vstupní, jindy jako v%stupní; pro-m!nná v Prologu ozna'uje b!hem v%po'tu objekt, kter% vyhovuje jist%mpodmínkám

• nerozli$uje se mezi daty a programem.

Nesmíme v$ak podlehnout lákadlu: je t#eba mít na pam!ti, "e programátornení zbaven zodpov!dnosti za to, jak bude v%po'et probíhat. V%po'et (tj. logickédokazování) je #ízen prologovsk%m p#eklada'em a programátor (alespo( chce-li psát efektivní programy) musí pravidla, kter%mi se v%po'et #ídí, znát a vsouladu s nimi program v Prologu vytvá#et.

6.2 Úvod do základních pojm$ logického programování

6.2.1 První logick" program

Na jednoduchém prologovském programu si uká"eme základní principy a pojmy.Ná$ první program je následující.

muz(petr).muz(jiri).muz(vaclav).muz(pavel).muz(josef).zena(jana).zena(olga).zena(marie).zena(tereza).jeDitetem(petr,jiri).

54

jeDitetem(jana,jiri).jeDitetem(jana,olga).jeDitetem(vaclav,jiri).jeDitetem(vaclav,olga).jeDitetem(jiri,pavel).jeDitetem(jiri,marie).jeDitetem(pavel,josef).jeDitetem(pavel,tereza).jeSynem(X,Y):-muz(X), jeDitetem(X,Y).jeDcerou(X,Y):-zena(X), jeDitetem(X,Y).potomek(X,Y):-jeDitetem(X,Y).potomek(X,Y):-jeDitetem(Z,Y), potomek(X,Z).

Uká"eme: p#e'teme program, #ekneme predikáty, jména predikát&, konstanty,prom!nné, kvantifikace.Dále dotaz: dotaz na fakt bez prom!nné, dotaz na fakt s prom!nnou, kvantifi-

kace u dotazu, opakované #e$ení, dotaz na pravidlo bez prom!nné a s prom!nnou,dále jeDitetem(petr,olga) nevyplyva (a' by se mohlo z kontextu zdát)

6.2.2 Logické programování: fakty, pravidla, dotazy (= Hornovskéklazule)

logicky program = konecna mnozina faktu a pravidel;v Prologu zalezi na jejich usporadani (to je pouzito v algoritmu hledani - viz

prace rezolucnho zasobniku)dalsi typ formuli: dotaz

6.2.3 Co znamená “dokazatelné”: rezolu!ní pravidlo a rezolu!ní do-kazování

strucny uvod

6.2.4 Jak se dokazuje: odstran$ní nedeterminismu, prologovsk" p#e-klada! a zásobník

K tomu: p#íklad práce prologovského zásobníku: (1) bez navracení; (2) s jedno-duch%m navracením

6.2.5 Deklarativní a procedurální sémantika

deklarativni: zalozena na pojmu logickeho vyplyvaniproceduralni: zalozena na SLD-rezoluci, popr. algoritmu prologovskeho za-

sobniku

55

6.3 Úvod do jazyka Prolog

6.3.1 Základy syntaxe, termy

6.3.2 Anonymní prom$nné

6.3.3 )ízení v"po!tu

repeat, fail, cykly, cut, negace

6.3.4 Mimologické predikáty

logicke a aritmeticke operatoryporovnavani termurizeni databazeI/O

6.4 Teoretické základy logického programování

Klauzule, hornovské klauzule Klauzule jsou speciální formule, které hrají vlogickém programování zásadní roli. Hornovské klauzule (A. Horn byl v%znamn%logik) jsou speciální klauzule, se kter%mi pracuje Prolog.

Definice 6.1 Literál je libovolná atomická formule (tzv. pozitivní literál)nebo negace atomické formule (tzv. negativní literál). Klauzule je libovolnádisjunkce literál&. Hornovská klauzule je klauzule, ve které se vyskytujemaximáln! jeden pozitivní literál. Symbolem ! se ozna'uje prázdná klauzule(tj. klauzule obsahující 0 literál&).

Poznamenejme, "e atomické formule se v kontextu logického programovánínaz%vají také atomy.

Poznámka 6.2 (1) ! je v logickém programování symbolem sporu (viz poz-d!ji). Klauzule jsou toti" speciální formule, a mohou b%t tedy pravdivé nebonepravdivé. Chápeme-li ! jako formuli (podle definice to ale není formule), pak! nem&"e b%t nikdy pravdivá (klauzule je disjunkce a disjunkce je pravdivá,práv! kdy" je pravdiv% aspo( jeden její 'len).(2) Jak uvidíme dále (te) p#edbíháme, ale usnadní nám to pochopení dal-

$ího v%kladu), pracuje Prolog následovn!. Je-li dán logick% program P zadá-liu"ivatel dotaz G (pop#. obecn!ji G1, . . . , Gn), p#eklada' Prologu p#idá k P ne-gaci dotazu, tj. p#idá G, a sna"í se z P, G (to je vlastn! mno"ina formulí)odvodit (tzv. rezolu'ní metodou, viz pozd!ji) spor, tj. odvodit !. Dá se dokázat,"e G sémanticky vypl%vá z P (P |= G), práv! kdy" je z P, G odvoditelná !.Oznámí-li prologovsk% p#eklada' po zadání dotazu G na program P odpov!)Yes, znamená to práv!, "e p#eklada' odvodil z P, klauzuli !.

Poznámka 6.3 Klauzule L1 · · · Ln (Li jsou literály) se v logickém pro-gramování 'asto zapisují jako {L1, . . . , Ln}. Pozor, 'árky zde neznamenají kon-junkce (jak tomu bylo v prologovsk%ch pravidlech, ale disjunkce). Tedy ! sezna'í { }.

56

P#íklad 6.4 Uva"ujme jazyk s unárními rela'ními symboly muz a zena bi-nárními rela'ními symboly otec (“b%t otcem”) a deda (“b%t d!dem”), symbolykonstant (0-ární funk'ní symboly) petr , pavel , jiri , vaclav , milena, jana .Formule muz(petr ), zena(jana), zena(pavel ), zena(pavel), zena(pavel)

zena(milena), zena(pavel) zena(milena), otec(pavel) zena(milena),otec(petr, vaclav), deda(X, Y ) otec(X, Z) otec(Z, Y ) jsou klauzule. Z nichnení zena(pavel ) zena(milena) hornovská (ostatní jsou).Formule zena(pavel) zena(milena), ani otec(X, Z) otec(Z, Y ) deda(X, Y )

klauzule nejsou (pozor, ta druhá je logicky ekvivalentní klauzuli deda(X, Y )otec(X, Z) otec(Z, Y ), ale sama o sob! klauzulí není).

Co jsou to vlastn! hornovské klauzule? Hornovská klauzule je klauzule, kteráobsahuje nejv%$e jeden pozitivní literál. Má tedy jeden z následujících tvar&(dohodn!me se, "e obecn% a existen'ní uzáv!r formule ! budeme zna'it /! a1!; to je sice pon!kud nep#esné, proto"e obecn%ch i existen'ních uzáv!r& m&"eexistovat více; my ale budeme p#edpokládat, "e v$echny volné prom!nné jsouse#azeny, nap#. o'íslováním, tj. volné prom!nné jsou po #ad! X1, . . . , Xm, aobecn%m uzáv!rem rozumíme formuli (/X1 · · · /Xm)! a existen'ním uzáv!remrozumíme (1X1 · · · 1Xm)!):

• (nenulov% po'et negativních literál&, práv! jeden pozitivní literál) AB1 · · · Bn (A, Bi jsou atomické formule); tato klauzule je ekviva-lentní formuli B1 · · · Bn A (Pro'? Uv!domte si, "e B A jeekvivalentní A B a "e (B1 · · · Bn) je ekvivalentní B1· · · Bn.). Tyto klauzule odpovídají prologovsk%m pravidl&m.

• (nulov% po'et negativních literál&, práv! jeden pozitivní literál) A. Tytoklauzule odpovídají prologovsk%m fakt&m.

• (nenulov% po'et negativních literál&, "ádn% pozitivní literál) C1 · · ·Cn (Ci jsou atomické formule); tato klauzule, resp. její obecn% uzáv!r/( C1 · · · Cn) je ekvivalentní formuli (1C1 · · · Cn (Pro'?Uv!domte si, "e (1x)! je ekvivalentní (/x) !). Tyto klauzule odpoví-dají prologovsk%m dotaz&m.

Definice 6.5 Logick! program (n!kdy definitní logick% program) je kone'námno"ina hornovsk%ch klauzulí s jedním pozitivním literálem (tj. klauzulí odpo-vídajících pravidl&m a fakt&m).

Poznámka 6.6 V logick%ch programech se volné prom!nné ve formulích chá-pou jako univerzáln! kvantifikované (to známe z Prologu). Jak je to v$ak sdotazy? Z v%$e uvedeného víme, "e dotaz C1, . . . , Cn na program P se chápejako dotaz, zda P |= C1, . . . , Cn (tj. P |= C1 . . . Cn). Jsou-li ve for-mulích Ci volné prom!nné X1, . . . , Xm, uva"ují se jako existen'n! kvantifiko-vané, tj. dotazujeme se, zda P |= (1X1 · · ·1Xm)C1 . . . Cn (to dob#eznáme z Prologu: z pohledu u"ivatele se ptáme “Existují hodnoty prom!nn%chX1, . . . , Xm pro které C1, . . . , Cn vypl%vá z programu?”). Víme, "e prologovsk%

57

p#eklada' p#evádí tento problém na problém, zda z P negace dotazu, tj. z P a(1X1 · · · 1Xm)C1 . . . Cn, tj. z P (P obsahuje jen fakty a pravidla, a ty

jsou ekvivalentní hornovsk%m klauzulím) a (/X1 · · · /Xm)( C1 · · · Cn),je odvoditeln% spor, tj. klauzule !. Vidíme tedy, "e v$e nakonec vede k hledáníodvození sporu z univerzáln! kvantifikovan%ch hornovsk%ch klauzulí. Hledámetedy odvození sporu z formulí /Hi, kdeHi jsou hornovské klauzule (odpovídajícífakt&m, pravidl&m a dotazu).

Substituce, unifikace S pojmem substituce jsme se setkali p#i v%kladu syn-taxe predikátové logiky. P#ipome(me, "e !(x/s) a t(x/s) ozna'uje formuli aterm, které vzniknou substitucí termu s za prom!nnou x podle uveden%ch pra-videl. V%klad o substitucích nyní pro na$e pot#eby roz$í#íme. Substituce m&-"eme ozna'ovat (x/s) a v dal$ím budeme uva"ovat obecn! i substituce tvaru(x1/s1, . . . , xn/sn) (xi prom!nné, si termy), kde prom!nné xi jsou navzájemr&zné (tj. pro i -= j je xi -= xj) a dále xi -= si. Speciáln!, () ozna'uje tzv. prázd-nou substituci (n = 0, nic se nenahrazuje); pro ni platí !() = ! a t() = t. Substi-tuce budeme ozna'ovat symboly $, $1, . . .. Pro substituci $ = (x1/s1, . . . , xn/sn)bude !$ (pop#. t$) ozna'ovat v%sledek substituce pou"ité na formuli ! (pop#.term t); tento v%sledek vznikne sou'asn%m nahrazením prom!nn%ch x1, . . . , xn

termy s1, . . . , sn podle stejn%ch pravidel jako v p#ípad! !(x/s) (pop#. t(x/s)).Budeme pot#ebovat skládání substitucí. Pro substituce $ a ' budeme sym-

bolem ' 2 $, pop#. jen '$ ozna'ovat substituci, která bude mít následující efekt:!('$) bude formule, která vznikne aplikací substituce $ na formuli vzniklouaplikací substituce ' na !.Pro substituce ' = (x1/s1, . . . , xn/sn) a $ = (y1/t1, . . . , ym/tm) definujeme

substituci '$ jako substituci, která vznikne z

(x1/s1$, . . . , xn/sn$, y1/t1, . . . , ym/tm)

vymazáním (1) xi/si$, pro která xi = si$ a (2) yi/ti, pro která yi ! {x1, . . . , xn}.Lehce se ov!#í následující tvrzení.

Lemma 6.7 Pro substituce ', $, ( platí (1) '() = ()' = '; (2) E('$) = (E')$pro libovolnou formuli, pop'. term, E; (3) ('$)( = '($().

Tedy: Aplikace '$ je ekvivalentní postupné aplikaci ' a (potom) $ (bod (2));substituce je mo"né skládat, p#i'em" nezále"í na po#adí skládání (bod (3)).

Definice 6.8 Substituce $ se naz%vá obecn$j&í ne" substituce ', jestli"eexistuje substituce ( , pro kterou ' = $( .

Tedy: (p#irozen% v%znam) $ je obecn!j$í, proto"e z ní m&"eme dostat ( do-date'n%m “up#esn!ním” ( .

P#íklad 6.9 Viz p#edná$ky.

58

Definice 6.10 Substituce $ se naz%vá unifika%ní substituce (také unifikace)mno"iny {!1, . . . ,!n} formulí (pop#. term&), pokud !i$ = !j$ pro libovolnéi, j ! {1, . . . , n}. Tedy, unifikace je substituce, pop její" aplikaci p#ejdou v$echnyformule !i ve stejnou formuli.

P#íklad 6.11 Viz prednasky

Definice 6.12 Unifikace $ mno"iny {!1, . . . ,!n} se naz%vá nejobecn$j&í un-fikací (zkratka mgu z anglického “most general unifier”) této mno"iny, jestli"eje obecn!j$í ne" ka"dá jiná unifikace mno"iny {!1, . . . ,!n}.

Poznámka 6.13 mgu neni urcen jednoznacne

P#íklad 6.14 Viz p#edná$ky.

Unifika!ní algoritmus V dal$ím naz%váme jednoduch%m v%razem term neboatomickou formuli. Cílem je najít k dané mno"in! jednoduch%ch v%raz& nejo-becn!j$í unifikaci.Pro kone'nou mno"inu S jednoduch%ch v%raz& nazv!me její rozdílovou mno-

$inou následovn! definovanou mno"inu: Najdi první pozici i zleva, na které ne-mají v$echny v%razy z S stejn% symbol; podv%razy v$ech v%raz& z S, kteréza'ínají na pozici i tvo#í rozdílovou mno"inu mno"iny S.

P#íklad 6.15 Treba z Lloyda

Popí$eme základní algoritmus pro hledání nejobecn!j$í unifikace dané mno-"iny S jednoduch%ch v%raz&. Pro S = {E1, . . . , En} ozna'me S$ = {E1$, . . . , En$}.Algoritmus hledání mgu dané kone'né mno"iny S jednoduch%ch v%raz&:

1. k := 0; $0 := ().

2. Je-li S$k jednoprvková, zastav; $k je hledan% mgu mno"iny S. Jinak najdirozdílovou mno"inu Dk mno"iny S$k.

3. Existují-li v Dk term t a prom!nná x, která se nevyskytuje v t, polo"$k+1 := $k(x/t); k := k + 1; jdi na 2. Jinak zastav, S není unifikovatelná.

P#íklad 6.16 Treba z Lloyda.

Poznámka 6.17 Tento algoritmus m&"e mít vysokou 'asovou slo"itost. Jsouznámy algoritmy s lineární 'asovou slo"itostí. Ve v!t$in! implementací Prologuje v$ak implementována modifikace v%$e uvedeného algoritmu, která spo'ívá vevynechání testu v%skytu x v t (viz algoritmus). To v$ak m&"e vést k nesprávn%mv%po't&m.

59

Obecná rezolu!ní metoda Popí$eme nyní tzv. obecnou rezolu'ní metodunavr"enou v 60. letech 20. stol. Robinsonem. Základem je tzv. rezolu'ní odvozo-vací pravidlo, které ze dvou klauzulí odvodí jinou klauzuli, jejich tzv. rezolventu.Obecn% tvar rezolu'ního pravidla je

z klauzule {L1, . . . , Li#1, A, Li+1, . . . , Ln}a klauzule {L"

1, . . . , L"i#1, A", L"

i+1, . . . , L"m}

odvo) klauzuli (tzv. rezolventu v%$e uveden%ch klauzulí)

{L1$, . . . , Li#1$, Li+1$, . . . , Ln$, L"1$, . . . , L

"i#1$, L

"i+1$, . . . , L

"m$},

je-li $ mgu mno"iny {A, A"}.

P#itom jsou Li, L"j literály a A a A" jsou atomické formule.

Poznámka 6.18 Rezolu'ní pravidlo je svou povahou odvozovací pravidlo vestejném duchu jako pravidla, se kter%mi jsme se setkali: z n!jak%ch formulíodvodí jinou formuli. Pravidlo MP lze chápat jako speciální p#ípad rezolu'níhopravidla: Pravidlo MP #íká “z A a A B odvo) B”. Formule A B jeekvivalentní klauzuli A B. Tedy odvození pomocí MP odpovídá odvození{B} z { A, B} a {A}. To lze pomocí rezolu'ního pravidla s unifikací, za kterouvezmeme identickou (prázdnou) substituci.

P#íklad 6.19 Vymyslete p#íklady na rezolu'ní odvození (1) kdy pravidlo nejdealpikovat, (2) kdy jde jedinym zpusobem, (3) kdy jde vice zpusoby, (4) odvozeníprázdné klauzule.

Pro danou mno"inu F klauzulí ozna'me

R(F ) = {C | C je rezolventou n!jak%ch klauzulí z F}.

Dále definujme R0(F ) = F a Rn+1(F ) = Rn(F )'R(Rn(F )). Tedy Rn(F ) jenmo"ina klauzulí odvoditeln%ch z F nejv%$e n-násobn%m pou"itím kroku “utvo#v$echny mo"né rezolventy”.Základní v%sledek popisující rezolu'ní metodu:

V$ta 6.20 Mno$ina F klauzulí je sporná, práv& kdy$ existuje n tak, $e ! !Rn(F ).

Poznámka 6.21 Spornost F je t#eba chápat jako spornost v d#íve uvedenémaxiomatickém systému (tj. "e z F je dokazatelná libovolná formule). Víme v$ak,"e F je sporná, práv! kdy" nemá "ádn% model. Nepot#ebujeme se tedy na axi-omatick% systém odvolávat a vysta'íme se sémantick%mi pojmy.

SLD-rezoluce Víme, "e v Prologu je po zadání dotazu G cílem p#eklada'ezjistit, zda z programu P dotaz G plyne, tj. zda P |= G. Víme, "e P |= G,práv! kdy" P, G je sporná (viz . . . odkaz). Podle V!ty 6.20 je zji$t!ní spornosti

60

P, G ekvivalentní (nebo+ v$echny vyskytující se formule jsou klauzule) zji$t!ní,zda ! pat#í do n!jakého Rn(F ). V%po'et Rn je v$ak obecn! náro'n% a nijaknevyu"ívá speciální formu klauzulí pou"ívanou v Prologu (hornovské klauzule).Cílem následujícího textu je ukázat speciální formu rezolu'ní metody, tzv. SLD-rezoluci.V následujcím ozna'uje P kone'nou mno"inu hornovsk%ch klauzulí, které od-

povídají fakt&m a pravidl&m (tzv. programové klauzule, tj. hornovsk%ch klauzulís jedním pozitivním literálem; takové mno"in! se #íká logick% program, pop#.definitní logick% program); G ozna'uje hornovskou klauzuli, která odpovídá ne-gaci u"ivatelem zadaného cíle ? 3 G1, . . . , Gn, tzv. cílová klauzule, tj. klauzuli

G1 · · · Gn.

Definice 6.22 Odpov$' pro P'{G} je libovolná substituce $ = (x1/t1, . . . , xm/tm),kde ka"dá prom!nná xi se vyskytje v G.

Definice 6.23 Odpov!) $ pro P ' {G} se naz%vá korektní , jestli"e formule/((G1 · · · Gn)$) sémanticky plyne z P .

To je základem deklarativní sémantiky logického programu P (je ji mo"néchápat jako mno"inu v$ech G spolu s $, kde $ je korektní odpov!) pro P ' {G};tj. Decl(P ) = {"?3 G1, . . . , Gn, $# | $ je korektní odpov!) pro P ' {G}}).To souvisí s odpov!)mi Prologu následovn!: Prolog odpoví na dotaz ? 3

G1, . . . , Gn bu) Yes se substitucí $ (ta m&"e b%t prázdná, a pak ji Prolog nevy-pisuje), nebo No. Odpov!) Yes se substitucí $ je korektní, jestli"e $ je korektníodpov!) pro P ' {G} v práv! definovaném smyslu. Odpov!) No je korektní,jestli"e /((G1 · · · Gn)$) sémanticky neplyne z P pro "ádnou $.Pokou$íme-li se aplikovat rezolu'ní pravidlo na klauzule, z nich" jedna od-

povídá cíli (nemá "ádn% pozitivní literál) a druhá odpovídá pravidlu nebo faktu(má práv! jeden pozitivní literál A), u" se nepot%káme s následujícím nede-terminismem implicitn! obsa"en%m v obecném rezolu'ním pravidle: z podstatyrezolu'ního pravidla je jasné, "e v cíli hledáme takov% Gi, kter% je mo"né uni-fikovat s A (tedy nevybíráme dvojice atomick%ch formulí mající unifikaci jakov obecné rezolu'ní metod!, ale jen atomické formule, které jsou unifikovatelnés A).

Definice 6.24 Nech+ P a G jsou jako v%$e (logick% program a klauzule odpo-vídající cíli). SLD-odvození z P ' {G} je posloupnost H0 = G, H1, . . . cílo-v%ch klauzulí, posloupnost C1, C2, . . . variant programov%ch klauzulí z P (tj. Ci

vzniknou z klauzulí z P p#ejmenováním prom!nn%ch) a posloupnost $1, $2, . . .unifikací takov%ch, "e $i+1 je mgu mno"iny {Hi, Ci+1} a Hi+1 je odpovídajícírezolventou (tj. vznikne pou"itím rezolu'ního pravidla na Hi a Ci+1 p#i $i+1).SLD-odvození se naz%vá zamítnutí (refutace) délky n, jestli"e jeho poslednícílová klauzule je Hn = !.

Poznámka 6.25 To je základem tzv. procedurální sémantiky. SLD-odvozeníodpovídá v%po'tu prologovského p#eklada'e. Souvislost s prologovsk%m zásob-níkem (tém!# z#ejmá, stav zásobníku odpovídá SLD-odvození).

61

Odvození m&"e refutací (úsp!$né); nekone'né (neúsp!$né 1); kone'né nekon-'ící !, které nelze dále prodlou"it (neúsp!$né 2).

Definice 6.26 Vypo%ítaná odpov$' pro P ' {G} je substituce $, pro kte-rou existuje refutace z P ' {G} délky n s odpovídající posloupností $1, . . . , $n

takovou, "e $ vznikne z $1 · · · $n (slo"ení substitucí) vynecháním t!ch x/t, prokteré se x nevyskytuje v G.

V$ta 6.27 (korektnost SLD-rezoluce) Ka$dá vypo(ítaná odpov&* pro P '{G} je korektní odpov&dí pro P ' {G}.

Poznámka 6.28 Obsahov! odpovídá v!t! o korektnosti, . . .

V$ta 6.29 (úplnost SLD-rezoluce; odpov$* Yes) Pro cíl ?3G1, . . . , Gn aprogram P platí, $e jestli$e 1(G1 · · · Gn) sémanticky plyne z P , pak existujerefutace z P ' {G}.

Poznámka 6.30 Odpovídá v!t! o úplnosti: Jestli"e to sémanticky plyne, pakto lze prokázat syntakticky (refutací).

V$ta 6.31 (úplnost SLD-rezoluce; odpov$* Yes se substitucí) Pro ka$-dou korektní odpov&* $ pro P '{G} existuje vypo(ítaná odpov&* ' pro P '{G},která je (jako substituce) obecn&j%í ne$ $ (tj. $ = '( pro n&jakou substituci ().

Poznámka 6.32 P#e't!me to znovu, podrobn!ji: Jestli"e pro cíl ?3G1, . . . , Gn

a program P platí, "e 1(G1 · · · Gn) sémanticky plyne z P se substitucí $,pak to lze prokázat syntakticky refutací, která v sob! má substituci obecn!j$íne" $.

Sjednocující pohled: U"ivatelsk% pohled na PROLOG je zalo"en na dekla-rativní sémantice (sémantické vypl%vání); programátorsk% pohled je zalo"en narezolu'ním zásobníku (tak je hledání odpov!di, tj. hledání refutace se substi-tucí, tj. hledání d&kazu) implementováno; logick% pohled je zalo"en na rezo-lu'ní metod!, spec. SLD-rezoluci. V%$e uvedené v%sledky ukazují souvislostimezi jednotliv%mi pohledy. P#edev$ím: Sémantické vypl%vání je p#irozené z hle-diska intuitivního pochopení, co prologovsk% p#eklada' hledá, jak% je v%znamodpov!di. Nedává v$ak návod, jak hledání odpov!di implementovat. Toto hle-dání lze v principu realizovat hledáním d&kazu v axiomatickém systému, kter%byl uveden v základním v%kladu o predikátové logice. Takové hledání je v$ak p#í-li$ náro'né (“p#íli$ nedeterministick%” pojem d&kazu v axiomatickém systému,tento pojem není primárn! vhodn% pro hledání d&kazu). Proto byla navr"enarezolu'ní metoda, která je je$t! vhodn!j$í v p#ípad! SLD-rezoluce (viz v%$epopsan% efekt hornovskosti klauzulí: v cílové klauzuli jsou v$echny literály ne-gativní, jedin%m literálem, kter% je mo"né unifikovat v programové klauzuli jetedy jedin% pozitivní literál).Pozor: Úplnost #íká, "e má-li b%t odpov!) Yes, pak tato odpov!) vypo'í-

tatelná. To ale neznamená, "e ji Prolog v"dy najde — p#eklada' prohledává

62

podle algoritmu zásobníku, tj. hledá mo"né d&kazy a m&"e se rozb!hnout ponekone'né v!tvi. Prohledává toti" strom mo"n%ch #e$ení do hloubky (p#i tomvyu"ívá o'íslování formulí). To v$ak není tím, "e bychom zatím $patn! hledalia p#íslu$n% algoritmus, kter% refutující v%po'et v"dy najde, je$t! neobjevili. Jeto jen jeden z projev& jednoho ze základních v%sledk& vy'íslitelnosti: prediká-tová logika je nerozhodnutelná (problém: ”zjisti, zda je formule tautologií” jenerozhodnuteln%, pota"mo pak problém logického vypl%vání). Tato situace jeanalogická situaci, která je více známá, toti" ta, "e musíme 'elit NP-úplnostin!kter%ch problém&. Nejde se jim vyhnout, musíme pou"ít heuristiky. Krásav%sledk& teoretické informatiky a logiky spo'ívá v tom, "e tyto principiální v!cinám sd!lují (jinak bychom t#eba marn! hledali efektivní algoritmy, které neexis-tují). Z tohoto pohledu je tedy algoritmus prologovského p#eklada'e heuristikou'elící nerozhodnutelnosti problému, kter% nás zajímá (”p#edpokládám-li znalostiv databázi, plyne z nich m&j dotaz?”).V$imn!me si dále v%znamu o'íslování formulí v prologovském programu,

které pou"ívá algoritmus prologovského zásobníku. Z pohledu vysv!tlené SLD-rezoluce spo'ívá v%znam o'íslování v tom, "e odstra(uje nedeterminismus vkroku, ve kterém je t#eba vybrat programovou klauzuli k unifikaci. Zatímco vSLD-rezoluci je p#ipu$t!na libovolná mo"ná programová klauzule, algoritmusprologovského zásobníku #íká, "e se pou"ije ta mo"ná s nejmen$ím 'íslem.

7 Dodatek: Pot"ebné pojmy a v!sledkyObsah dodatku nebude u zkou$ky po"adován.

Formální jazyky Abeceda je libovolná kone'ná mno"ina symbol&. Slovo naddanou abecedou je libovolná kone'ná posloupnost symbol& této abecedy. Uva-"ujeme také tzv. prázdné slovo (ozna'ujeme ho )), tj. slovo neobsahující "ádn%symbol. (z#et!zení, podslovo, . . .) Mno"inu v$ech slov nad abecedou , se zna'í,!. Jazyk na danou abecedou je libovolná mno"ina slov této abecedy. (DODE-LAT)

Algebry (Univerzální) algebra je . . . (DODELAT), podalgebra

Strukturální indukce

V$ta 7.1 (princip strukturální indukce) Nech# A je algebra, B její podal-gebra generovaná mno$inou C . A. Chceme-li dokázat, $e v%echny prvky algebryB mají vlastnost V, sta(í ukázat, $e

(1) v%echny prvky z C mají vlastnost V;

(2) mají-li prvky b1, . . . , bn ! B vlastnost V, pak vlastnost V má také prvekf(b1, . . . , bn) pro ka$dou n-ární operaci f algebry A.

63

D̊ukaz. Ozna'me DV mno"inu obsahující ty prvky mno"iny B, které mají vlast-nost V , tj. DV = {b ! B | b má V}. Proto"e C . B, plyne z (1) C . DV . Z(2) plyne, "e DV je uzav#ená na operace algebry A, a tedy B . DV (nebo+B je podle p#edpokladu generovaná mno"inou C, tj. je nejmen$í podmno"inoumno"iny A, která obsahuje C a je uzav#ená na operace algebry A). D&kaz jehotov. !

8 Dodatek: Neformální logika

Reference[1] Jakákoli u'ebnice matematické logiky bude vhodn%m studijním pramenem.

[2] Kolá# J., Chytil M., 1t!páknová O.: Logika, algebry a grafy. SNTL, Praha,1989 (dostupná v knihovnách, u'ebnice pro V1 technické).

[3] Lloyd J. W.: Foundations of Logic Programming. Springer, 1984.

[4] Sochor A.: Klasická matematická logika. Karolinum, Praha, 2001 (v prodeji,velmi dob#e psaná s #adou dopl(ujících informací).

[5] Sterling L., Shapiro E.: The Art of Prolog. MIT Press, 1986.

[6] 1vejdar V.: Logika, neúplnost a slo"itost. Academia, Praha, 2002.

64