Doc. RNDr. Luděk Cienciala, Ph.D. U" vod do logiky Skripta do předmětu Ústav informatiky Filozoficko-přírodovědecká fakulta v Opavě Slezská univerzita v Opavě Opava 2020 doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 2 OBSAH: 1 ÚVOD DO LOGIKY ......................................................................................................................3 2 VÝROKOVÁ LOGIKA .................................................................................................................6 3 SÉMANTIKA VÝROKOVÉ LOGIKY......................................................................................15 3.1 Tabulková metoda interpretace formule .............................................................................16 4 NORMÁLNÍ FORMY VÝROKOVÝCH FORMULÍ...............................................................23 5 SPLNITELNOST A PLATNOST, LOGICKÝ DŮSLEDEK ...................................................32 5.1 Rozhodování pomocí sémantického stromu ........................................................................33 5.2 Quineův algoritmus................................................................................................................35 5.3 Reductio ad absurdum...........................................................................................................36 5.4 Tablová metoda......................................................................................................................37 5.5 Dedukce ve výrokové logice ..................................................................................................39 6 REZOLUČNÍ PRINCIP...............................................................................................................46 7 AXIOMATICKÝ SYSTÉM VÝROKOVÉ LOGIKY...............................................................54 7.1 Formální systém Gentzenova typu .......................................................................................57 7.2 Gentzenovský formální systém výrokové logiky.................................................................66 8 PREDIKÁTOVÁ LOGIKA 1. ŘÁDU.........................................................................................70 8.1 Sémantika PL1 – interpretace formulí.................................................................................75 9 AUTOMATICKÉ DOKAZOVÁNÍ V PREDIKÁTOVÉ LOGICE (OBECNÁ REZOLUČNÍ METODA) ........................................................................................................................................84 10 SÉMANTICKÉ TABLO, AXIOMATICKÝ SYSTÉM PREDIKÁTOVÉ LOGIKY ........100 10.1 Rozhodování splnitelnosti formulí sémantickými tably .................................................100 10.2 Formální systém (logický kalkul) Hilbertova typu .........................................................103 10.3 Gentzenovský axiomatický systém ...................................................................................106 11 TRADIČNÍ ARISTOTELOVA LOGIKA..............................................................................111 12 KLASIFIKACE ZDROJŮ .......................................................................................................115 31 Úvod do logiky doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 1 ÚVOD DO LOGIKY ČAS POTŘEBNÝ KE STUDIU Celkový doporučený čas k prostudování KAPITOLY je 90 minut. RYCHLÝ NÁHLED DO PROBLEMATIKY KAPITOLY ÚVOD DO LOGIKY Cílem prvního a druhého modulu je uvedení do problematiky logiky, výrokové logiky, naučit používat výrokové spojky, naučit pracovat s výrokovými formulemi, převádět z přirozeného jazyka do symbolického jazyka výrokové logiky. Rychlý ná- hled KLÍČOVÁ SLOVA KAPITOLY ÚVOD DO LOGIKY Logika, druhy logik, logické vyplývání, analytická pravdivost, sporná množina výroků, důkaz tvrzení Klíčová slova Existuje mnoho typů logik, například: Formální logika, matematická logika, modální logika (popis dynamického chování systému), dvouhodnotová, vícehodnotová logika, pravděpodobnostní logika, temporální (uvažuje pravdivost či nepravdivost v čase, disponuje prostředky pro vyjádření pojmů vždy nebo někdy) atd. Termín logika často vyskytuje i v běžné řeči v rozmanitých slovních spojeních jako „to nemá žádnou logiku, neúprosná logika vývoje, ženská logika, logika věci vyžaduje, aby.... „apod. Odkud termín logika vlastně pochází? Evangelista sv. Jan jedné ze svých kapitol praví, že na počátku bylo Slovo (řecky logoz), tedy jazyk, myšlení, uvažování, ale též řád věcí. Logika se pokouší k objektům a pochodům lidského myšlení vytvořit adekvátní model pomocí určitých sobě vlastních prostředků. (stejně jako matematika nebo matematická informatika.) Model se vytváří na základě určitého zjednodušení (abstrakce) modelované reality, a to tak, aby vněm bylo obsaženo to nejdůležitější. Za zakladatele logiky a to logiky formální je považován Aristoteles. Formální logika je nejstarší pokus o modelování a modelové zkoumání zákonitostí vnímání a usuzování. Jde o logiku založenou na dvouhodnotové interpretaci pojmu pravdivosti. Tvrzení může být buď pravdivé nebo nepravdivé. Logika je především věda o správném usuzování, o umění správné argumentace. Logika doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 4 Obecně můžeme úsudek charakterizovat následujícím schématem: Na základě pravdivosti výroků (soudů, tvrzení) V1, …., Vn soudím, že je pravdivý rovněž výrok V. (pozn. předpoklady = premisy) Úsudek Existují různé druhy úsudků – ne všemi se zabývá logika. Obecně se nezabývá tzv. pravděpodobnostními úsudky: Slunce doposud vyšlo každý den. Tedy: Slunce (pravděpodobně) vyjde i zítra. Nezabývá se úsudky generalizací: Všechny labutě, které jsme dosud viděli, jsou bílé. Tedy: Všechny labutě jsou bílé. Budeme se zabývat tzv. deduktivními úsudky: DEFINICE 1-1 LOGICKÉ VYPLÝVÁNÍ Úsudek P1, …., Pn / Z je deduktivně správný (platný), značíme P1, …Pn ⊨Z, jestliže závěr Z logicky vyplývá z předpokladů P1, ….Pn, tj. za všech okolností takových že jsou pravdivé všechny předpoklady P1, …., Pn je ( za těchto okolností) pravdivý i závěr Z. Tedy jinými slovy: Za žádných okolností, nikdy se nemůže stát, aby byly všechny předpoklady P1, … , Pn pravdivé a zároveň závěr Z byl nepravdivý. Deduktivní usuzování v praktickém životě všichni více či méně používáme. Např. Víme, že všechny muchomůrky zelené jsou prudce jedovaté a zjistíme (např. za pomoci atlasu hub), že houba, kterou jsme nalezli, je muchomůrka zelená, pak jistě nebudeme tuto houbu ochutnávat a spolehneme se na logiku, neboť to nám zaručuje, že houba, kterou jsme našli, je prudce jedovatá. Nyní uvedeme příklady jednoduchých, správných deduktivních úsudků: • Všechny kovy se teplem roztahují. Měď je kov. Měď se teplem roztahuje. • Je doma nebo odešel do kavárny. Je-li doma, pak nás očekává. Jestliže nás neočekává, pak odešel do kavárny. • Všechny muchomůrky zelené jsou prudce jedovaté. Tato tužka je muchomůrka ze- lená. Tato tužka je prudce jedovatá. • Všichni muži mají rádi fotbal a pivo. Někteří milovníci piva nemají rádi fotbal. Pepa má rád pouze milovníky fotbalu a piva. Některé ženy nemá Pepa rád. Logika také zkoumá skladbu – konstrukci jednotlivých složených výrazů (soudů) z jejich podvýrazů. Jednou z disciplín logiky je proto rovněž tzv. logická analýza jazyka – spočívá v nalezení příslušné logické konstrukce vyjádřené daným výrazem. Logická analýza ja- zyka 51 Úvod do logiky doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Ovšem ne všechny deduktivně správné úsudky můžeme ověřit pomocí daného logického systému. Proto hovoříme o expresivní síle logického systému, která je dána tím, do jaké míry podrobnosti můžeme analyzovat jednotlivé výrazy. Ideální logický systém by nám měl umožnit analyzovat premisy do takové hloubky, abychom mohli odvodit všechny závěry, které z těchto premis logicky vyplývají a ověřit všechny správné úsudky. Expresivní síla Uvedeme příklady logických systémů podle jejich expresivní síly: • Výroková logika umožňuje analyzovat pouze do úrovně elementárních výroků, jejichž strukturu již dále nezkoumá. • Predikátová logika 1. řádu umožňuje analyzovat elementární výroky do úrovně vlastností jednotlivých objektů zájmu (tzv. individuí – prvků univerza diskursu) a jejich vztahů. • Predikátové logiky vyšších řádů umožňují navíc analyzovat vlastnosti vlastností, vlastností funkcí, atd. Jaké jsou vlastnosti deduktivních úsudků? Ověříme-li správnost (platnost) úsudku, nedokážeme tím pravdivost závěru! Vlastnosti deduktiv- ních úsudků První vlastností je, že platný úsudek může mít nepravdivý závěr. Uvedeme příklad: Je doma nebo odešel do kavárny. Je-li doma, pak nás očekává. Jestliže nás neočekává, pak odešel do kavárny. Správnost úsudku nedokazuje, že dotyčný je v kavárně, jestliže nás neočekává, klidně mohl jít třeba do kina. V tom případě by ovšem zřejmě nebyla pravdivá první premisa. To neznamená, že platný úsudek, jehož závěr není pravdivý, by byl bezcenný. Vždyť takovýto způsob běžně používáme, chceme-li demonstrovat, že někdo neříká pravdu. Představme si následující dialog: Vy tedy tvrdíte, že X1, ….Xn. Avšak z vašich tvrzení plyne, že A. Z A dále plyne, že B atd. až dostaneme závěr Z, který je evidentně nepravdivý. Tedy vy tvrdíte Z, což není pravda. Proto alespoň jedno z vašich původních tvrzení Xi není pravdivé. První vlastnost Druhou vlastností deduktivních úsudků je monotónnost: Jestliže P1, …..Pn ⊨ Z, pak P1, …Pn, Pn+1 ⊨ Z, pro libovolnou další premisu Pn+1. Tuto vlastnost nemají jiné úsudky, které nejsou deduktivní. Druhá vlastnost Třetí vlastností je tranzitivita: Jestliže P1, …..Pn ⊨ Z a Q1, …..Qm , Z ⊨ Z´, pak P1, …..Pn, Q1, …..Qm ⊨ Z´ a čtvrtou reflexivita: Je-li B rovna jedné z premis P1, …..Pn, pak P1, …..Pn ⊨ B. Třetí a čtvrtá vlastnost Nyní definujeme analytickou pravdivost a kontradikci. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 6 DEFINICE 1-2 ANALYTICKÁ PRAVDIVOST Výrok V je analyticky pravdivý, značíme ⊨ V, je-li pravdivý za všech okolností, vždy. (Množina předpokladů je prázdná, V nemůže být nepravdivý.) DEFINICE 1-3 SPORNÁ MNOŽINA Množina { P1, …..Pn} výroků je sporná (kontradiktorická, nesplnitelná) jestliže nemůže nikdy za každých okolností nastat případ, že by byly všechny P1, …..Pn pravdivé, značíme P1, …..Pn ⊨ (Tedy z této množiny logicky vyplývá jakýkoli výrok, i nepravdivý, proto musí být vždy alespoň jeden Pi nepravdivý) Důležitou vlastností je, že ze sporné množiny předpokladů vyplývá jakýkoli závěr. Všechny pravdivé matematické výroky jsou analyticky pravdivé. Matematikové formulují a dokazují tvrzení. Výsledkem jejich práce je tedy zpravidla (ne-li vždy) nalezení nějakého důkazu. Avšak důkazy a jejich analýza je to, co zajímá logiky, důkaz je rovněž jedním z nejdůležitějších logických pojmů. Co je to důkaz? Obecně řečeno, důkaz tvrzení A z předpokladů P1,…,Pn je posloupnost tvrzení B1,…,Bm taková, že: Bm = A pro každé i £ m platí, že Bi je buď jeden z předpokladů Pj nebo Bi vznikne z předchozích B1,…,Bi-1 uplatněním nějakého odvozovacího pravidla. Důkaz 2 VÝROKOVÁ LOGIKA ČAS POTŘEBNÝ KE STUDIU Celkový doporučený čas k prostudování KAPITOLY je 90 minut. KLÍČOVÁ SLOVA KAPITOLY VÝROKOVÁ LOGIKA Logika-výroková logika-jazyk výrokové logiky-spojky výrokové logiky. Klíčová slova 72 Výroková logika doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Výrok je jazykový výraz, o němž má smysl prohlásit, zda je pravdivý či nepravdivý. Výrok Ne každá věta vyjadřuje výrok. Např. věta Český král je holohlavý nemůže být v současné době (kdy neexistuje český král) ani pravdivá, ani nepravdivá. Kdyby totiž nastal jeden z těchto případů, vyplývala by z ní existence českého krále! Výroky dělíme na jednoduché (elementární, atomické), které nelze dále rozložit na výroky jednodušší, jsou to tvrzení, jehož žádná vlastní část již není výrokem a složené, které mají vlastní části – výroky. Nyní uvedeme příklady jednotlivých typů výroků: "Koupím si telefon, o němž si předtím přečtu recenzi." Jedná se o jednoduchý výrok. "Když si jdu koupit telefon, tak si nejprve projdu pár recenzí." Jde o výrok složený, který lze rozložit na dva jednoduché výroky A a B, kde A = "jdu si koupit telefon" a B = "nejprve si projdu pár recenzí". Jednoduché výroky jsou spojeny logickou spojkou implikace, která je zde zastoupena slovním spojením "když ..., tak". "Není pravda, že jak telefon vypadá charakterizuje, to co umí." Jedná se o složený výrok, ale netvoří ho dva výroky jako v předešlém případě, ale jen jeden jednoduchý výrok A (A = "jak telefon vypadá charakterizuje to co umí "), u kterého je použita logická spojka negace. "Je pravda, že čtení knih zvyšuje slovní zásobu a rozvíjí čtenářovu fantazii." Jedná se o složený výrok tvořený dvěma jednoduchými výroky A a B (A = "čtení knih zvyšuje slovní zásobu" a B = "čtení knih rozvíjí čtenářovu fantazii") spojenými logickou spojkou konjunkce (vyjádřenou spojkou přirozeného jazyka - "a"). Výroková logika zkoumá způsob skládání jednoduchých výroků pomocí logických spojek do výroků složených. Jednoduché výroky vstupují do spojení pouze svou pravdivostní hodnotou a jsou navzájem nezávislé. Pravdivostní hodnota složeného výroku je tedy jednoznačně určena pravdivostními hodnotami jeho složek a druhem spojek, které tyto jednodušší složky spojují. V matematických textech výrok tvaru „jestliže A, pak B“ bývá vyjadřován některým z těchto způsobů: A je podmínka postačující pro B B je podmínka nutná pro A Případně Aby B, k tomu stačí, že A Aby A, k tomu je nutné, aby B. Sledujme pravdivost. „Gen je biologická struktura.“ Je pravdivý výrok. „Gen není biologická struktura.“ Je nepravdivý výrok. „Na Marsu je život.“ „Ve vesmíru existuje život i mimo Zemi.“ Míra přesvědčení o pravdivosti věty „Na Marsu je život.“ klesá, u věty „Ve vesmíru existuje život i mimo Zemi.“ doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 8 roste např. díky kosmickým výzkumům. Poslední dvě věty jsou pravdivé, nebo nepravdivé, ale naše prostředky, jak zjistit jejich pravdivostní hodnotu, nejsou dostatečně silné. „Život je pravoúhlý.“ „Pravoúhlý život je když.“ Věta „Pravoúhlý život je když.“ není dobře sestavená, její skladba neodpovídá pravidlům skladby českého jazyka, nemá tudíž smysl cokoli říkat o její pravdivosti či nepravdivosti. Věta „Život je pravoúhlý.“ je sice gramaticky správná, avšak zjevně nesmyslná vzhledem k vadnému použití predikátu pravoúhlý. Zde nemá smysl uvažovat o její pravdivosti či nepravdivosti. Věta „Pravoúhlý život je když.“ odporuje syntaxi, zatímco věta „Život je pravoúhlý.“ sémantice českého jazyka. V syntaxi jazyka výrokové logiky je stanoveno, jakých symbolů abecedy jazyk používá a jsou předepsána pravidla zřetězování symbolů abecedy jazyka do útvarů zvaných formule jazyka. Jde tedy o soustavu syntaktických pravidel, umožňující konstruovat jistá zřetězení symbolů jazyka, která jsou jeho dobře utvořenými formulemi a patří proto do jeho slovníku. Syntaxe jazyka Nyní definujeme abecedu jazyka výrokové logiky. DEFINICE 2-1 ABECEDA JAZYKA VÝROKOVÉ LOGIKY Mezi symboly abecedy jazyka výrokové logiky patří výhradně do některé z následujících skupin elementárních symbolů: • symboly a, b, c, ….a1, b1, c1 …. pro prvotní proměnné označující elementární výroky • symboly pro logické konstanty true a false, • symboly pro logické spojky: negace ¬, konjunkce &, disjunkce Ú, implikace ®, ekvivalence «, • pomocné symboly - závorky. Syntax jazyka výrokové logiky vychází z množiny symbolů • a, b, c, ….a1, b1, c1 označujících výroky • true a false. Uvedené symboly představují atomické formule, ze kterých se vytvářejí další dobře utvořené výrokové formule podle pravidel. Definujme pravidla pro tvorbu formulí výrokové logiky. Základní pravidlo – báze: Každá atomická formule je formulí. Indukce: Jsou-li X a Y formule, pak ùX, X&Y, XÚY, X®Y a X«Y jsou formule. Generalizace: všechny dobře utvořené formule jazyka výrokové logiky jsou výsledkem konečného počtu aplikací základního pravidla a pravidla indukce. Poznamenejme, že X a Y zastupují libovolné formule, jsou to metasymboly sloužící k označení formulí. Pravidla pro tvorbu formulí Příkladem formule může být: )( CBA Ú® 92 Výroková logika doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Výrazy, které nejsou formulemi: Jazyk výrokové logiky je množina všech formulí výrokové logiky. V následující tabulce uvádíme alternativní označení výrokových spojek. Jazyk výrokové logiky Symbol pro spojku Alternativní Symboly & Ù ® É, Þ « º, Û Budeme používá následující konvence. Složenou formuli nejvyššího řádu netřeba závorkovat. Logické spojky uspořádáme do prioritní stupnice ¬, &, Ú, ®, «. Ze dvou funktorů váže silněji ten, který je v uvedené stupnici umístěn více vlevo. Tuto konvenci však příliš ”nezneužíváme” a závorky raději použijeme vždy, když chceme vyznačit strukturu formule. V případě, že o prioritě vyhodnocení nerozhodnou ani závorky ani prioritní stupnice, vyhodnocujeme formuli zleva doprava. např. formuli p ® q ® r ® s vyhodnocujeme tak, jako by byla zapsána ((p ® q) ® r) ® s. U vícečlenných konjunkcí nebo disjunkcí není třeba (vzhledem k jejich asociativitě – viz dále) uvádět závorky, např. místo (p Ú q) Ú r nebo p Ú (q Ú r) lze psát pouze p Ú q Ú r. Tato konvence souvisí s předchozí konvencí na pořadí vyhodnocování nezáleží, a tedy lze standardně vyhodnocovat zleva doprava. Podle definice S využitím konvencí Hier.řád p, q p, q 0 (¬p), (¬q), (p & q) ¬p, ¬q, p & q 1 ((¬p) Ú (¬q)), (¬(p & q)) ¬p Ú ¬q, ¬(p & q) 2 (((¬p) Ú (¬q)) « (¬(p & q))) ¬p Ú ¬q « ¬(p & q) 3 V předchozí tabulce v prvním sloupci je zobrazen postup konstrukce složené formule striktně podle definice, ve druhém s maximálním využitím konvencí šetřících závorky, v třetím sloupci je uveden hierarchický řád formulí uvedených v daném řádku. Podformule definujeme jakou souvislou část formule, která je sama formulí. Každá formule je svou podformulí. Chceme-li hovořit o podformulích, které jsou různé od původní formule, používáme termín vlastní podformule. Podfor- mule Konstrukci formule lze vyjádřit i graficky pomocí tzv. formačního stromu formule. ))(, CBAA ®Ú¬¬ doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 10 DEFINICE 2-2 FORMAČNÍ STROM FORMULE Formační strom formule A jazyka výrokové logiky je konečný binární strom, jehož všechny uzly jsou označeny návěstími – podformulemi formule A – tak, že platí: • Kořen má 0-tou úroveň a je označen formulí A. • Jestliže je uzel označen některým z návěstí X & Y, X Ú Y, X ® Y, X «Y, kde X, Y jsou formule, pak uzly bezprostředně následující úrovně nesou po řadě (zleva doprava) návěstí X, Y. • Je-li uzel označen podformulí ¬X, pak uzel bezprostředně následující úrovně nese jako návěstí podformuli X. Listy jsou označeny atomickými formulemi vyskytujícími se v A. VĚTA 2-1 Ke každé výrokové formuli existuje jediný odpovídající formační strom. Uvedeme příklad formačního stromu k formuli Vzájemné jednoznačné přiřazení dobře utvořené výrokové formule a jejího formačního stromu umožňuje definovat vedle složitosti konstrukce formule také její hloubku a zá- kladnu. ( )( ) ( )( )rsprqp ®Ù¬®®Ú 112 Výroková logika doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky DEFINICE 2-3 HLOUBKA FORMULE Hloubka formule je hloubkou formačního stromu. DEFINICE 2-4 ZÁKLADNA FORMULE Základnu formule tvoří množina atomických formulí, které jsou návěštími listů jejího formačního stromu. DEFINICE 2-5 SLOŽITOAT FORMULE Složitost formule je rovna počtu uzlů formačního stromu formule, které nejsou listy. VĚTA 2-2 Složitost formule je rovna počtu výskytů logických spojek ve formuli. Uvedeme příklad pro určení hloubky a základny formule: ((p ® q) Ú false) ® ¬q ® Ú ¬q ® false q p q Formule má hloubku 3, neboť obsahuje maximálně uzly 3. úrovně. Základnu formule tvoří tři atomické formule p, q, false. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 12 KONTROLNÍ OTÁZKA 1 1. O co se v logice snažíme? 2. Jakým typem úsudku se logika zabývá? 3. Jaké jsou vlastnosti deduktivních úsudků? 4. Co nazýváme analytickou pravdivostí, kontradikcí? 5. Kdy je množina výroků sporná? 6. Co nazýváme důkazem? 7. Co nazýváme výrokovou logikou? CVIČENÍ 1 Příklad 1: Jedná se o výrok? • Autobus může jet v úterý nebo ve středu. • Odjíždím do Španělska a do Německa. • Je ČR právním státem? • Účast na akci je povinná nebo není povinná. • Pavla nestuduje historii, nýbrž sociologii a právo. • Není pravda, že jestliže souhlasíš s Petrem, pak souhlasím s Marcelou. • Cassidy je živý nebo mrtvý. • Je pravděpodobné, že půjde domů a do práce. Příklad 2: Negujte: • Budu se procházet nebo si zazpívám. • Pavel nefandí ani Spartě ani Slavii. • Je-li středa, je schůze. • Jestli se budu hodně učit nebo budu mít štěstí, pak udělám zkoušku. • Jestli se budu pilně učit, pak uspěju u zkoušky nebo budu mít pech. • Jestli bude zítra třetí světová válka, pak zahyne více než 3 milióny lidí. • Dám ti facku, když mě oklameš. • Bude-li pěkné počasí a nepokazí-li se nám auto, pojedeme na pláž a budeme se koupat. Příklad 3: Co vyplývá z následujících předpokladů? Karel pojede autobusem nebo vlakem. Jede-li Karel autobusem nebo svým vozem, pak přijede pozdě a zmešká schůzku. Karel nepřišel pozdě. Příklad 4: Převeďte větu v přirozeném jazyce na formuli ve výrokové logice. • Neběží-li motor, je vada v motoru nebo nejde proud. • Není pravda, že uchazeč umí anglicky i německy. 132 Výroková logika doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Příklad 5: Není černý, ale za to je hezký. Který z následujících výroků je pravdivý? • Není černý jen tehdy, když je hezký. • Je hezký. • Není černý a hezký. • Není černý. • Není černý a je hezký. Příklad 6: Hokejisté Havířova remizovali nebo prohráli se Slavií. Který z následujících výroků je pravdivý? • Hokejisté Havířova neremizovali nebo neprohráli se Slavií. • Hokejisté Havířova prohráli se Slavií. • Jestliže hokejisté Havířova prohráli se Slavií, pak s ní neremizovali. • Jestliže hokejisté Havířova remizovali se Slavií, pak s ní neprohráli. • Hokejisté Havířova remizovali. Příklad 7: Člověk je mrtvý jen tehdy, když zemřel. Který z následujících výroků je prav- divý? • Člověk je mrtvý. • Jestliže je člověk mrtvý, pak zemřel. • Jestliže člověk nezemřel, pak není mrtvý. • Člověk nezemřel. • Člověk je mrtvý a zemřel. Příklad 8: Fotbalisté trénují v létě a v zimě. Který z následujících výroků je určitě ne- pravdivý? • Fotbalisté netrénují v létě. • Fotbalisté netrénují v zimě. • Fotbalisté netrénují v zimě, ale trénují v létě. • Fotbalisté trénují v zimě a netrénují v létě. • Fotbalisté netrénují v létě nebo v zimě. SAMOSTATNÝ ÚKOL 1 Doplňte: • Výrok „email nedošel“ je negací výroku … • Výrok „a≠b“ je negací výroku … • Výrok „není pravda, že dopis nebyl odeslán“ je negací výroku… • Negujeme-li výrok „0,9 není celé číslo“, dostáváme výrok… • Negujeme-li výrok „a≠b“, dostáváme výrok… • Konjunkce „x je sudé číslo a x je prvočíslo“ má hodnotu pravda, právě když x = … doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 14 • Výrok tvaru „jestliže A, pak B“ se nazývá… • Druhý výrok v implikaci se nazývá… • První výrok v implikaci se nazývá… • Výrok „jestliže je doma, je na facebooku“ je pravdivý v těchto situacích: o Je doma a je na facebooku o … o … • Implikace je nepravdivá jen v případě, že antecedent je… a konsekvent je… • Zdůvodněte pravdivost výroku „jestliže x = 0, pak xy = 0“. Tento výrok je pravdivý, protože je vyloučeno, aby … • Ekvivalence „a-b = 0, když a jen když a = b“ je pravdivá, protože není možné, aby … nebo … • Kdyby ekvivalence „x 0) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 74 • Žádná individuová proměnná vystupující v termu t se po provedení substituce x/t nesmí stát ve formuli A vázanou (v takovém případě je term t za proměnnou x ve formuli A nesubstituovatelný). Symbolem A(x1,x2,...,xn / t1,t2,...,tn) označujeme formuli, která vznikne z formule A korektními substitucemi xi/ti pro i = 1, 2,...,n. Všechny formule tvaru A(x1, x2,...,xn / t1, t2,...,tn) nazýváme instancemi formule A. Jestliže formule A po substituci termů za proměnné již neobsahuje žádnou proměnnou, nazývá se bázovou instancí A. Proměnné obsažené ve formulích umožňují vyjadřovat obecná tvrzení. Dosazováním termů za proměnné lze pak získat jednotlivé instance formule, které představují tvrzení o jejich speciálních případech. ŘEŠENÝ PŘÍKLAD 8-1 Nechť formulí A(x) je: p(x) ® "y q(x, y) a term t nechť je f(y). Proveďte substituci A(x/f(y)). Řešení příkladu Provedeme-li substituci A(x/f(y)), dostaneme: p(f(y)) ® "y q(f(y), y). Vidíme, že druhý (zvýrazněný) výskyt proměnné y není volný (přitom původně zde byla volná proměnná x, takže jsme změnili ”smysl výrazu”). Tedy term f(y) není substituovatelný za x v dané formuli A, tj. p(x) ® "y q(x, y). * Nyní si ukážeme, jak převádět z přirozeného jazyka do symbolického jazyka PL1. Jde o analýzu výrazů přirozeného jazyka v rámci PL1. Volba predikátových (a funkčních) konstant je libovolná potud, že nesmí dojít ke ”kolizi vlastností, funkcí či vztahů”. Výrazy jako ”všichni”, ”každý”, ”nikdo”, apod. ”překládáme” všeobecným kvantifikátorem ", výrazy jako ”někdo”, ”někteří”, apod. ”překládáme” existenčním kvantifikátorem $. Dále budeme předpokládat, že jde o jazyk nad homogenním universem, proto v následujících příkladech považujeme za universum diskursu (obor proměnnosti proměnných) množinu všech individuí. Pro přehlednost budeme používat velká písmena pro predikátové symboly. 758 Predikátová logika 1. řádu doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky ŘEŠENÝ PŘÍKLAD 8-2 Analyzujte v jazyce PL1 následující výroky: 1. Nikdo, kdo není zapracován (P), nepracuje samostatně (S). 2. Ne každý talentovaný (T) spisovatel (Sp) je slavný (Sl). 3. Pouze zaměstnanci (Z) používají výtahu (V). 4. Ne každý člověk (C), který hodně mluví (M), nemá co říci (R). 5. Někdo je spokojen (Sn) a někdo není spokojen. 6. Někteří chytří lidé (Ch) jsou líní (L). 7. Všichni zaměstnanci (Z) používají výtahu (V). Řešení příkladu Jako pomůcka k řešení může sloužit tato zásada: Po všeobecném kvantifikátoru " následuje formule ve tvaru implikace (®), kdežto po existenčním kvantifikátoru formule ve tvaru konjunkce (&). 1. Nikdo, kdo není zapracován (P), nepracuje samostatně (S). "x [¬P(x) ® ¬S(x)] 2. Ne každý talentovaný (T) spisovatel (Sp) je slavný (Sl). ¬"x {[T(x) & Sp(x)] ® Sl(x)} 3. Pouze zaměstnanci (Z) používají výtahu (V). "x [V(x) ® Z(x)] 4. Ne každý člověk (C), který hodně mluví (M), nemá co říci (R). ¬"x {[C(x) & M(x)] ® ¬R(x)} 5. Někdo je spokojen (Sn) a někdo není spokojen. $x Sn(x) & $x ¬Sn(x) 6. Někteří chytří lidé (Ch) jsou líní (L). $x [Ch(x) & L(x)] 7. Všichni zaměstnanci (Z) používají výtahu (V). "x [Z(x) ® V(x)] * 8.1 Sémantika PL1 – interpretace formulí Sémantika neboli význam formulí predikátové logiky 1. řádu, je dána jejich interpretací. Než tento pojem přesně definujeme, uvedeme několik neformálních motivací a vysvětlení. Položíme-li si otázku, zda daná formule PL1 je pravdivá či ne, pak taková otázka je v podstatě nesmyslná, pokud nevíme, co formule znamená, tedy jak je interpretována. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 76 Tak např. formule "x p(f(x), x) • může ”říkat”, že pro všechna přirozená čísla platí, že jejich druhá mocnina je větší než to číslo, nebo že pro všechny lidi platí, že jejich otec je starší než dotyčný člověk, pak je samozřejmě v takových interpretacích pravdivá. • Může ale také znamenat, že pro všechna přirozená čísla platí, že jejich druhá mocnina je menší než to číslo, nebo že pro všechny lidi platí, že jejich otec je mladší než dotyčný člověk, pak je samozřejmě (v takové interpretaci) neprav- divá. V čem tedy spočívá interpretace formule? Nejprve musíme stanovit, ”o čem mluvíme”, tedy jaká je předmětná oblast – obor proměnnosti (individuových) proměnných, tj. zvolíme jistou neprázdnou množinu – universum diskursu, jejíž prvky jsou individua. Jelikož predikátové symboly mají vyjadřovat vztahy mezi těmito předměty – prvky universa, přiřadíme každému n-árnímu predikátovému symbolu jistou n-ární relaci (tj. podmnožinu Kartézského součinu) nad universem. Speciálně, jedná-li se o unární predikátový symbol (n = 1), pak přiřadíme podmnožinu universa. Podobně funkční symboly budou vyjadřovat n-ární funkce nad universem. Teprve poté, co je daná formule interpretována, můžeme vyhodnotit její pravdivost či nepravdivost v dané interpretaci. Informace představují data spolu se svou interpretací. Interpretací dat se rozumí jejich významová stránka. Pojem informace je tedy neoddělitelný od sémantiky dat. Je zde však ještě jeden problém, a to jsou proměnné. Proměnným jazyka PL1 přiřazujeme valuací individua, tj. prvky universa. (Proměnným jazyka PL2 mohou být přiřazeny také vlastnosti či funkce.) Jak uvidíme dále z definice sémantiky kvantifikátorů, pravdivostní hodnota formule nezávisí na hodnotě vázaných proměnných (pouze volné proměnné jsou ”skutečné” proměnné). Obsahuje-li však formule nějaké volné proměnné, můžeme vyhodnotit její pravdivost v interpretaci pouze v závislosti na ohodnocení (valuaci) volných proměnných. Při některé valuaci může být formule v dané interpretaci pravdivá, při jiné nepravdivá. Tak např. formule "x p(f(x), y) • může být interpretována nad množinou celých čísel tak, že symbolu p je přiřazena relace větší nebo rovno (³), symbolu f funkce druhá mocnina (tedy f(x) ”znamená” x2 ). • Pak formule ”říká”, že pro každé celé číslo x platí, že x2 je větší než nebo rovno jistému číslu y. • Tedy pravdivost formule v této interpretaci závisí na ohodnocení (valuaci) proměnné y. • Přiřadíme-li např. y číslo 5, je formule nepravdivá, přiřadíme-li třeba číslo -3 nebo 0, je formule pravdivá. • Obecně bude formule pravdivá (v této interpretaci) pro každou valuaci proměnné y, která přiřadí y záporné číslo nebo nulu, nepravdivá pro všechny valuace, které přiřadí proměnné y číslo kladné. 778 Predikátová logika 1. řádu doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky DEFINICE 8-2 INTERPRETACE JAZYKA PL1 Interpretace jazyka predikátové logiky 1. řádu je tato trojice objektů (která je někdy nazývána interpretační struktura): • Neprázdná množina M, která se nazývá universum diskursu a její prvky jsou individua. • Interpretace funkčních symbolů jazyka, která přiřazuje každému n-árnímu funkčnímu symbolu f určité zobrazení fM: Mn ® M. Interpretace predikátových symbolů jazyka, která přiřazuje každému n-árnímu predikátovému symbolu p jistou n-ární relaci pM nad M, tj. podmnožinu Kartézského součinu Mn . Každý n-ární funkční symbol je tedy interpretován jako funkce, která přiřazuje n-tici individuí právě jedno individuum, tj. zobrazení z M ´...´ M do M. Specielně: • je-li n = 0, pak se jedná o nulární funkční symbol, tedy o individuovou konstantu, které je přiřazen prvek universa – individuum • je-li n = 1, pak se jedná o unární funkční symbol, kterému je přiřazena funkce o jednom argumentu (např. nad množinou čísel x2 , x + 1, nad množinou individuí otec(x), matka(x), atd.) • je-li n = 2, pak se jedná o binární funkční symbol, kterému je přiřazena binární funkce se dvěma argumenty (např. nad množinou čísel x + y, x.y, atd.) Každý n-ární predikátový symbol p je interpretován jako n-ární relace pM, tj. podmnožina Kartézského součinu M ´...´ M, neboli zobrazení M ´...´ M ® {1,0}. Tato relace pM se nazývá obor pravdivosti predikátu. Speciálně: • je-li n = 0, pak se jedná o nulární predikátový symbol, kterému je přiřazena hodnota 1 nebo 0 (pravda, nepravda) tak, jak to již známe z výrokové logiky. • je-li n = 1, pak se jedná o unární predikátový symbol, kterému je přiřazena podmnožina universa M. (Vlastnosti tedy v PL1 vyjadřujeme – poněkud nepřesně – jako podmnožiny universa.) • je-li n = 2, pak se jedná o binární predikátový symbol, kterému je přiřazena binární relace nad universem (např. relace větší, menší, apod.) Výroková logika je tedy speciálním (nejjednodušším) případem predikátové logiky, a to 0. řádu, ve které pracujeme pouze s nulárními predikáty a nepotřebujeme proto termy, funkční symboly, individuové proměnné ani universum diskursu (obor proměnnosti proměnných). Nulárním predikátům přiřazujeme pouze hodnoty pravda, nepravda. Ohodnocení (valuace) individuových proměnných je zobrazení e, které každé proměnné x přiřazuje hodnotu e(x) Î M (prvek univerza). Ohodnocení termů e* indukované ohodnocením proměnných e je induktivně definováno takto: • e* (x) = e(x) • e*(f (t1, t2,...,tn)) = fM (e*(t1), e*(t2),...,e*(tn)), kde fM je funkce přiřazená v dané interpretaci funkčnímu symbolu f. Hodnotou (realizací) termu t v interpretaci I je tedy vždy jistý prvek universa. Tedy funkční symboly jsou “jména funkcí – zobrazení”, termy jsou “jména prvků universa”, doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 78 zatímco predikátové symboly jsou “jména relací” a formule jsou “jména pravdivostních hodnot”. DEFINICE 8-3 PRAVDIVOST FORMULE Pravdivost formule A v interpretaci I pro ohodnocení e individuových proměnných (což značíme |=I A[e] – formule A je pravdivá v I pro e, nebo také A je splněna v I ohodnocením e), je definována v závislosti na tvaru formule: Je-li A atomická formule tvaru • p(t1, …, tn), kde p je predikátový symbol (různý od =) a t1, …, tn jsou termy, pak |=I A[e], jestliže platí < e*(t1), e*(t2),...,e*(tn)> Î pM, kde pM je relace přiřazená interpretací I symbolu p – obor pravdivosti p. Tedy individua, která jsou hodnotou termů t1, …, tn, jsou v relaci pM. • (t1 = t2), pak |=I A[e], jestliže platí e*(t1) = e*(t2), tj. oba termy jsou realizovány týmž individuem. Je-li A složená formule tvaru • ¬B, pak |= I A[e] jestliže neplatí |= I B[e] • B & C, pak |= I A[e], jestliže platí |= I B[e] a |= I C[e] • B Ú C, pak |= I A[e], jestliže platí |= I B[e] nebo |= I C[e] • B ® C, pak |= I A[e], jestliže neplatí |= I B[e] nebo platí |= I C[e] • B «C, pak |= I A[e], jestliže platí |= I B[e] a |= I C[e], nebo neplatí |= I B[e] a neplatí |= I C[e]. Je-li A formule tvaru • "x B, pak |= I A[e], jestliže pro libovolné individuum i Î M platí |= I B[e(x/i)], kde e(x/i) je valuace stejná jako e až na to, že přiřazuje proměnné x individuum i. • $x B, pak |= I A[e], jestliže pro alespoň jedno individuum i Î M platí |= I B[e(x/i)], kde e(x/i) je valuace stejná jako e až na to, že přiřazuje proměnné x individuum i. Je-li universum diskursu konečná množina M = {a1,…,an}, pak platí následující ekvivalence formulí: "x A(x) Û A(a1) & … & A(an) $x A(x) Û A(a1) Ú… Ú A(an). Z definice kvantifikátorů je navíc zřejmé, že platí: "x A(x) Û ¬$x ¬A(x), $x A(x) Û ¬"x ¬A(x). Formule A je splnitelná v interpretaci I, jestliže existuje ohodnocení e proměnných takové, že platí |= I A [e]. Formule A je pravdivá v interpretaci I, značíme |= I A , jestliže pro všechna možná ohodnocení e individuových proměnných platí, že |= I A[e]. 798 Predikátová logika 1. řádu doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Formule A je splnitelná, jestliže existuje interpretace I, ve které je splněna, tj. jestliže existuje interpretace I a valuace e takové, že |= I A[e]. Taková interpretace I a valuace e, tedy dvojice , pro kterou platí |= I A[e], se nazývá model formule. Formule A je tautologií (logicky pravdivá), značíme |= A, jestliže je pravdivá v každé interpretaci. Formule A je kontradikcí, jestliže nemá model, tedy neexistuje interpretace I, která by formuli A splňovala. Podmnožinou množiny splnitelných formulí je množina formulí platných v dané struktuře při všech jejích možných valuacích a podmnožinou této podmnožiny je pak množina logicky platných formulí. Model množiny formulí {A1,…,An} je taková interpretace I (a případně valuace e volných proměnných), která splňuje všechny formule A1,…,An, tedy dvojice , pro kterou platí |= I A1[e],…, |= I An[e]. Formule B logicky vyplývá z formulí A1, …, An, značíme A1,…,An |= B, jestliže B je pravdivá v každém modelu množiny formulí A1,…,An. Tedy pro každou interpretaci I, která splňuje formule A1, …, An (|= I A1[e],…, |= I An[e]) platí, že splňuje také formuli B (|= I B[e]). Formule A, B jsou (sémanticky) ekvivalentní, jestliže pro všechny interpretace I a všechny valuace e mají stejná pravdivostní ohodnocení. Skutečnost, že formule A, B jsou ekvivalentní zapisujeme: A Û B. VĚTA 8-1 Nechť platí: A je formule výrokové logiky sestavená z výrokových symbolů p1, p2,...,pn, B1,B2,...,Bn jsou libovolné formule predikátové logiky, formule A' vznikne z formule A náhradami proměnných p1, p2,...,pn formulemi B1, B2,...,Bn (po řadě, tj. Bi za pi). Potom platí: je-li A tautologií výrokové logiky, je A' tautologií predikátové logiky. Důkaz : Pravdivostní hodnota formule A nezávisí na pravdivostních hodnotách formulí p1, p2,...,pn a tedy ani pravdivostní hodnota formule A' nezávisí na pravdivostních hodnotách formulí B1, B2,...,Bn. VĚTA 8-2 Nechť platí: Formule A obsahuje podformule B1, B2,...,Bn , formule B1, B2,...,Bn jsou po řadě ekvivalentní s formulemi B1', B2',...,Bn' /tj. Bi Û Bi'/, formule A' vznikne z formule doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 80 A náhradami formulí B1, B2,...,Bn formulemi B1', B2',...,Bn' (po řadě, tj. Bi' za Bi). Potom platí: je-li A tautologií predikátové logiky, je i A' tautologií predikátové logiky. Důkaz : Ve formuli A nahrazujeme podformule formulemi se stejným pravdivostním ohodnocením (pro všechny (I, e)). Tedy pravdivostní ohodnocení formule A' musí být pro všechny (I, e) stejné jako pravdivostní ohodnocení formule A. Je-li tedy A tautologií, je tautologií i A'. Nyní uvedeme některé důležité tautologie predikátové logiky: 1. |= "xA(x) ® A(y) dictum de omni speciálně |= "xA(x) ® A(x/t) 2. |= A(y) ® $xA(x) De Morganovy zákony: 3. |= ¬"xA(x) « $x¬A(x) 4. |= ¬$xA(x) « "x¬A(x) Zákony distribuce kvantifikátorů: 5. |= "x[A(x) ® B(x)] ® ["xA(x) ® "xB(x)] 6. |= "x[A(x) ® B(x)] ®[$xA(x) ® $xB(x)] 7. |= "x[A(x) & B(x)] « ["xA(x) & "xB(x)] 8. |= $x[A(x) & B(x)] ® [$xA(x) & $xB(x)] 9. |= ["xA(x) Ú "xB(x)] ® "x[A(x) Ú B(x)] 10. |= $x[A(x) Ú B(x)] « [$xA(x) Ú $xB(x)] Zákony prenexních operací (předpokládáme, že formule A neobsahuje volnou proměnnou x): 11. |= "x[A ® B(x)] « [A ® "xB(x)] 12. |= $x[A ® B(x)] « [A ® $xB(x)] 13. |= "x[B(x) ® A] « [$xB(x) ® A] 14. |= $x[B(x) ® A] « ["xB(x) ® A] 15. |= "x[A & B(x)] « [A & "xB(x)] 16. |= $x[A & B(x)] « [A & $xB(x)] 17. |= "x[A Ú B(x)] « [A Ú "xB(x)] 18. |= $x[A Ú B(x)] « [A Ú $xB(x)] Zákony komutace kvantifikátorů: 19. |= "x"yA(x,y) « "y"xA(x,y) 20. |= $x$yA(x,y) « $y$xA(x,y) |= $x"yA(x,y) ®"y$xA(x,y) Nechť term t je substituovatelný za proměnnou x: 22. |= "xA(x) ® A(x/t) zákon konkretizace 23. |= A(x/t) ® $xA(x) zákon abstrakce 24. |= "xA(x) ® $xA(x) zákon partikularizace 818 Predikátová logika 1. řádu doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky DEFINICE 8-4 DUÁLNÍ FORMULE Nechť formule F je utvořena z elementárních formulí A, B,... pouze pomocí funktorů ¬, &, Ú, ", $. Formuli F', která vznikne z formule F vzájemnými záměnami funktorů & a Ú a vzájemnými záměnami funktorů " a $, nazýváme duální formulí k formuli F. Vzhledem k tomu, že F'' = F, jsou formule F a F´ duálními navzájem. VĚTA 8-3 Nechť L je jazyk predikátové logiky s danou interpretací I, v němž x je proměnná, A je formule. I ⊨ A, právě když I ⊨ "x A. Důkaz : Nechť I ⊨ A, tj. A je pravdivá v I při libovolném ohodnocení, tedy i pro takové ohodnocení e, v němž za x zvolíme libovolné individuum m z universa M. Platí tedy I ⊨ "x A[e(x/m)] pro libovolně zvolené m a proto platí I ⊨ "x A. Dokážeme nepřímo: předpokládejme, že neplatí I ⊨ "x A. Potom by muselo existovat ohodnocení e0 takové, že při němž by neplatilo I ⊨ A[e0], tj. platilo by I ⊨ ¬A[e0]. To ale odporuje předpokladu, že I ⊨ A[e] pro všechna e. VĚTA 8-4 Nechť A je formule jazyka L a I jeho interpretace. Potom A je nesplnitelná v I, právě když I ⊨ "¬A. Důkaz : Je-li A nesplnitelná, tj. neplatí I ú= A[e] pro libovolné e, platí tedy I ú= ¬ A[e] pro všechna e a proto platí I ú= ¬A. Podle předcházející věty pak platí I ú= "¬A. Dokážeme nepřímo: Kdyby A byla splnitelná v I, existovalo by ohodnocení e takové, že Iú=A[e], proto by nemohlo platit I ú= "¬A. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 82 VĚTA 8-5 Nechť A je formule jazyka L a I jeho interpretace. Potom A je splnitelná v I, právě když I ú= $A. Důkaz : Je-li A splnitelná, pak existuje takové ohodnocení e, že platí I ú= A[e]. Zřejmě pak platí Iú=$A[e]. Podle důsledku předchozího lemmatu je pak ale I ú= $A, neboť $A je uzavřená formule. Dokážeme nepřímo: kdyby A byla nesplnitelná, neexistovalo by ohodnocení e takové, že i Iú=A[e], tedy by neplatilo Iú= $A[e] a proto ani I ú= $ A. KONTROLNÍ OTÁZKA 7 1. Definujte jazyk predikátové logiky. 2. Definujte splnitelnost a pravdivost v predikátové logice. 3. Co nazýváme interpretací? CVIČENÍ 7 Příklad 1: Převeďte následující věty v přirozeném jazyce do formulí v predikátové lo- gice. • Někteří studenti nemají hudební nadání. • Někteří přítomní bydlí v hotelu. • Někteří studenti nejsou ani nadaní ani pilní. • Každé číslo dělitelné 8 je dělitelné 4. • Kdo seje vítr, ten sklízí bouři. • Psi, kteří hodně štěkají, nekoušou. • Žádný tyran není spravedlivý. • Každý člověk má otce, má i matku. • Každý, kdo má otce, má i matku. • Každý člověk je mladší než jeho rodiče. (pomocí termů) • Žádný dobrý učitel nikoho zbytečně nepotrestal. • Někdo má rád každého. • Někdo má rád ostatní. • Není všechno zlato, co se třpytí. • Všichni sourozenci mají stejného otce. (pomocí termů) Příklad 2: Nechť výraz P(l, e, t) znamená Luboš půjčuje Evě tužku. Zapište symbolicky následující výroky. 838 Predikátová logika 1. řádu doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky • Někdo půjčuje Evě tužku. • Eva půjčuje někomu tužku. • Eva někomu něco půjčuje. • Někdo Evě něco půjčuje. • Luboš každému něco půjčuje. • Někdo někomu něco půjčuje. • Každý někomu něco půjčuje. • Někdo každému všechno půjčuje. • Někdo nikomu nic nepůjčuje. • Žádný každému všechno nepůjčuje. • Všichni všechno všem půjčují. Příklad 3: Nechť výraz V(p, t) znamená „vidím předmět p v okamžiku t. „zapište symbolicky věty. • Vždy něco vidím. • Někdy nevidím nic. • Existují předměty, které nikdy nevidím. • Vidím každou věc v některém časovém okamžiku. Příklad 4: Najděte negace formulí • $x ((p(x) & q(x)) Ú r(x)) • " x(p(x) ® "y q(y)) • " x(p(x) Ú $y q(y)) • " x(p(x) ® q(x)) & $x(r(x) & s(x)) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 84 9 AUTOMATICKÉ DOKAZOVÁNÍ V PREDIKÁTOVÉ LOGICE (OBECNÁ REZOLUČNÍ METODA) ČAS POTŘEBNÝ KE STUDIU Celkový doporučený čas k prostudování KAPITOLY je 90 minut. RYCHLÝ NÁHLED DO PROBLEMATIKY KAPITOLY AUTOMATICKÉ DOKAZOVÁNÍ V PREDIKÁTOVÉ LOGICE (OBECNÁ REZOLUČNÍ METODA) Cílem devátého modulu je rezoluční princip v predikátové logice 1. řádu. Rychlý ná- hled KLÍČOVÁ SLOVA KAPITOLY AUTOMATICKÉ DOKAZOVÁNÍ V PREDIKÁTOVÉ LOGICE (OBECNÁ REZOLUČNÍ METODA) Rezoluční princip, prenexní tvar, Skolemova forma, unifikace. Klíčová slova Důkaz logické pravdivosti, a tedy i logického vyplývání apod., zkoumáním všech možných interpretací, je v predikátové logice často obtížný. Jednou z efektivních metod je však rezoluční metoda, která je pro PL1 zobecněním základní rezoluční metody výrokové logiky. Obecná rezoluční metoda se stala základem pro logické programování, zejména programovací jazyk PROLOG (Programming in Logic). Rezoluční metoda je jedna z procedur (algoritmů), které parciálně rozhodují, zda daná formule PL1 je nesplnitelná. Pro předloženou formuli A, která nesplnitelná je, tedy procedura v konečném čase tuto skutečnost zjistí a zastaví se. V případě, že A je splnitelná, algoritmus nemusí nikdy skončit svou činnost. Chceme-li tedy rozhodnout, zda daná formule A je logicky pravdivá, použijeme rezoluční metodu na formuli ¬A a zjišťujeme, zda je nesplnitelná. Je-li tomu tak, procedura to zjistí a vydá kladnou odpověď. V opačném případě proces nemusí nikdy skončit. Chceme-li zjistit, zda-li B vyplývá z předpokladů A1,…,An , formálně zapsáno: {A1,…,An} |= B aplikujeme rezoluční metodu na formuli A1 & … & An & ¬B, neboť 859 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky pokud je tato formule nesplnitelná, pak je formule (A1 & … & An) ® B tautologie a vztah vyplývání platí. Rezoluční metodu lze aplikovat pouze na formule speciálního tvaru, v tzv. klauzulární (Skolemově) formě. Nejprve proto ukážeme, že každou formuli je možno převést do klauzulární formy tak, že výsledná formule je splnitelná, právě když výchozí formule je splnitelná. Potom uvedeme Herbrandovu větu, o niž se opírají první známé rozhodovací procedury pro dokazování nesplnitelnosti v predikátové logice 1. řádu. Uplatnění rezolučního pravidla výrokové logiky je totiž v PL1 komplikováno tím, že v literálech se vyskytují termy obecně různého „tvaru”, které je nutno nějak „unifikovat”. Popíšeme základní rezoluční metodu pro PL1, která je značně neefektivní. Průlomem v těchto metodách se však stal Robinsonův objev unifikačního algoritmu, který umožnil zobecnění základní rezoluční metody na mnohem účinnější rezoluční metodu, která se pak stala základem logického programování. Automatické dokazování v predikátové logice zobecňuje postupy automatického dokazování výrokové logiky. Oproti situaci ve výrokové logice je situace v predikátové logice složitější a to z těchto důvodů. Komplikovanější je procedura převedení formule na klauzulární tvar. Oproti výrokové logice obsahuje navíc: převod formule na prenexní tvar, eliminaci kvantifikátorů z formule. Složitější je tvar rezolučního odvozovacího pravidla. Jeho použití vyžaduje úpravu literálů - unifikaci. DEFINICE 9-1 PRENEXNÍ TVAR FORMULE Formule A predikátové logiky je v prenexním tvaru, má-li podobu Q1x1 Q2x2...Qnxn B, kde • n ³ 0 a pro každé i = 1, 2,...,n je Qi buď všeobecný kvantifikátor " nebo existenční $, • x1, x2,...,xn jsou navzájem různé individuové proměnné, • B je formule utvořená z elementárních formulí pouze užitím výrokových funktorů ¬, &, Ú. Výraz Q1x1 Q2x2...Qnxn se nazývá prefix (charakteristika) a B otevřeným jádrem (maticí) formule A v prenexním tvaru. VĚTA 9-1 Každou formuli lze přepsat do prenexního tvaru, tj. ke každé formuli predikátové logiky A existuje formule A* v prenexním tvaru, která je s formulí A ekvivalentní (tj. A Û A*). Důkaz : Algoritmus převodu formule do prenexního tvaru má tyto kroky: doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 86 1. Eliminace funktorů ® a «. Toho lze dosáhnout užitím následujících ekvivalencí (náhrady jejich levé strany pravou stranou): A ® B Û ¬A Ú B, A « B Û (A ® B) & (B ® A) Û (¬A Ú B) & (¬B Ú A). 2. Převedení formule na tvar s čistými proměnnými. • Použijeme následující ekvivalence (náhrady levé strany pravou): ("xA & "xB) Û "x (A & B) ($xA Ú $xB) Û $x (A Ú B) • Přejmenování vázaných proměnných tak, aby žádná proměnná nebyla ve formuli současně volná i vázaná a tak, aby všechny vázané proměnné byly navzájem různé. To platí nejenom pro celou formuli, ale i pro každou její podformuli. 3. Vypuštění nadbytečných kvantifikátorů, tj. Kvantifikátorů jejichž oblast působnosti neobsahuje žádný výskyt kvantifikované proměnné. 4. Přenesení všech výskytů funktoru negace bezprostředně před elementární formule. Toho lze dosáhnout opakovaným užitím následujících ekvivalencí (náhrady jejich levé strany pravou stranou): ¬¬A Û A, ¬(A & B) Û ¬A Ú ¬B, ¬(A Ú B) Û ¬A & ¬B, ¬"x A(x) Û $x ¬A(x), ¬$x A(x) Û "x ¬A(x). 5. Přenesení všech kvantifikátorů na začátek formule. Toho lze dosáhnout opakovaným užitím následujících ekvivalencí (náhrady jejich levé strany pravou stra- nou): "xA & B Û "x (A & B) $xA Ú B Û $x (A Ú B) B neobsahuje volnou x A & "xB Û "x (A & B) A Ú $xB Û $x (A Ú B) A neobsahuje volnou x $xA & B Û $x (A & B) "xA Ú B Û "x (A Ú B) B neobsahuje volnou x A & $xB Û $x (A & B) A Ú "xB Û "x (A Ú B) A neobsahuje volnou x ŘEŠENÝ PŘÍKLAD 9-1 Určete prenexní formu formule: "x [p(x) & "y$x (¬q(x,y) ® "z r(a,x,y))]. Řešení příkladu "x [p(x) & "y$x (q(x,y) Ú "z r(a,x,y))] eliminace ® "x [p(x) & "y$t (q(t,y) Ú "z r(a,t,y))] přejmenování proměnné "x [p(x) & "y$t (q(t,y) Ú r(a,t,y))] vypuštění nadbytečného kvantifiká- toru 879 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky "x"y [p(x) & $t (q(t,y) Ú r(a,t,y))] přesun kvantifikátoru doleva "x"y$t [p(x) & (q(t,y) Ú r(a,t,y))] přesun kvantifikátoru dolev. * Prenexní tvar formule není určen jednoznačně. Konečná podoba prenexní formule závisí na pořadí provádění úprav a na způsobu přejmenování vázaných proměnných. Všechny prenexní tvary jsou však ekvivalentní. DEFINICE 9-2 SKOLEMOVA FORMA FORMULE Skolemova forma uzavřené formule je prenexní tvar této formule, která neobsahuje žádné existenční kvantifikátory. Skolemova forma vznikne z prenexní formy opakovaným použitím následujících dvou operací (skolemizací): "x1 "x2..."xn $y A(x1, x2,...,xn, y) ® "x1 "x2..."xn A(x1, x2,...,xn, f(x1, x2,..., xn)), kde f je nový (v jazyce dosud nepoužitý) n-ární funkční symbol, tzv. Skolemova funkce, $x "y1 "y2..."yn A(x, y1, y2,...,yn) ® "y1 "y2..."yn A(c, y1, y2,...,yn), kde c je nová (v jazyce dosud nepoužitá) individuová konstanta, tzv. Skolemova konstanta Každému eliminovanému existenčnímu kvantifikátoru odpovídá jiná Skolemova funkce nebo konstanta. Skolemovu formu formule A označíme zápisem AS . Konjunktivní normální tvar formule predikátové logiky je prenexní tvar formule, jejíž matice je konjunkce disjunkcí literálů (tj. konjunkce klauzulí). Disjunktivní normální tvar formule predikátové logiky je prenexní tvar formule, jejíž matice je disjunkce konjunkcí literálů. Klauzulární forma formule je Skolemova forma, jejíž matice je v klauzulárním tvaru, tj. je konjunkcí klausulí. Skolemovy konstanty a funkce představují předměty (reprezentanty předmětů), o jejichž existenci vypovídají původní formule. Například: $x"y A(x,y) ® "y A(c, y) Je-li univerzem množina všech nezáporných celých čísel a realizací (interpretací) predikátu A je relace < (tedy A(x,y) „chápeme jako“ x < y), pak c interpretujeme jako 0. V tomto modelu je konstanta c jediná, ale v jiných modelech tomu tak být nemusí. "x$y A(x,y) ® "x A(x,f(x)) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 88 Je-li univerzem množina reálných čísel a oborem pravdivosti predikátu A je relace <, pak interpretací funkčního symbolu f může být např. funkce f‘, která je zadaná předpisem: f‘(x) = x + Ö3. Po provedené skolemizaci zůstávají v prefixu formule pouze obecné kvantifikátory. Důležitá pro nás je klausulární forma formule: "x1"x2…"xn[C1&C2& …Ck], kde Ci jsou klausule (disjunkce literálů). Vzhledem k tomu, že uvažujeme pouze uzavřené formule, není nutné tyto kvantifikátory explicitně uvádět. Skolemova forma AS uzavřené formule A není ekvivalentní s formulí A, ale platí: ⊨ AS ® A, neboli AS ⊨ A. VĚTA 9-2 Každá formule A může být převedena na formuli AS v klauzulární (Skolemově) formě takovou, že A je splnitelná, právě když AS je splnitelná. Důkaz : Uvedeme algoritmus převodu A ® AS . 1. Utvoření existenčního uzávěru formule A. (Zachovává splnitelnost.) 2. Eliminace nadbytečných kvantifikátorů. (Ekvivalentní krok.) Z formule A vypustíme všechny kvantifikátory "xi, $xi, v jejichž rozsahu se nevyskytuje proměnná xi. 3. Přejmenování proměnných. (Ekvivalentní rok.) Přejmenujeme všechny proměnné, které jsou v A kvantifikovány více než jednou tak, aby všechny kvantifikátory měly navzájem různé proměnné. 4. Eliminace spojek ®, « podle těchto vztahů (Ekvivalentní krok.): (A ® B) Û (¬A Ú B), (A « B) Û (¬A Ú B) & (¬B Ú A) 5. Přesun spojek ¬ dovnitř. (Ekvivalentní krok.) 6. Přesun kvantifikátorů doprava. (Ekvivalentní krok.) Provádíme náhrady podle těchto ekvivalencí (Q je kvantifikátor " nebo $; © je symbol & nebo Ú; A, B neobsahují volnou proměnnou x): Qx (A © B(x)) Û A © Qx B(x), Qx (A(x) © B) Û Qx A(x) © B 7. Eliminace existenčních kvantifikátorů (Zachovává splnitelnost.) Provádíme postupně Skolemizaci. 8. Přesun všeobecných kvantifikátorů doleva. (Ekvivalentní krok, neboť jsme již provedli krok 3. a platí ekvivalence dle 6.) 9. Použití distributivních zákonů. (Ekvivalentní krok.) Provedeme postupné náhrady podformulí vlevo formulemi vpravo: (A &B) Ú C Û (A Ú C) & (B Ú C), A Ú (B & C) Û (A Ú B) & (A Ú C). 899 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Z praktických důvodů se snažíme minimalizovat počet argumentů zaváděných Skolemových funkcí. Krok 6 slouží tomuto účelu. Výslednou formuli můžeme ještě zjednodušit použitím úprav, které zachovávají splnitelnost. Uvažujme formuli A = "x $y "z $v [p(z,y) Ù q(x,v)]. Pokud bychom aplikovali Skolemizaci bez kroku 6, dostali bychom formuli: AS ‘ = "x "z [p(z, f(x) & q(x, h(x,z)], kde f, h jsou zavedené Skolemovy funkce. Použijeme-li však nejprve krok 6, dostaneme A’ = $y "z p(z,y) & "x $v q(x,v) a z ní eliminací existenčních kvantifikátorů A’’ = "z p(z, a) & "x q(x, h(x)). Odtud pak přesunem kvantifikátorů doleva: AS = "z "x [p(z, a) & q(x, h(x))], v níž zavedené Skolemovy funkce a, h jsou jednodušší. ŘEŠENÝ PŘÍKLAD 9-2 Nalezněte Skolemovu formu uzavřené prenexní formy $u"v$w"x"y$z A(u, v, w, x, y, z). Řešení příkladu 1. $u"v$w"x"y$z A(u, v, w, x, y, z) výchozí forma 2. "v$w"x"y$z A(a, v, w, x, y, z) po eliminaci $u 3. "v"x"y$z A(a, v, f(v), x, y, z) po eliminaci $w 4. "v"x"y A(a, v, f(v), x, y, g(v,x,y)) po eliminaci $z 5. A(a, v, f(v), x, y, g(v,x,y)) bez explicitní obecné kvantifikace. Převedeme formuli A na formuli v klausulární (Skolemově) formě AS : A = "x{p(x) ® $z{¬"y[q(x,y) ® p(f(x1))] & "y[q(x,y) ® p(x)]}}. 1.,2. Utvoření existenčního uzávěru a eliminace $z: A2 = $x1"x{p(x) ® {¬"y[q(x,y) ® p(f(x1))] & "y[q(x,y) ® p(x)]}}. 3. Přejmenování proměnné y: A3 = $x1"x{p(x) ® {¬"y[q(x,y) ® p(f(x1))] & "z[q(x,z) ® p(x)]}}. 4. Eliminace ®: A4 = $x1"x{¬p(x) Ú {¬"y[¬q(x,y) Ú p(f(x1))] & "z[¬q(x,z) Ú p(x)]}}. 5. Přesun negace dovnitř: A5 = $x1"x{¬p(x) Ú {$y[q(x,y) & ¬p(f(x1))] & "z[¬q(x,z) Ú p(x)]} 6. Přesun kvantifikátorů $y a "z doprava: A6 = $x1"x{¬p(x) Ú {[$y q(x,y) & ¬p(f(x1))] & ["z ¬q(x,z) Ú p(x)]}}. 7. Eliminace existenčních kvantifikátorů: doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 90 A7 = "x{¬p(x) Ú {[q(x,h(x)) & ¬p(f(a))] & ["z ¬q(x,z) Ú p(x)]}}. 8. Přesun "z doleva: A8 = "x"z{¬p(x) Ú {[q(x,h(x)) & ¬p(f(a))] & [¬q(x,z) Ú p(x)]}}. 9. Použití distributivního zákona: A9 = "x"z{[¬p(x) Ú q(x,h(x))] & [¬p(x) Ú ¬p(f(a))] & [¬p(x) Ú ¬q(x,z) Ú p(x)]}. 10. Provedeme zjednodušení: i) Vypustíme třetí klausuli (je to tautologie) ii) Odstraníme kvantifikátor "z (stal se zbytečným) iii) Ve druhé klausuli odstraníme ¬p(x), neovlivníme tím splnitelnost AS = "x{ [¬p(x) Ú q(x,h(x))] & ¬p(f(a)) }. * Herbrandova procedura. Chceme-li dokázat logickou pravdivost formule A v PL1, pak budeme postupovat obdobně jako ve VL: • Formuli A znegujeme • Formuli ¬A převedeme do klauzulární formy (¬A)S • Na formuli (¬A)S budeme postupně uplatňovat rezoluční pravidlo. Pokud získáme prázdnou klausuli, je důkaz úspěšně ukončen. o Tento třetí bod však v PL1 nelze provést tak jednoduše jako ve výrokové logice. Problémem je to, že literály s opačným znaménkem, které bychom mohli při uplatňování rezoluce „vyškrtávat“, mohou obsahovat různé termy. ŘEŠENÝ PŘÍKLAD 9-3 Uvažujme formuli A v klauzulární formě: "x "y "z "v [p(x, f(x)) & q(y, h(y)) & (¬p(a, z) Ú ¬q(z, v))]. Dokažte, že tato formule je nesplnitelná. Řešení příkladu Vypišme jednotlivé klausule pod sebe a pokusme se uplatňovat pravidlo rezoluce: 1. p(x, f(x)) 2. q(y, h(y)) 3. ¬p(a, z) Ú ¬q(z, v) Klausule 1. a 3. obsahují literály s opačným znaménkem, avšak uplatnění rezoluce brání to, že p(x, f(x)) ¹ p(a, z). Je-li term t substituovatelný za x ve formuli A(x), pak "x A(x) |= A(x/t), „co platí pro všechny, platí i pro t“), můžeme se pokusit najít vhodnou substituci termů za proměnné tak, abychom dostali shodné „unifikované“ literály. 919 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky V našem příkladě taková substituce existuje: x / a, z / f(a). Po provedení této substituce dostaneme klausule: 1’. p(a, f(a)) 2. q(y, h(y)) 3‘. ¬p(a, f(a)) Ú ¬q(f(a), v) kde na 1‘ a 3‘ již lze uplatnit pravidlo rezoluce: 4. ¬q(f(a), v) Abychom nyní mohli rezolvovat klausule 2. a 4., zvolíme opět substituci: y / f(a), v / h(f(a)). Dostaneme 2‘. q(f(a), h(f(a))) 4’. ¬ q(f(a), h(f(a))) a jejich rezolucí již obdržíme prázdnou klausuli. Tedy formule A je nesplnitelná. * Problémem ovšem je to, že příslušné substituce jsme hledali ”zkusmo”, intuitivně. Aby mohl být celý proces automatizován (a mohl tak sloužit jako základ pro logické programování), musíme najít nějaký algoritmus, jak provádět příslušné unifikace. Uvedeme zde dva: • Herbrandova procedura • Robinsonův unifikační algoritmus Podle definice je daná formule A nesplnitelná, právě když nabývá hodnoty nepravda ve všech interpretacích nad všemi možnými obory interpretace. Důkaz toho, že A je nesplnitelná, by samozřejmě usnadnilo, kdybychom našli jistý pevný obor interpretace D takový, že A je nesplnitelná, právě když nabývá hodnoty nepravda ve všech interpretacích nad tímto pevným oborem D. Takový obor ke každé formuli A existuje a nazývá se Herbrandovo universum HA. DEFINICE 9-3 HERBRANDOVO UNIVERSUM Herbrandovo universum HA je tvořeno množinou všech termů, které mohou být sestrojeny z individuových konstant ai a funkčních konstant fi, které se vyskytují v A. (Pokud v A není žádná individuová konstanta, použijeme libovolnou, např. a.) V dalším výkladu budeme vyznačovat prvky Herbrandova universa kurzívou a tučně, abychom je odlišili od funkčních symbolů formule. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 92 Příklad: Pro formuli A = "x [p(a) Ú q(b) ® p(f(x))] je HA = {a, b, f(a), f(b), f(f(a)), f(f(b)), …} Pro formuli B = "x "y p( (f(x), y, q(x,y)) je HA = {a, f(a), q(a,a), f(f(a)), q(a,f(a)), q(f(a),a), …}. DEFINICE 9-4 Buď A formule v klausulární formě: "x1 "x2 … "xn [C1 & …& Ck]. Základní instancí klausule Ci (1 £ i £ k) rozumíme klausuli, která vznikne z Ci tím, že všechny individuové proměnné v Ci nahradíme nějakými prvky z HA. VĚTA 9-3 HERBRAND Formule A v klausulární formě je nesplnitelná, právě když existuje konečná konjunkce základních instancí jejích klausulí, která je nesplnitelná. Herbrandova procedura parciálně rozhoduje, zda je daná formule A nesplnitelná. K dané formuli postupně generujeme základní instance jejích klausulí a resoluční metodou vždy testujeme, zda je jejich konjunkce nesplnitelná. Jestliže tomu tak je, pak A je nesplnitelná a tato procedura to po konečném počtu kroků zjistí. V případě splnitelnosti A může procedura generovat donekonečna nové a nové základní instance a testovat jejich kon- junkce. Podstatným problémem této metody je skutečnost, že generování základních klausulí je neefektivní. Počet základních instancí, které musí být generovány, dokud nenarazíme na ”protipříklad” – nesplnitelnou konjunkci, může být často tak velký, že nám přeplní paměť počítače, nehledě na časovou složitost takového algoritmu. J.A. Robinson navrhl v r. 1965 metodu, která na rozdíl od Herbrandovy procedury nevyžaduje generování základních instancí, ale rozhodne přímo, zda k libovolné konjunkci klausulí existuje substituce taková, která unifikuje některé literály a umožní dokázat nesplnitelnost (pokud tato konjunkce nesplnitelná je). DEFINICE 9-5 SIMULTÁNNÍ SUBSTITUCE TERMŮ Nechť A je formule obsahující individuové proměnné xi, i = 1,2,...,n, a to buď přímo (jako bezprostřední argumenty) nebo zprostředkovaně (jako argumenty funkcí). Označme s ={x1/t1, x2/t2, ...,xn/tn} simultánní substituci termů ti za (všechny výskyty) 939 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky předmětové proměnné xi pro i = 1,2, ...,n. Potom zápisem As označíme formuli, která vznikne z formule A provedením substituce s. Poznamenejme, že substituce se může týkat všech, nebo jen některých, nebo dokonce žádné individuové proměnné obsažené v A (v tomto případě pro některá nebo všechna i substituujeme xi/xi). Formule B je instancí formule A, jestliže existuje substituce s taková, že B = As. DEFINICE 9-6 UNIFIKACE Unifikace (unifikační substituce, unifikátor) formulí A, B je substituce s taková, že As = Bs. DEFINICE 9-7 NEJOBECNĚJŠÍ UNIFIKACE Nejobecnější unifikace formulí A, B je unifikace s taková, že pro každou jinou unifikaci r formulí A, B platí r = st, kde t ¹ e, tj. každá unifikace vznikne z nejobecnější unifikace provedením další dodatečné substituce. VĚTA 9-4 ROBINSON: ZOBECNĚNÉ REZOLUČNÍ ODVOZOVACÍ PRAVIDLO Nechť Ai, Bi, Li jsou atomické formule predikátové logiky. Potom platí následující odvozovací pravidlo: A1 Ú...Ú Am Ú L1, B1 Ú...Ú Bn Ú ¬L2 |– A1s Ú...Ú Ams Ú B1s Ú...Ú Bns , kde s je unifikace formulí L1, L2, tj. L1s = L2s. Klauzule na levé straně odvozovacího pravidla nazýváme rodičovskýmí klauzulemi a klauzuli na pravé straně rezolventou. Formule AS v klausulární formě je nesplnitelná, právě když z ní lze opakovaným použitím obecného pravidla rezoluce odvodit prázdnou klausuli. Speciální případy rezolučního odvozovacího pravidla (předpokládáme L1s = L2s): • m = 0, n = 0: L1, ¬L2 |– odvození sporu • m = 0, n = 1: L1, ¬L2 Ú B |– Bs pravidlo MP • m = 1, n = 1: L1 Ú A, ¬L2 Ú B |– As Ú Bs základní tvar rez. pravidla doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 94 Unifikace s formulí L1, L2 může být jakákoliv, chceme-li však vyvodit z předpokladů (rodičovských klauzulí) nejobecnější závěr (rezolventu) je třeba použít nejobecnější uni- fikaci. ŘEŠENÝ PŘÍKLAD 9-4 Dokážeme správnost úsudku (analytickou pravdivost věty): Jistý filosof odporuje všem filosofům, tedy odporuje sám sobě. Řešení příkladu Větu analyzujeme jako („zamýšlená” interpretace je nad množinou individuí, p ® podmnožina filosofů, q ® relace, ve které budou ty dvojice, kde první odporuje druhému) $x {[p(x) & "y (p(y) ® q(x,y))] ® q(x,x)} Formuli znegujeme a převedeme na klausulární tvar: "x "y {p(x) & [¬p(y) Ú q(x,y)] & ¬q(x,x)}. K jednotlivým klausulím 1. p(x) 2. ¬p(y) Ú q(x,y) 3. ¬q(x,x) je nejobecnějším unifikátorem substituce {y/x}: 4. q(x,x) z 1. a 2. 5. z 3. a 4. * ŘEŠENÝ PŘÍKLAD 9-5 Dokažme správnost úsudku: Kdo zná Pavla a Marii, ten Marii lituje. Někteří nelitují Marii, ačkoli ji znají. ––––––––––––––––––––––––––––––– Někdo zná Marii, ale ne Pavla. 959 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Řešení příkladu Kdo zná Pavla a Marii, ten Marii lituje. "x ([Z(x, P) & Z(x, M)] ®L(x, M)) Někteří nelitují Marii, ačkoli ji znají. $x [¬L(x, M) & Z(x, M)] ––––––––––––––––––––––––––––––– Někdo zná Marii, ale ne Pavla. $x [Z(x, M) & ¬Z(x, P)] "x [¬Z(x, P) Ú ¬Z(x, M) Ú L(x, M)] odstranění implikace (1. předpoklad) ¬L(a, M) & Z(a, M) Skolemizace (2. předpoklad) "y [¬Z(y, M) Ú Z(y, P)] negovaný závěr (přejmenování x) Klausule: 1. ¬Z(x, P) Ú ¬Z(x, M) Ú L(x, M) 2. ¬L(a, M) 3. Z(a, M) 4. ¬Z(y, M) Ú Z(y, P) 5. ¬Z(a, P) Ú ¬Z(a, M) rezoluce 1., 2., substituce x/a 6. ¬Z(a, P) rezoluce 3., 5. 7. ¬Z(a, M) rezoluce 4., 6., substituce y/a 8. rezoluce 3., 7. * ŘEŠENÝ PŘÍKLAD 9-6 Dokažme správnost úsudku: Všichni členové vedení jsou majiteli obligací nebo akcionáři. Žádný člen vedení není zároveň majitel obligací i akcionář. Všichni majitelé obligací jsou členy vedení. Žádný majitel obligací není akcionář. Řešení příkladu "x [v(x) ® (o(x) Ú a(x))] "x [v(x) ® ¬(o(x) & a(x))] "x [o(x) ® v(x)] ––––––––––––––––––––– "x [o(x) ® ¬a(x)] Klausule: 1. ¬v(x) Ú o(x) Ú a(x) 1. Předpoklad 2. ¬v(x) Ú ¬o(x) Ú ¬a(x) 2. Předpoklad 3. ¬o(x) Ú v(x) 3. Předpoklad 4. o(k) negovaný závěr 5. a(k) (po Skolemizaci) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 96 6. ¬o(x) Ú ¬a(x) rezoluce 2., 3. 7. ¬a(k) rezoluce 4., 6., substituce x/k 8. rezoluce 5., 7. * ŘEŠENÝ PŘÍKLAD 9-7 Dokažme správnost úsudku: Všichni členové vedení jsou majiteli obligací nebo akcionáři. Žádný člen vedení není zároveň majitel obligací i akcionář. Všichni majitelé obligací jsou členy vedení. –––––––––––––––––––––––––––––––––––––––––––––––– Žádný majitel obligací není akcionář. Řešení příkladu "x [v(x) ® (o(x) Ú a(x))] "x [v(x) ® ¬(o(x) & a(x))] "x [o(x) ® v(x)] ––––––––––––––––––––– "x [o(x) ® ¬a(x)] Klausule: 1. ¬v(x) Ú o(x) Ú a(x) 1. Předpoklad 2. ¬v(x) Ú ¬o(x) Ú ¬a(x) 2. Předpoklad 3. ¬o(x) Ú v(x) 3. Předpoklad 4. o(k) negovaný závěr 5. a(k) (po Skolemizaci) 6. ¬o(x) Ú ¬a(x) rezoluce 2., 3. 7. ¬a(k) rezoluce 4., 6., substituce x/k 8. rezoluce 5., 7. * 979 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky ŘEŠENÝ PŘÍKLAD 9-8 Dokažme správnost úsudku: Každý, kdo má rád Jiřího, bude spolupracovat s Milanem. Milan nekamarádí s nikým, kdo kamarádí s Láďou. Petr bude spolupracovat pouze s kamarády Karla. Jestliže Karel kamarádí s Láďou, pak Petr nemá rád Jiřího. Řešení příkladu "x [R(x, J) ® S(x, M)] "x [K(x, L) ® ¬K(M, x)] "x [S(P, x) ® K(x, Kr) –––––––––––––––––––– K(Kr, L) ® ¬R(P, J) Klausule: 1. ¬R(x, J) Ú S(x, M) 1. předpoklad 2. ¬K(y, L) Ú ¬K(M, y) 2. předpoklad 3. ¬S(P, z) Ú K(z, Kr) 3. předpoklad 4. K(Kr, L) negovaný 5. R(P, J) závěr 6. ¬K(M, Kr) rezoluce 4., 2., substituce y/Kr 7. ¬S(P, M) rezoluce 3., 6., substituce z/M 8. ¬R(P, J) rezoluce 1., 7., substituce x/P 9. rezoluce 5., 8. * ŘEŠENÝ PŘÍKLAD 9-9 Dokažme správnost úsudku: Každý muž má rád fotbal a pivo. Xaver má rád pouze milovníky fotbalu a piva. Někteří milovníci fotbalu nemají rádi pivo. ––––––––––––––––––––––––––––––––––––– Některé ženy nemá Xaver rád. Řešení příkladu "x [M(x) ® (R(x,f) Ù R(x,p))] 1. předpoklad "x [R(Xa,x) ® (R(x,f) Ù R(x,p))] 2. předpoklad $x [R(x,f) Ù ¬R(x,p)] 3. předpoklad doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 98 "x [M(x) Ú R(Xa,x)] negovaný závěr: $x [¬M(x) Ù ¬R(Xa,x)], (žena = není muž) Klausule: 1. ¬M(x) Ú (R(x,f) 2. ¬M(x) Ú (R(x,p) 3. ¬R(Xa,y) Ú (R(y,f) 4. ¬R(Xa,y) Ú (R(y,p) 5. R(k,f) 6. ¬R(k,p) 7. M(z) Ú R(Xa,z) –––––––––––––––––– 8. ¬R(Xa,k) rezoluce 4., 6. (y/k) 9. M(k) rezoluce 7., 8. (z/k) 10. R(k,p) rezoluce 2., 9. (x/k) 11. rezoluce 6., 10. * KONTROLNÍ OTÁZKA 8 1. Srovnejte rezoluční princip ve výrokové logice a v predikátové logice. 2. Popište použití rezolučního principu v predikátové logice. CVIČENÍ 8 Příklad 1: Pomocí rezoluční metody ověřte platnost úsudků • Nikdo, kdo trpí klaustrofobií nemůže pracovat jako liftboy. Všichni horolezci trpí klaustrofobií. -------------------------------------------------- Proto žádný horolezec nemůže pracovat jako liftboy. • Všechny dřevěné stoly jsou stoly. Všechny dřevěné stoly jsou ze dřeva. -------------------------------------------------- Některé stoly jsou ze dřeva. • Všechny muchomůrky zelené jsou jedovaté. Tato tužka je muchomůrka zelená. -------------------------------------------------- Tato tužka je jedovatá. 999 Automatické dokazování v predikátové logice (obecná rezoluční metoda) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky • Každý, kdo miluje jachting a moře, cítí k moři respekt. Někteří respekt k moři necítí, ačkoli ho milují. -------------------------------------------------- Zřejmě existují takoví, kteří milují moře, ale nikoliv jachting. • Každý někomu pije krev. Komu pije krev Drákula, ten brzo zemře. -------------------------------------------------- Někdo brzo zemře. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 100 10 SÉMANTICKÉ TABLO, AXIOMATICKÝ SYSTÉM PREDIKÁTOVÉ LOGIKY ČAS POTŘEBNÝ KE STUDIU Celkový doporučený čas k prostudování KAPITOLY je 90 minut. RYCHLÝ NÁHLED DO PROBLEMATIKY KAPITOLY SÉMANTICKÉ TABLO, AXIOMATICKÝ SYSTÉM PREDIKÁTOVÉ LOGIKY Cílem desátého modulu je možnost využití sémantické tabla při rozhodování splnitelnosti v predikátové logice a zavedení axiomatický systémů predikátové logiky a to Hilbertovského a Gentzenovského. Rychlý ná- hled KLÍČOVÁ SLOVA KAPITOLY SÉMANTICKÉ TABLO, AXIOMATICKÝ SYSTÉM PREDIKÁTOVÉ LOGIKY Sémantické tablo, Hilbertovský axiomatický systém, Gentzenovský axiomatický sys- tém. Klíčová slova 10.1 Rozhodování splnitelnosti formulí sémantickými tably Sémantické tablo formule A jazyka L predikátové logiky je konečný ohodnocený binární strom, jehož všechny uzly jsou označeny návěštími – sekvencemi formulí A, tak, že platí: Listy jsou označeny sekvencemi literálů proměnných vyskytujících se ve formuli A. Jestliže je uzel označen sekvencí formulí X1, X2, …, a, …, Xn obsahující jako člen formuli typu alfa, pak jediný uzel bezprostředně následující je označen sekvencí X1, X2, …., a1, a2, …., Xn obsahující formule a1, a2. 10110 Sémantické tablo, axiomatický systém predikátové logiky doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky a-pravidla: a a 1 a 2 ¬¬A A A 1 &A 2 A 1 A 2 ¬(A 1 ÚA 2 ) ¬A 1 ¬A 2 ¬(A 1 ®A 2 ) A 1 ¬A 2 ¬(A 1 ¬A 2 ) ¬A 1 A 2 A 1 «A 2 A 1 ®A 2 A 2 ®A 1 Jestliže je uzel označen sekvencí formulí X1, X2, …, b, …, Xn obsahující jako člen formuli typu b, pak dvojice uzlů bezprostředně následujících je označena sekvencemi X1, X2, …, b1, …, Xn a X1, X2, …, b2, …, Xn obsahujícími po řadě formule b1, b2. b - pravidla: b b 1 b 2 B 1 ÚB 2 B 1 B 2 ¬(B 1 &B 2 ) ¬B 1 ¬B 2 B 1 ®B 2 ¬B 1 B 2 B 1 ¬B 2 B 1 ¬B 2 ¬(B 1 «B 2 ) ¬(B 1 ®B 2 ) ¬(B 2 ®B 1 ) Jestliže je uzel označen sekvencí formulí X1, X2, …, g, …, Xn obsahující jako člen formuli typu g pak jediný uzel bezprostředně následující je označen sekvencí X1, X2, …, g, g(a) …, Xn obsahující původní formuli g a její instanci g(a) přičemž a je konstanta vyskytující se již v jazyce. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 102 g - pravidla pro univerzální formule: g g(a) "xA(x) "xA(x), A(a) ¬$xA(x) ¬$xA(x),¬A(a) Jestliže je uzel označen sekvencí formulí X1, X2, …, d, …, Xn obsahující jako člen formuli typu d, pak jediný uzel bezprostředně následující je označen sekvencí X1, X2, …, d,d(a) …, Xn obsahující instanci d(a) formule d přičemž a je nová konstanta nevyskytující se dosud v jazyce. d - pravidla pro existenční formule: d d(a) $xA(x) A(a) ¬"xA(x) ¬A(a) Návěštím kořene sémantického tabla je formule A. Pravidla pro rozhodnutí zda větev stromu je uzavřená a otevřená jsou stejná jako u sémantického tabla ve výrokové logice. Stejný princip použijeme i při rozhodování zdali formule je splnitelná, tautologie či kontradikce. Nesmíme opět zapomenout, že pro důkaz, že formule je tautologií, musíme pracovat s negovanou formulí a dokazujeme nesplnitelnost negované formule a tím pádem původní formule je tautologií. ŘEŠENÝ PŘÍKLAD 10-1 Rozhodněte o splnitelnosti formule pomocí sémantického tabla ¬("x(p(x) ® q(x)) ® ($x p(x) ® $ x q(x))) 10310 Sémantické tablo, axiomatický systém predikátové logiky doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Řešení příkladu ¬("x(p(x) ® q(x)) ® ($x p(x) ® $ x q(x))) 2x aplikujeme alfa pravidlo pro negaci implikace ½ "x(p(x) ® q((x)), ¬($xp(x)®$x q(x)) ½ "x(p(x) ® q(x)), $xp(x), ¬$xq(x) ½ "x(p(x) ® q(x)), p(a) ® q(a), p(a), ¬$xq(x), ¬q(a) ½ "x(p(x) ® q(x)), ¬$xq(x), ¬p(a), p(a), ¬q(a) "x(p(x) ® q(x)), ¬$xq(x), q(a), p(a), ¬q(a) Obě větve jsou uzavřeny, z čehož lze učinit závěr, že formule je nesplnitelná. * 10.2 Formální systém (logický kalkul) Hilbertova typu DEFINICE 10-1 AXIOMATICKÝ SYSTÉM HILBERTOVA TYPU definice axiomatického systému Hilbertova typu • Jazyk: Viz definice dříve s jedinou výjimkou: množina funktorů je omezena na funktory ¬, ®, ". • Axiómová schémata: A1: A ® (B ® A) A2: (A ® (B ® C)) ® ((A ® B) ® (A ® C)) A3: (¬B ® ¬A) ® (A ® B) A4: axióm specifikace "xA(x) ® A(x/t), term t je substituovatelný za x v A A5: axióm kvantifikace implikace ("x[A ® B(x)]) ® (A ® "xB(x)), x není volná v A • Odvozovací pravidla: MP: A, A É B |– B (pravidlo odloučení, modus ponens) (Z dokazatelných formulí A, A ® B odvoď formuli B. G: A |– "xA (pravidlo generalizace) (Pro libovolnou volně se vyskytující proměnnou x ve formuli odvoď z formule A formuli "xA) doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 104 Důkaz je konečná posloupnost kroků – dobře utvořených formulí (DUF) dle gramatiky jazyka, z nichž každá je buď axióm nebo vznikne z předchozích DUF pomocí odvozovacího pravidla. Posledním krokem je dokazovaná formule – teorém. Volba axiómů není pochopitelně zcela libovolná; aby byl systém ”rozumný”, tedy korektní, podléhá dvěma kritériím: • Každý axióm je tautologie • Množina axiómů musí umožňovat, aby se z nich daly odvodit všechny logicky platné formule a přitom je rozumné, aby tato množina byla minimální, tedy žádný axióm není dokazatelný z jiných axiómů – nezávislá množina axiómů. Rovněž volba odvozovacích pravidel není libovolná. Aby byl systém korektní, musí pravidla ‘zachovávat pravdivost‘ v tom smyslu, že formule, kterou podle pravidla obdržíme, je pravdivá alespoň ve všech modelech předpokladů pravidla, tedy z těchto předpokladů vyplývá. Tedy pro každé pravidlo A1,…,An |– B by mělo platit, že A1,…,An |= B. Pravidlo generalizace A(x) |– "xA(x) však zjevně tento požadavek obecně nesplňuje, formule A(x) ® "xA(x) není tautologie. Přesto je Hilbertův kalkul korektní systém a formuli A(x) ® "xA(x) v něm nedokážeme. Jak je to možné? Intuitivní zdůvodnění tohoto pravidla je : Máme-li dokázat nějakou vlastnost pro všechny objekty, je možno ji dokázat na jednom libovolně vybraném (při důkazu však nesmíme používat žádných dalších specifických vlastností tohoto objektu). Vzpomeňme si, jak jsme prováděli ve škole např. důkazy v geometrii. Nakreslíme libovolný trojúhelník a pro tento trojúhelník provedeme nějakou konstrukci, jejíž pomocí dokážeme zkoumanou vlastnost (tohoto) trojúhelníka, a protože to byl trojúhelník libovolný, prohlásíme, že tuto vlastnost mají všechny trojúhelníky. Musíme si však dát pozor, aby zvolený trojúhelník byl skutečně libovolný, tedy aby neměl nějakou další vlastnost, třeba rovnoramenný, protože takovéto specifické vlastnosti nesmíme – ani podvědomě – v důkazu využít. Jinak bychom naše tvrzení dokázali pouze pro všechny rovnoramenné trojúhelníky. VĚTA 10-1 O DEDUKCI Pro uzavřenou formuli A a libovolnou formuli B platí: |– A ® B právě tehdy, když A |– B. 10510 Sémantické tablo, axiomatický systém predikátové logiky doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky VĚTA 10-2 O KOKEKTNOSTI Každá dokazatelná formule predikátové logiky (tj. teorém kalkulu Hilbertova typu) je také tautologií predikátové logiky. Formálně: Jestliže |– A, pak |= A. Důkaz /nástin/: ¨ Všechny formule, které obdržíme z axiómových schémat A1–A5 jsou tautologiemi, tedy jsou pravdivé v každé interpretační struktuře I (při libovolné valuaci e volných proměnných). Korektnost pravidla MP (modus ponens) byla demonstrována v důkazu Postovy věty. Korektnost pravidla generalizace A(x) |– "xA(x) je zaručena definicí splňování formule "xA ve struktuře I. Předpokládejme, že jsme v důkazové posloupnosti dosud pravidlo generalizace nepoužili. Tedy formule A(x) musí být tautologií (neboť mohla vzniknout z axiómů – tautologií pouze použitím pravidla MP, které zachovává pravdivost). To znamená, že v libovolné struktuře I platí, že |=I A(x)[e] – formule A(x) je pravdivá v I pro libovolné ohodnocení e proměnné x. Tedy platí pro libovolné individuum i Î M, kde M je universum zvolené v interpretační struktuře I, že formule A je pravdivá v I pro valuaci, která přiřazuje individuum i proměnné x, tedy |= I A[e(x/i)], kde e(x/i) je valuace stejná jako e až na to, že přiřazuje proměnné x individuum i. Tedy formule "xA(x) je pravdivá v I, |=I "xA(x). Pravidlo generalizace je korektní v tom smyslu, že zachovává pravdivost formule v interpretaci. VĚTA 10-3 O SÉMANTICKÉ ÚPLNOSTI AXIOMATICKÉHO SYSTÉMU - K. GÖDEL Každá tautologie predikátové logiky je dokazatelná (v logickém kalkulu Hilbertova typu). Formálně, je-li |= A pak |– A. VĚTA 10-4 Nechť A, B jsou formule predikátové logiky. Je-li |- A ® B a proměnná x nemá žádný volný výskyt ve formuli A, pak |- A ® "x B. Důkaz : 1. A ® B |- A ® B předpoklad 2. A ® B |- "x(A ® B) generalizace na 1. 3. |- "x(A ® B) ® (A ® "xB) schéma kvantifikace implikace 4. A ® B |- A ® "xB modus ponens na 2. a 3. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 106 10.3 Gentzenovský axiomatický systém DEFINICE 10-2 LOGICKÝ AXIOM Logickým axiómem gentzenovského axiómatického systému G1 predikátové logiky je množina (sekvence) U formulí obsahující komplementární pár literálů {p(x1, x2, ...xn), ¬p(x1, x2, ...xn), } ® U některé atomické formule p(x1, x2, ...xn). Odvozovací pravidla jsou rovněž téměř beze změn přenesena z G do základu gentzenovského formálního systému G1 predikátové logiky. Odvozovací pravidla a a b systému G1 jsou zde rovněž definována metajazykově, a to příslušnými schématy a tabulkami. Navíc jsou zde pravidla g a d pro formule s kvantifikátory určená metajazykovými schématy. DEFINICE 10-3 Odvozovacími pravidly gentzenovského axiómatického systému G1 jsou : a) a - pravidla daná schématem U È{ a1, a2 } U È{a}. b) b - pravidla daná schématem U1 È{b1} U2 È{b2} U1 È U2 È {b} c) g - pravidla daná schématy U È { $x A(x), A(a)} U È {$x A(x)} U È {¬"x A(x),¬A(a)} U È {¬"x A(x)} d) d - pravidla daná schématy U È {A(a)} U È {"x A(x)} U È {¬A(a)} U È {¬$x A(x)}, 10710 Sémantické tablo, axiomatický systém predikátové logiky doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky kde A(x) je formule. a a 1 a 2 A ¬¬A A 1 Ú A 2 A 1 A 2 ¬(A 1 & A 2 ) ¬ A 1 ¬ A 2 A 1 ® A 2 ¬ A 1 A 2 A 1 ¬ A 2 A 1 ¬ A 2 ¬(A 1 « A 2 ) ¬(A 1 ® A 2 ) ¬(A 1 ¬A 2 ) b b 1 b 2 B 1 & B 2 B 1 B 2 ¬(B 1 Ú B 2 ) ¬ B 1 ¬ B 2 ¬(B 1 ® B 2 ) B 1 ¬ B 2 ¬(B 1 ¬ B 2 ) ¬ B 1 B 2 B 1 « B 2 B 1 ® B 2 B 2 ® B 1 ŘEŠENÝ PŘÍKLAD 10-2 a) Dokažte pomocí sémantického tabla logickou platnost formule ("x p(x) Ú "x q(x)) ® "x (p(x) Ú q(x)) b) Proveďte gentzenovský důkaz této formule. Řešení příkladu ¬("x p(x) Ú "x q(x)) ® "x (p(x) Ú q(x)) ("x p(x) Ú "x q(x)), ¬"x (p(x) Ú q(x)) "x p(x), ¬"x (p(x) Ú q(x)) "x q(x), ¬"x (p(x) Ú q(x)) "x p(x), $x ¬(p(x) Ú q(x)) "x q(x), $x ¬(p(x) Ú q(x)) "x p(x), ¬(p(a) Ú q(a)) "x q(x), ¬(p(a) Ú q(a)) "x p(x), ¬p(a), ¬q(a) "x q(x), ¬p(a), ¬q(a) "x p(x), p(a), ¬p(a), ¬q(a) "x q(x), q(a), ¬p(a), ¬q(a) Vytvoříme důkazový strom dané formule jako duální strom k sémantickému stromu, formule konstruovaný v obráceném pořadí jeho uzlů. Protože v případě duálního stromu čárky mezi podformulemi představují jejich disjunkci a větvení doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 108 konjunkci, stačí při konstrukci duálního stromu zdola nahoru negovat všechny podformule obsažené v návěštích jeho uzlů. ¬"x p(x), ¬p(a), p(a), q(a) ¬"x q(x), ¬q(a), p(a), q(a) ¬"x p(x), p(a), q(a) ¬"x q(x), p(a), q(a) ¬"x p(x), (p(a) Ú q(a)) ¬"x q(x), (p(a) Ú q(a)) ¬"x p(x), "x (p(x) Ú q(x)) ¬"x q(x), "x (p(x) Ú q(x)) Ø("x p(x) Ú "x q(x)), "x (p(x) Ú q(x)) ("x p(x) Ú "x q(x)) ® "x (p(x) Ú q(x)) Důkaz formule : 1. ¬"x p(x), ¬p(a), p(a), q(a) axióm 2. ¬"x p(x), p(a), q(a) g - pravidlo na 1. 3. ¬"x p(x), (p(a) Ú q(a)) a Ú na 2. 4. ¬"x p(x), "x (p(x) Ú q(x)) d - pravidlo na 3. 5. ¬"x q(x), ¬q(a), p(a), q(a) axióm 6. ¬"x q(x), p(a), q(a) g - pravidlo na 5. 7. ¬"x q(x), (p(a) Ú q(a)) a Ú na 6. 8. ¬"x q(x), "x (p(x) Ú q(x)) d - pravidlo na 7. 9. ¬("x p(x) Ú "x q(x)), "x (p(x) Ú q(x)) b Ú na 4. a 8. 10. ("x p(x) Ú "x q(x)) ® "x (p(x) Ú q(x)) a ® na 9. * Způsob, jakým byl důkaz formule sestrojen (využitím duality) ukazuje, že gentzenovské důkazy logicky platných predikátových formulí nebývají tak obtížné, jako tomu bylo v případě hilbertovských důkazů. Ze způsobu řešení uvedeného příkladu lze též usoudit, že zde zavedený gentzenovský axiómatický systém predikátové logiky je sémanticky korektní a úplný, neboť platí ná- sledující. VĚTA 10-5 Gentzenovský důkaz formule A predikátové logiky existuje, právě když se sémantické tablo formule ¬A uzavře. 10910 Sémantické tablo, axiomatický systém predikátové logiky doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky DEFINICE 10-4 DŮKAZ FORMULE V G1 Důkaz formule A z množiny speciálních axiómů U v gentzenovském axiómatickém systému G1 predikátové logiky je posloupnost sekvencí formulí taková, že každá sekvence je buď logickým axiómem v G1 nebo speciálním axiómem nebo je odvozena z jednoho nebo dvou předcházejících členů posloupnosti pomocí některého z odvozovacích pravidel a, b, g, d systému G1. Je-li formule A posledním prvkem posloupnosti, nazývá se posloupnost důkazem formule A a samotná formule A větou větou teorie T(U) dokazatelnou z U v systému G1. ŘEŠENÝ PŘÍKLAD 10-3 Dokažte ze speciálních axiómů p(x) ® q(x), p(x) větu q(x) (pravidlo modus ponens systému H1). Řešení příkladu 1. p(x) ® q(x) |- p(x) ® q(x) první předpoklad 2. p(x) ® q(x) |- ¬p(x), q(x) přepis prvního předpokladu 3. p(x) |- p(x) druhý předpokla 4. p(x) ® q(x), p(x) |- p(x) & ¬p(x), q(x) b & na 3. 5. p(x) ® q(x), p(x) |- q(x) vynechání nesplnitelné konjunkce * VĚTA 10-6 Formule dokazatelné v gentzenovském axiomatickém systému predikátové logiky jsou právě logicky platné formule. Důkaz /nástin/: Důkaz korektnosti axiomatického gentzenovského axiomatického systému predikátové logiky, tzn., že jestliže formule je dokazatelná, pak je logicky platná dokážeme indukcí: Důkaz obsahující jeden axióm systému, je v podstatě logicky platnou disjunkcí Nechť indukční předpoklad platí až do délky důkazu n. Potom n+1-ní člen důkazové posloupnosti seznamů formulí může vzniknout tak, že na jeden důkazový řádek je aplikováno pravidlo a, g nebo d nebo je na dva řádky aplikováno pravidlo b. Ve všech těchto případech jsou tak vygenerovány seznamy, jimž odpovídají logicky platné formule nebo jde o logické důsledky, které zachovávají jejich modely. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 110 Důkaz úplnosti gentzenovského axiomatického systému: Je-li formule A logicky platná, je její negace nesplnitelná, z čehož vyplývá existence uzavřeného sémantická tabla negované formule. Existuje pak důkaz formule v gentzenovském systému. KONTROLNÍ OTÁZKA 9 1. Popište postup při použití sémantického tabla při dokazování splnitelnosti v predikátové logice. 2. Definujte Hilbertovský axiomatický systém predikátové logiky. 3. Definujte Gentzenovský axiomatický systém predikátové logiky. 11111 Tradiční Aristotelova logika doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 11 TRADIČNÍ ARISTOTELOVA LOGIKA ČAS POTŘEBNÝ KE STUDIU Celkový doporučený čas k prostudování KAPITOLY je 90 minut. RYCHLÝ NÁHLED DO PROBLEMATIKY KAPITOLY TRADIČNÍ ARISTOTELOVA LOGIKA Cílem jedenáctého modulu je popsání tradiční logiky od Aristotela. Rychlý ná- hled KLÍČOVÁ SLOVA KAPITOLY TRADIČNÍ ARISTOTELOVA LOGIKA Tradiční Aristotelova logika, sylogismus. Klíčová slova Tradiční Aristotelova logika je fragment predikátové logiky 1. řádu, který je omezen pouze na jednomístné predikáty. Tato logika byla (v podstatě jako jediná) vyučována ještě v 19. století. Umožňuje kontrolovat správnost zvláštního typu jednoduchého úsudku, který se nazývá kategorický sylogismus. Tyto úsudky zkoumal před více než 2000 lety řecký filosof a zakladatel logiky Aristoteles. Aristotelova logika vznikla kupodivu dříve než výroková logika, kterou zkoumali stoici. Stoici byli v jisté opozici vůči Aristotelovi a z jejich díla se zachovaly jen fragmenty, ze kterých je však zjevné, že používali rozvinutý systém výrokové logiky a v podstatě (i když poněkud v jiné formě) i systém predikátové logiky 1. řádu. Aristotelova logika zkoumá tzv. subjekt – predikátové výroky (S-P výroky), kde S i P jsou nějaké vlastnosti (formalizované jako predikáty). Tyto výroky dělíme na obecné a částečné, kladné a záporné. Všechny možnosti a jejich vzájemný vztah jsou znázorněny logickým čtvercem, kde význam zkratek je odvozen z latinského affirmo (tvrdím) a nego (popírám): • SaP – Všechna S jsou P • SeP – Žádné S není P • SiP – Některá S jsou P • SoP – Některá S nejsou P doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 112 Logický čtverec znázorňuje jednoduché úsudky platné mezi těmito výroky. 1. Kontradiktorické (protikladné, jeden je vždy ekvivalentní negaci druhého): SaP º ¬SoP SeP º ¬SiP 2. Kontrární (z jednoho vyplývá negace druhého): SaP |= ¬SeP SeP |= ¬SaP Může však být zároveň nepravda jak SaP tak SeP (tedy ani Sap ani Sep není pravda): Všechny houby jsou jedlé, všechny houby jsou nejedlé. 3. Subkontrární (podprotivné): ¬SiP |= SoP ¬SoP |= SiP Může však být SiP i SoP pravdivé: Některé labutě jsou černé, některé labutě nejsou černé 4. Subalterní (podřízený): SaP |= SiP SeP |= Sop ¬SiP |= ¬SaP ¬SoP |= ¬SeP 5. Dále platí tzv. obraty: SiP |= PiS SeP |= PeS Někteří studenti jsou ženatí |= Někteří ženatí jsou studenti Žádný člověk není strom |= Žádný strom není člověk SaP |= PiS SeP |= PoS Všichni učitelé jsou státní zaměstnanci |= Někteří státní zaměstnanci jsou učitelé Žádné jedovaté houby nejsou jedlé |= Některé jedlé houby nejsou jedovaté Sylogismy jsou úsudky, které sestávají ze tří S-P výroků tvaru (4 figury): Kombinací a, e, i, o lze nyní vytvořit 64 tzv. modů, z nichž jen některé jsou platné. Platné módy se pochopitelně neučíme nazpaměť (jako to kdysi dělali naši otcové), neboť jejich platnost můžeme snadno ověřit i sémanticky, na základě množinových úvah, které můžeme znázornit geometricky (např. metodou známých Vénových kroužků). Obrázek 4 Logický čtverec 11311 Tradiční Aristotelova logika doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky Obory pravdivosti predikátů S, P, M zakreslíme jako (vzájemně se protínající) kroužky. Poté znázorníme situaci, kdy jsou premisy pravdivé, tj. vyšrafujeme plochy, které odpovídají prázdným třídám objektů. Označíme křížkem plochy, které jsou jistě neprázdné (křížek přitom klademe jen tehdy, když neexistuje jiná plocha, ”kam by mohl přijít”). Nakonec ověříme, zda vzniklá situace znázorňuje pravdivost závěru. Příklad správného úsudku: Všechny velryby jsou savci. Někteří vodní živočichové jsou velryby. U1 –––––––––––––––––––––––––––––– Někteří vodní živočichové jsou savci. Příklad nesprávného úsudku: Žádný učený z nebe nespadl Všechno co spadlo z nebe je voda U2 ––––––––––––––––––––––––––– Žádná voda není učená. KONTROLNÍ OTÁZKA 10 Popište Aristotelovu logiku. doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 114 DALŠÍ ZDROJE 1. BAADER, F., CALVANESE, D., MCGUINNESS, D. L., NARDI, D., PATELSCHNEIDER, P. F. The Description Logic Handbook – Theory, implimentation, and applications, Cambridge university press 2010, ISBN 978-0-521-150011-8 2. CHURCH, A. Introduction to Mathematical Logic. Princeton University Press, 1956. 3. IRVING M. COPI, CARL COHEN, KENNETH MCMAHON Introduction to Logic. 14 th Editon, Published by Routledge Taylor & Francis (2017), ISBN 10: 9332539618 ISBN 13: 9789332539617 4. JIRKŮ, P., VEJNAROVÁ, J. Logika-Neformální výklad základů formální logiky (2. přepracované a doplněné vydání). Praha: Univerzita Karlova, 2000. 5. JONES, A. Logic and Knowledge Reprentation and introduction for systems analysts. Pitman Publishing 1991. ISBN 0 273 03150 3 6. LUKASOVÁ, A. Formální logika v umělé inteligenci. Computer Press, Brno, 2003. ISBN 80-251-0023-5 7. LUKASOVÁ, A. Logické základy umělé inteligence 1. Výroková a predikátová logika (2. přepracované vydání). Ostrava: Ostravská univerzita, 1999. 8. SOCHOR, A. Klasická matematická logika. Praha: Univerzita Karlova, 2001. 9. ŠTĚPÁNEK, P. Matematická logika. Praha: Univerzita Karlova, 2000. 10. ŠVEJDAR, V. Logika: neúplnost, složitost a nutnost. Praha: Academia, 2002. ISBN 80-200-1005-X. ONLINE ZDROJE 1. ŠTĚPÁNEK, P: Predikátová logika, Praha, 2000. http://ktiml.mff.cuni.cz/ktiml/teaching/files/materials/StepanekPetr_PredikatovaLogika.pdf ověřeno: 15. 9. 2017 2. DUŽÍ, M.: Logika pro informatiky (a příbuzné obory), VŠB-TU Ostrava 2012. http://www.cs.vsb.cz/duzi/Matlogika_ESF_Definite.pdf ověřeno: 15. 9. 2017 3. DUŽÍ, M.: Matematická logika, VŠB-TU Ostrava, 2003. http://www.cs.vsb.cz/duzi/Matlogika_Vyber.pdf ověřeno: 15. 9. 2017 4. ŠVEJDAR, V.: Logika: neúplnost, složitost a nutnost, Praha: Academia, 2002. http://www1.cuni.cz/~svejdar/book/LogikaSve2002.pdf ověřeno: 15. 9. 2017 5. JIRKŮ, P., VEJNAROVÁ, J.: Logika-Neformální výklad základů formální logiky (2. přepracované a doplněné vydání). Praha: Univerzita Karlova, 2000. https://peter.smolinsky.sk/cms/files/52/jirku-logika2.pdf ověřeno: 15. 9. 2017 6. STARÝ, J.: Úvod do matematické logiky. FIT ČVUT, 2017. https://users.fit.cvut.cz/~staryja2/BIMLO/matematicka-logika.pdf ověřeno: 15. 9. 2017 7. HROMEK, P. : Logika v příkladech. Univerzita Palackého v Olomouci, Olomouc, 2002. https://users.fit.cvut.cz/~staryja2/BIMLO/matematicka-logika.pdf ověřeno: 15. 9. 2017 8. PEREGRIN, J.: Logika a logiky – Systém klasické výrokové logiky, jeho rozšíření a alternativy, 2004. http://jarda.peregrin.cz/mybibl/PDFTxt/455.pdf Ověřeno: 15. 9. 2017 11512 Klasifikace zdrojů doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 9. KVASNIČKA, V., POSPÍCHAL, J.: Matematická logika, Slovenská technická univerzita v Bratislave 2006. http://www2.fiit.stuba.sk/~kvasnicka/Free%20books/Matematicka%20Logika_all.pdf ověřeno: 15. 9. 2017 12 KLASIFIKACE ZDROJŮ Doporučená literatura: 1. CIENCIALA, L.: Opory k předmětům: Úvod do logiky/Logika, 2017. 2. LUKASOVÁ, A. Formální logika v umělé inteligenci. Computer Press, Brno, 2003. ISBN 80-251-0023-5 3. LUKASOVÁ, A. Logické základy umělé inteligence 1. Výroková a predikátová logika (2. přepracované vydání). Ostrava: Ostravská univerzita, 1999. 4. JIRKŮ, P., VEJNAROVÁ, J. Logika-Neformální výklad základů formální logiky (2. přepracované a doplněné vydání). Praha: Univerzita Karlova, 2000. 5. ŠVEJDAR, V. Logika: neúplnost, složitost a nutnost. Praha: Academia, 2002. ISBN 80-200-1005-X. http://www1.cuni.cz/~svejdar/book/LogikaSve2002.pdf ověřeno: 15. 9. 2017 6. DUŽÍ, M.: Logika pro informatiky (a příbuzné obory), VŠB-TU Ostrava 2012. http://www.cs.vsb.cz/duzi/Matlogika_ESF_Definite.pdf ověřeno: 15. 9. 2017 Rozšiřující literatura: 1. DUŽÍ, M.: Matematická logika, VŠB-TU Ostrava, 2003. http://www.cs.vsb.cz/duzi/Matlogika_Vyber.pdf ověřeno: 15. 9. 2017 2. STARÝ, J.: Úvod do matematické logiky. FIT ČVUT, 2017. https://users.fit.cvut.cz/~staryja2/BIMLO/matematicka-logika.pdf ověřeno: 15. 9. 2017 3. HROMEK, P. : Logika v příkladech. Univerzita Palackého v Olomouci, Olomouc, 2002. 4. PEREGRIN, J.: Logika a logiky – Systém klasické výrokové logiky, jeho rozšíření a alternativy, 2004. http://jarda.peregrin.cz/mybibl/PDFTxt/455.pdf Ověřeno: 15. 9. 2017 5. KVASNIČKA, V., POSPÍCHAL, J.: Matematická logika, Slovenská technická univerzita v Bratislave 2006. http://www2.fiit.stuba.sk/~kvasnicka/Free%20books/Matematicka%20Logika_all.pdfověřeno: 15. 9. 2017 6. ŠTĚPÁNEK, Petr: Predikátová logika, Praha, 2000. http://ktiml.mff.cuni.cz/ktiml/teaching/files/materials/StepanekPetr_PredikatovaLogika.pdf ověřeno: 15. 9. 2017 SEZNAM POUŽITÝCH ZNAČEK, SYMBOLŮ A ZKRATEK doc. RNDr. Luděk Cienciala, Ph.D. Úvod do logiky 116 INFORMATIVNÍ, NAVIGAČNÍ, ORIENTAČNÍ KE SPLNĚNÍ, KONTROLNÍ, PRACOVNÍ Čas potřebný k prostudování Kontrolní otázka Průvodce textem, podnět, otázka, úkol Samostatný úkol Nezapomeň na odměnu a odpočinek Test a otázka VÝKLADOVÉ NÁMĚTY K ZAMYŠLENÍ, MYŠLENKOVÉ, PRO DALŠÍ STUDIUM Řešený příklad Úkol k zamyšlení Definice Část pro zájemce Věta Další zdroje