IB112 Základy matematiky Základy matematické logiky Jan Strejček Obsah ■ Výroková logika m výrokové formule, pravdivostní ohodnocení a valuace ■ pravdivost a splnitelnost ■ normální formy ■ úplný systém spojek ■ axiomatický systém ■ Predikátová logika ■ termy, kvantifikátory, predikátové formule ■ interpretace, valuace, pravdivost ■ axiomatický systém IB112 Základy matematiky: Základy matematické logiky 2/76 Výroková logika IB112 Základy matematiky: Základy matematické logiky Výroky a výroková logika Výroky = tvrzení = oznamovací věty, u které můžeme určit její pravdivost ■ složený výrok je poskládán z atomických výroků a spojek ■ Příklady: ■ venku prší (atomický výrok) ■ jestli budeš do osmi v pyžamu, tak bude pohádka (složený výrok) ■ Výroky budeme označovat velkými písmeny A,B,C,... Výroková logika ■ Popisuje, jak lze z výroků a logických spojek budovat další výroky. ■ Zkoumá vztahy mezi pravdivostí různých výroků. IB112 Základy matematiky: Základy matematické logiky 4/76 Logické spojky Logické spojky = výrazy, kterými z výroků vyrábíme složené výroky ■ Příklady: "není pravda, že A\ UA, ledaže by B" ■ V matematické logice používáme jen vybrané spojky, jejichž význam se může mírně lišit od významu v běžném jazyce. Např. "půjdu tam dnes nebo tam půjdu zítra" chápeme tak, že nastane jen jedna eventualita. notace výraz v češtině název "není pravda, že A" negace A A B "A a B" konjunkce A\f B "A nebo B" disjunkce A=> B "jestliže A, tak B" implikace A^B "A právě tehdy, když B" ekvivalence IB112 Základy matematiky: Základy matematické logiky 5/76 Výrokové formule ■ Výrokové formule mohou obsahovat pouze výrokové symboly (reprezentují výroky), logické spojky a závorky (,). Definice (Výrokové formule) Nechť P = {a, b, c,...} je neprázdná množina výrokových symbolů. Výrokové formule nad P definujeme takto: D Každá výrokový symbol je výroková formule. B Jsou-li A, B výrokové formule, pak i (-/A), (AaB),(Av B),(A=> B),(A<& B) jsou výrokové formule. Q Nic jiného není výroková formule. ■ Výrokové symboly nazýváme atomické formule. ■ Ostatní výrokové formule se nazývají složené. IB112 Základy matematiky: Základy matematické logiky 6/76 Poznámky ■ Příklady výrokových formulí: (a =4> (-■£)), (-■((-■a) v £>)), (aA(Ď^>(c^ ... ■ Odvození ((a A b) (c =4> (^a))): ■ a, £>, c jsou formule dle bodu 1. ■ (a a £>) a (-ia) jsou formule dle bodu 2. ■ (c => (^a)) je pak také formule dle bodu 2. ■ Konečně ((a a £>) <=> (c => (->a))) je také formule dle bodu 2. ■ Závorky v zápisu formulí často vynecháváme, pokud tím není dotčena jednoznačnost. Např. píšeme (aAĎ)^(c^> -ia) namísto ((aAb)^(c^ IB112 Základy matematiky: Základy matematické logiky 7/76 Pravdivostní ohodnocení ■ Pravdivost výrokové formule závisí pouze na pravdivosti atomických formulí, které se ve formuli vyskytují. ■ Pravdivost atomických formulí je dána pravdivostním ohodnocením, pravdivost složených formulí je dána valuací Definice (Pravdivostní ohodnocení) Pravdivostní ohodnocení (neboli interpretace) je funkce I: P -> {0,1} přiřazující každé atomické formuli pravdivostní hodnotu 1 (pravda) nebo 0 (nepravda). ■ Pravdivostní hodnoty 1,0 se někdy také značí 7", F. IB112 Základy matematiky: Základy matematické logiky 8/76 Valuace Definice (Valuace) Nechť I je pravdivostní ohodnocení. Valuace V je funkce přiřazující každé výrokové formuli A pravdivostní hodnotu 1 nebo O a splňující: ■ Je-li A atomická formule, pak l\A) = l{A). ■ fi^A) = 1 pokud l\A) = O a l'{-^A) = O pokud I'{A) = 1. ■ I'{A a B) = 1 pokud I'{A) = l\B) = 1. Jinak lr{A a B) = 0. ■ v6) = 0 po/avd = /'(B) = 0. J/na/c /'(d v B) = 1. ■ =4> 6) = O po/avd /'(d) = 1 a /'(B) = 0. Jinak I'{A B) = 1. ■ /'(d ^ B) = 1 po/cud l'(A) = /'(B). J/na/c /'(d ^ B) = 0. ■ Valuace je pravdivostním ohodnocením určena jednoznačně a je jeho rozšířením. ■ Valuaci a pravdivostní ohodnocení tedy lze ztotožnit. IB112 Základy matematiky: Základy matematické logiky 9/76 Pravdivost formule Definice Výroková formule A se nazývá ■ pravdivá při ohodnocení I, jestliže ľ (A) = 1. ■ pravdivá nebo tautologie, psáno |= A, pokud je pravdivá při všech ohodnoceních. ■ kontradikce, pokud není pravdivá při žádném ohodnocení ■ splnitelná, pokud je pravdivá při nějakém ohodnocení Formule A, B jsou ekvivalentní, psáno A = B, pokud jsou pravdivé při stejných ohodnoceních. Příklady ■ tautologie: aw ^a, a^> a, a^ -i-ia, (a A -ia) b ■ kontradikce: aA^a^^a ■ ekvivalentní formule: a =4> b = bv^a IB112 Základy matematiky: Základy matematické logiky 10/76 Příklad Je formule ((a Ai))^>(c l(b) = 0, /(c) = 1? (-■a))) pravdivá při ohodnocení /(a) = 1 IB112 Základy matematiky: Základy matematické logiky 11/76 Příklad Je formule ((a A b) (c ^ (->a))) pravdivá při ohodnocení /(a) = 1 l(b) = 0, l(c) = 1 ? /'(a) = 1, l'(b) = 0, l'(c) = 1 /'(a A Ď) = 0 /'(-a) = 0 /'(c (^a)) = 0 /'((aAb)^(c^(-a))) = 1 Zadaná formule je při daném ohodnocení pravdivá. IB112 Základy matematiky: Základy matematické logiky 12/76 Vybrané tautologie Mnohé tautologie mají svoje názvy: ■ komutativní zákony: (aAí))^(ďa a), (avĎ)^(bva), ■ asociativní zákony: ((a A b) A c) (a A (b A c)),... ■ distributivní zákony: (a A (Ď v c)) ^ ((a A b) v (a A c)),... ■ zákon vyloučení třetího: a v ^a ■ zákon sporu: -n(a A ^a) ■ zákon totožnosti: a ^> a ■ zákon dvojí negace: a ^ -i-ia ■ idempotence: (a A a) ^ a, (a v a) ^ a ■ de Morganovy zákony: -n(a aď)<^ (^a v -hď), -n(av £>) ^> (^aA^Ď) IB112 Základy matematiky: Základy matematické logiky 13/76 Věta o implikaci Věta (Věta o implikaci, sémantický modus ponens) Pokud platí |= A a |= A B, pak platí |= B. Důkaz Sporem. Nechť platí |= A a |= A B a nechť B není tautologie Označme / ohodnocení, v kterém B není pravdivé, t.j. I'{B) = 0 Jelikož A je tautologie, platí I*(A) = 1. Dohromady dostáváme l\A =4> B) = 0 a proto A B není tautologie. To je spor. IB112 Základy matematiky: Základy matematické logiky Pravdivostní tabulka Pravdivostní tabulka zaznamenává pravdivost dané formule (a jejích podformulí) při všech ohodnoceních. Každý řádek tabulky odpovídá jednomu ohodnocení. Počet řádků tabulky je 2n, kde n je počet různých atomických formulí v dané formuli. Pravdivostní tabulka pro (a b) c a b c a=? b (a = > b) =^ c 0 0 0 1 0 0 0 1 1 1 0 1 0 1 0 0 1 1 1 1 1 0 0 0 1 1 0 1 0 1 1 1 0 1 0 1 1 1 1 1 IB112 Základy matematiky: Základy matematické logiky 15/76 Využití pravdivostní tabulky ■ Z pravdivostní tabulky lze dle výsledných pravdivostních hodnot pro danou formuli snadno určit, zdaje formule: ■ tautologie - ve všech řádcích je pravdivostní hodnota 1 ■ kontradikce - ve všech řádcích je pravdivostní hodnota 0 ■ splnitelná - v nějakém řádku je pravdivostní hodnota 1 ■ Srovnáním dvou pravdivostních tabulek snadno rozhodneme i ekvivalenci formulí. ■ Jelikož existuje algoritmus rozhodující zda je výroková formule pravdivá, říkáme, že výroková logika je rozhodnutelná. IB112 Základy matematiky: Základy matematické logiky 16/76 Příklad ■ Sestrojte pravdivostní tabulku pro formuli a {b c). ■ Rozhodněte, zdaje formule tautologie, kontradikce, splnitelná a zda je ekvivalentní formuli (a b) c. a b c b ^ c a (ď =>• c) 0 0 0 0 0 1 0 1 0 0 1 1 1 0 0 1 0 1 1 1 0 1 1 1 IB112 Základy matematiky: Základy matematické logiky 17/76 Příklad ■ Sestrojte pravdivostní tabulku pro formuli a {b c). ■ Rozhodněte, zdaje formule tautologie, kontradikce, splnitelná a zda je ekvivalentní formuli (a b) c. a b c b ^ c a ■ (b ■ c) 0 0 0 1 1 0 0 1 1 1 0 1 0 0 1 0 1 1 1 1 1 0 0 1 1 1 0 1 1 1 1 1 0 0 0 1 1 1 1 1 IB112 Základy matematiky: Základy matematické logiky 18/76 Příklad ■ Sestrojte pravdivostní tabulku pro formuli a (b c). ■ Rozhodněte, zdaje formule tautologie, kontradikce, splnitelná a zda je ekvivalentní formuli (a b) c. a b c b =?■ c a ■ (b c) 0 0 0 1 1 0 0 1 1 1 0 1 0 0 1 0 1 1 1 1 1 0 0 1 1 1 0 1 1 1 1 1 0 0 0 1 1 1 1 1 ■ Není tautologie ani kontradikce, je splnitelná a není ekvivalentní formuli (a b) =^ c. IB112 Základy matematiky: Základy matematické logiky 19/76 Disjunktivní normální forma (DNF) ■ Jelikož je disjunkce asociativní, tedy {A v B) v C = A v (B v C), píšeme pouze Aw Bw C. Podobně lze psát i A a B a C. Definice (Literal, konjunktivní klauzule, DNF) Literál je atomická formule nebo její negace. Konjunktivní klauzule je konjunkce libovolného konečného počtu literálů. Formule A je v disjunktivní normální formě (DNF), je-li to jedna klauzule nebo disjunkce konečně mnoha konjunktivních klauzulí. Příklady ■ literály: a, b, -^a, -ic ■ konjunktivní klauzule: (a A A b), (--a a^c a^b a d) ■ formule v DNF: (aA^cAb)v (-.a A -.c a ^b a d) v (-.cř) IB112 Základy matematiky: Základy matematické logiky 20/76 Disjunktivní normální forma (DNF) ^^^^^^^^^^^^^^^^^ Ke každé výrokové formuli existuje ekvivalentní formule v DNF. Ekvivalentní formule v DNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule pravdivá, přidáme do vytvářené formule v DNF jednu konjunktivní klauzuli, která bude pro každý pravdivý atomický výrok a obsahovat literál a a pro každý nepravdivý atomický výrok b literál ^b. ■ Není-li formule pravdivá v žádném ohodnocení, pak je to kontradikce a je ekvivalentní kontradikci (a A -ia) a ta je v DNF a b (a o -•£>) 1 1 0 1 0 1 0 1 1 0 0 0 IB112 Základy matematiky: Základy matematické logiky 21/76 Disjunktivní normální forma (DNF) ^^^^^^^^^^^^^^^^^ Ke každé výrokové formuli existuje ekvivalentní formule v DNF. Ekvivalentní formule v DNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule pravdivá, přidáme do vytvářené formule v DNF jednu konjunktivní klauzuli, která bude pro každý pravdivý atomický výrok a obsahovat literál a a pro každý nepravdivý atomický výrok b literál ^b. ■ Není-li formule pravdivá v žádném ohodnocení, pak je to kontradikce a je ekvivalentní kontradikci (a A -ia) a ta je v DNF a b (a o -•£>) 1 1 0 1 0 1 0 1 1 0 0 0 ~> (a A ^b) IB112 Základy matematiky: Základy matematické logiky 22/76 Disjunktivní normální forma (DNF) ^^^^^^^^^^^^^^^^^ Ke každé výrokové formuli existuje ekvivalentní formule v DNF. Ekvivalentní formule v DNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule pravdivá, přidáme do vytvářené formule v DNF jednu konjunktivní klauzuli, která bude pro každý pravdivý atomický výrok a obsahovat literál a a pro každý nepravdivý atomický výrok b literál ^b. ■ Není-li formule pravdivá v žádném ohodnocení, pak je to kontradikce a je ekvivalentní kontradikci (a A -ia) a ta je v DNF a b (a o -•£>) 1 1 0 1 0 1 ~* (a A -ló) 0 1 1 ~* (->a A b) 0 0 0 IB112 Základy matematiky: Základy matematické logiky 23/76 Disjunktivní normální forma (DNF) ^^^^^^^^^^^^^^^^^ Ke každé výrokové formuli existuje ekvivalentní formule v DNF. Ekvivalentní formule v DNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule pravdivá, přidáme do vytvářené formule v DNF jednu konjunktivní klauzuli, která bude pro každý pravdivý atomický výrok a obsahovat literál a a pro každý nepravdivý atomický výrok b literál ^b. ■ Není-li formule pravdivá v žádném ohodnocení, pak je to kontradikce a je ekvivalentní kontradikci (a A -ia) a ta je v DNF a b (a o -•£>) 1 1 0 1 0 1 ~* (a A -ló) Celkem: 0 1 1 ~* (->a A b) (a ^ -no) = 0 0 0 (a A -ió) v (-.a A Ď) IB112 Základy matematiky: Základy matematické logiky 24/76 Konjunktivní normální forma (CNF) ■ Definice CNF je analogická definici DNF, akorát konjunkce a disjunkce se prohodí. Definice (klauzule, CNF) (Disjunktivní) klauzule je disjunkce libovolného konečného počtu literálů. Formule A je v konjunktivní normální formě (CNF), je-li to jedna klouzule nebo disjunkce konečně mnoha klauzulí Příklady ■ klauzule: (av^cvb),(--av^cv^vd) ■ formule v CNF: (av^cvb) A (-.av -.c v-.fc v d) A (-.cř) IB112 Základy matematiky: Základy matematické logiky 25/76 Konjunktivní normální forma (CNF) Ke každé výrokové formuli existuje ekvivalentní formule v CNF. Ekvivalentní formule v CNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule nepravdivá, přidáme do vytvářené formule v CNF jednu klauzuli, která bude pro každý nepravdivý atomický výrok a obsahovat literál a a pro každý pravdivý atomický výrok b literál ^b. ■ Je-li formule pravdivá při všech ohodnoceních, je to tautologie a je ekvivalentní tautologii (a v -ia) a ta je v CNF a b (a ^b) 1 1 0 1 0 1 0 1 1 0 0 0 IB112 Základy matematiky: Základy matematické logiky 26/76 Konjunktivní normální forma (CNF) Rěta^^^^^^^^^^^^^^^ Ke každé výrokové formuli existuje ekvivalentní formule v CNF. Ekvivalentní formule v CNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule nepravdivá, přidáme do vytvářené formule v CNF jednu klauzuli, která bude pro každý nepravdivý atomický výrok a obsahovat literál a a pro každý pravdivý atomický výrok b literál ^b. ■ Je-li formule pravdivá při všech ohodnoceních, je to tautologie a je ekvivalentní tautologii (a v -ia) a ta je v CNF a b (a ^b) 1 1 0 1 0 1 0 1 1 0 0 0 IB112 Základy matematiky: Základy matematické logiky 27/76 Konjunktivní normální forma (CNF) Věta Ke každé výrokové formuli existuje ekvivalentní formule v CNF. Ekvivalentní formule v CNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule nepravdivá, přidáme do vytvářené formule v CNF jednu klauzuli, která bude pro každý nepravdivý atomický výrok a obsahovat literál a a pro každý pravdivý atomický výrok b literál ^b. ■ Je-li formule pravdivá při všech ohodnoceních, je to tautologie a je ekvivalentní tautologii (a v -ia) a ta je v CNF a b (a ^b) 1 1 0 1 0 1 0 1 1 0 0 0 ~» (^a v ^b) (a v b) IB112 Základy matematiky: Základy matematické logiky 28/76 Konjunktivní normální forma (CNF) Ke každé výrokové formuli existuje ekvivalentní formule v CNF. Ekvivalentní formule v CNF lze sestrojit z pravdivostní tabulky: ■ Pro každé ohodnocení, kde je formule nepravdivá, přidáme do vytvářené formule v CNF jednu klauzuli, která bude pro každý nepravdivý atomický výrok a obsahovat literál a a pro každý pravdivý atomický výrok b literál ^b. ■ Je-li formule pravdivá při všech ohodnoceních, je to tautologie a je ekvivalentní tautologii (a v -ia) a ta je v CNF a b (a 4$ ^b) 1 1 0 ~h (-.av-iĎ) 1 0 1 Celkem: 0 1 1 (a -no) 0 0 0 ~» (avĎ) ( a . b) a (a v b) IB112 Základy matematiky: Základy matematické logiky 29/76 Pravdivostní funkce ■ Význam výrokových formulí lze také definovat pomocí pravdivostních funkcí Definice (Pravdivostní funkce) Pravdivostní funkce arity n je funkce f: {0,1 }n -> {0,1}. ■ Pravdivostní funkce každé n-tici pravdivostních hodnot přiřadí jednu pravdivostní hodnotu. ■ Každá formule s n (uspořádanými) atomickými formulemi jednoznačně určuje pravdivostní funkci arity n. ■ Např. aAb odpovídá binární pravdivostní funkci f(x, y) = x • y. IB112 Základy matematiky: Základy matematické logiky 30/76 Pravdivostní funkce ■ Pravdivostní funkci lze zapsat tabulkou. X y z 0 0 0 0 0 0 1 0 0 1 0 1 0 1 1 1 1 0 0 0 1 0 1 0 1 1 0 1 1 1 1 0 ■ Lze každou pravdivostní funkci vyjádřit pomocí výrokové formule? IB112 Základy matematiky: Základy matematické logiky 31/76 Pravdivostní funkce ■ Pravdivostní funkci lze zapsat tabulkou. X y z f{x,y,z) 0 0 0 0 0 0 1 0 0 1 0 1 0 1 1 1 1 0 0 0 1 0 1 0 1 1 0 1 1 1 1 0 ■ Lze každou pravdivostní funkci vyjádřit pomocí výrokové formule? ■ Ano. Formuli sestrojíme z tabulky stejně, jako jsme z tabulky vytvořili formuli v DNF (nebo CNF). IB112 Základy matematiky: Základy matematické logiky 32/76 Úplný systém spojek Definice (Úplný systém spojek) Množinu logických spojek nazveme úplný systém spojek, pokud lze každou pravdivostní funkci vyjádřit pomocí výrokové formule používající pouze spojky z dané množiny ■ Jelikož lze každou pravdivostní funkci popsat formulemi v DNF i v CNF, je množina {a, v, -■} úplným systémem spojek. ■ Protože platí A a B = ^(^A v --B) lze každou konjunkci vyjádřit pomocí v, -i. Proto je úplný i systém {v, -■}. ■ Podobně A v B = a -iB) a proto je úplný i systém {a, -i}. ■ {^>, -■} je také úplný systém. ■ Existuje jednoprvkový úplný systém spojek? IB112 Základy matematiky: Základy matematické logiky 33/76 Další logické spojky a b a xor b a nand b a nor b 1 1 0 0 0 1 0 1 1 0 0 1 1 1 0 0 0 0 1 1 ■ XOR - exclusive or, A xor B = -n (/A B) m NAND - Shefferova funkce, A nand B = ^{A A B) m NOR - Nicodova funkce, A nor B = ^{A v B) m {nand} i {nor} tvoří úplné jednoprvkové systémy spojek. ■ Všechny tři spojky jsou v informatice významné. IB112 Základy matematiky: Základy matematické logiky 34/76 Množiny formulí a vyplývání Definice (Splnitelnost, model, vyplývání) Nechť t je množina výrokových formulí. Množina t je splnitelná, pokud existuje ohodnocení, při kterém jsou pravdivé všechny formule z t. Takové ohodnocení se nazývá model množiny t. Formule a logicky vyplývá z množiny t, psáno t |= a, pokud je a pravdivá v každém modelu množiny t. ■ t |= a také čteme jako a je logickým důsledkem t. ■ Z nesplnitelné množiny t vyplývá libovolná formule. ■ Splnitelnost konečné množiny klauzulí t lze rozhodnout pomocí pravdivostní tabulky obsahující sloupce pro všechny formule z t. Platnost t |= a lze rozhodnout analogicky. IB112 Základy matematiky: Základy matematické logiky 35/76 Příklad Zjistěte, zda je množina formulí t = {^b v a, ^a v c} splnitelná a zda je jejím důsledkem formule b^ c. a b c -ifo v a -•ave b =?■ c 0 0 0 0 0 1 0 1 0 0 1 1 1 0 0 1 0 1 1 1 0 1 1 1 IB112 Základy matematiky: Základy matematické logiky 36/76 Příklad Zjistěte, zda je množina formulí t = {^b v a, ^a v c} splnitelná a zda je jejím důsledkem formule b^ c. a b c -ifo v a -•ave b =?■ c 0 0 0 1 1 0 0 1 1 1 0 1 0 0 1 0 1 1 0 1 1 0 0 1 0 1 0 1 1 1 1 1 0 1 0 1 1 1 1 1 m t je splnitelná. IB112 Základy matematiky: Základy matematické logiky 37/76 Příklad Zjistěte, zda je množina formulí t = {^b v a, ^a v c} splnitelná a zda je jejím důsledkem formule b^ c. a b c -ifo v a -•ave b =?■ c 0 0 0 1 1 1 0 0 1 1 1 1 0 1 0 0 1 0 0 1 1 0 1 1 1 0 0 1 0 1 1 0 1 1 1 1 1 1 0 1 0 0 1 1 1 1 1 1 ■ t je splnitelná. ■ b c je důsledkem t. IB112 Základy matematiky: Základy matematické logiky 38/76 Věta o dedukci a lemma o neutrální formuli Věta (Věta o dedukci, sémantická varianta) Buď T množina výrokových formulí. Pak platí T |= A když T u {A} |= B. B právě Věta (Lemma o neutrální formuli, sémantická varianta) Buď T množina výrokových formulí. Pokud platí T u {A} \= B a T u {^A} \= B, pak iT^B. IB112 Základy matematiky: Základy matematické logiky 39/76 Formální systémy ■ Pravdivost formulí lze zkoumat i na základě jejich syntaxe (bez interpretací, bez pravdivostních tabulek). Formální systém ■ umožňuje k formulím budovat důkazy ■ skládá se z ■ axiomů - tvrzení, jejichž pravdivost přijmeme bez důkazu ■ odvozovacích pravidel - konstrukce umožňující vytvářet důkazy ■ může být ■ axiomatický - méně pravidel, více axiomů ■ předpokladový - více pravidel, méně axiomů ■ Ukážeme axiomatický systém pro výrokovou logiku využívajících pouze spojek =4> a -■. IB112 Základy matematiky: Základy matematické logiky 40/76 Axiomatický systém Axiomy (A1) A^(B^A) (A2) (A^(B^ C)) ((A B)^(A^ C)) (A3) (-.B ^A) ^(A^ B) Odvozovací pravidlo (P1) ZAaA^ e plyne B. m A, B, C jsou libovolné výrokové formule. ■ Odvozovací nebo také inferenčnípravidlo (P1) se nazývá pravidlo odloučení nebo modus ponens. ■ V (P1) se formule A a A B nazývají předpoklady, B se pak nazýva zaver, m (P1) se často zapisuje jako A A^B B IB112 Základy matematiky: Základy matematické logiky 41/76 Důkaz Definice (Důkaz) Konečnou posloupnost /A1, A2l..., An výrokových formulí nazveme důkazem formule An, pokud pro každé i < n je A j buď axiomem nebo závěrem odvozovacího pravidla, jehož předpoklady jsou mezi formulemi A|, /42,..., A_1 • Výroková formule A je dokazatelná, psáno h A, pokud existuje důkaz formule A. IB112 Základy matematiky: Základy matematické logiky 42/76 Příklad Dokažte h A => A. IB112 Základy matematiky: Základy matematické logiky 43/76 Příklad Dokažte h a =>■ a. Řešení Důkazem je posloupnost a {(a a) a), (a => ({a => a) => a)) => ((a ^(a^ a)) ^(a^ a)), {a=>(A=> a)) => (a => a), a => (a => a), a^a. Označíme-li formule v posloupnosti a^,a2,... a5, pak ■ a-\ je (A1) pro volbu a, a =>■ a za a, b, ■ a2 je (A2) pro volbu a, a =>■ a, a za a, 6, c, m a3 je závěr (P1) s předpoklady a^a2, ■ a4 je (A1) pro volbu a, a za a, b, ■ a5 je závěr (P1) s předpoklady a3,a4. IB112 Základy matematiky: Základy matematické logiky 44/76 Zobecnění dokazatelnosti Definice Nechť T je množina výrokových formulí. Konečnou posloupnost A^A2,..., A? výrokových formulí nazveme důkazem formule An z T, pokud pro každé i < n je A\ buď axiomem, prvkem T nebo závěrem odvozovacího pravidla, jehož předpoklady jsou mezi formulemi A|, A2,..., A_1 - Píšeme T h An m\-A\e totéž jako 0 h A ■ Místo {A} h B píšeme pouze A h B. IB112 Základy matematiky: Základy matematické logiky 45/76 Věta o dedukci a lemma o neutrální formuli Věta (Věta o dedukci) Buď T množina výrokových formulí. Pak platí T h A B právě když T U {A} h B. Důkaz □ Směr "=4>". Platí-li T h A B, pak existuje důkaz Ai,A2,...,AmA=> B formule A B z T. Pak ale Ai,A2,...,An,A=> B, A, B je důkaz formule B z Tu {A}. B Důkaz je komplikovanější... □ IB112 Základy matematiky: Základy matematické logiky 46/76 Příklad Platí flhn/l4(^ b), Q h -.-.4 => a, |h(44B)4(ne4 ^a), ihH^yi)^ a. Důkaz Ukážeme (1), ostatní se lze dokázat podobně. ■ Z (A1) plyne I—i/4 (^b => ^a). m z Věty o dedukci dostáváme ->a I—a h a S. ■ Z Věty o dedukci dostaneme I— b). □ IB112 Základy matematiky: Základy matematické logiky 47/76 Vlastnosti axiomatického systému Věta (Lemma o neutrální formuli) Buď T množina výrokových formulí. Pokud platí T u {A} h B a ľuH} h B, pak i T \- B. Důkaz Postupně dokážeme D T I—>A^ Bz Věty o dedukci, B íh^S^ -i-.^ aplikací (P1) na (3) v předchozím příkladu a (1 H 7 u {^B} h -i-Tl z Věty o dedukci, □ 7 u {-B} h /A aplikací (P1) na (2) v předchozím příkladu a (3) B ľh/1^6z předpokladů a Věty o dedukci, □ T u {^6} h 6 z (P1) a předcházejících dvou tvrzení, H 7" I—B =4> B z Věty o dedukci, □ T h B aplikací (P1) na (5) v předchozím příkladu a (7). IB112 Základy matematiky: Základy matematické logiky 4í Korektnost a úplnost Věta (Korektnost a úplnost) Nechť T je množina výrokových formulí a A je výroková formule. Pak platí T h A právě tehdy, když T |= A. ■ Implikace "=4>" se nazývá korektnost (co dokážeme to platí). ■ K důkazu korektnosti stačí ukázat, že (A1), (A2) i (A3) jsou pravdivé a že (P1) z pravdivých předpokladů odvodí vždy pravdivý závěr. ■ Implikace se nazývá úplnost (dokážeme vše, co platí). ■ Existují i další formální systémy pro výrokovou logiku (např. Gentzenovskýsystém). IB112 Základy matematiky: Základy matematické logiky 49/76 Predikátová logika IB112 Základy matematiky: Základy matematické logiky Predikátová logika ■ Rozšiřuje výrokovou logiku. ■ Umožňuje přesněji popsat výrok a díky tomu odvodit logická vyplývání, která ve výrokové logice odvodit nelze: ■ Každý člověk je smrtelný. ■ Sokrates je člověk. ■ Sokrates je smrtelný. ■ Výroky označíme postupně a, b, c. Ve výrokové logice nelze odvodit logické vyplývání cza,b, přestože c zjevně je důsledkem a, b. IB112 Základy matematiky: Základy matematické logiky 51/76 Jazyk predikátové logiky Jazyk predikátové logiky se zkládá z těchto symbolů: ■ proměnné: x, y, z, x-i, x2,... ■ logické spojky: -i, A, v, ■ kvantifikátory: V (pro všechna), 3 (existuje) ■ rovnosť. = ■ závorky: (,) ■ relační neboli predikátové symboly: P, Q, P, P1, P2,... ■ funkční symboly: f, g, h, ^, ŕ2,... ■ Každý predikátový symbol má pevně danou arity n > 0. ■ Každý funkční symbol má pevně danou aritu n > 0 (počet argumentů). ■ Funkce s aritou 0 se nazývají konstanty a značí se a, b, c,.... IB112 Základy matematiky: Základy matematické logiky 52/76 Konstanty, proměnné a funkce ■ Konstanty, proměnné i funkce slouží k označení objektů. ■ Objekty jsou prvky dané množiny objektů nazývané doména nebo univerzum. ■ Konstanty jsou vlastně jména objektů. ■ Proměnné zastupují libovolné objekty. ■ Pomocí funkcí vytváříme složená jména objektů. Příklad ■ Uvažujme doménu nezáporných celých čísel. ■ Konstanty jsou např. 0,1,42. ■ Příkladem binární funkce (funkce arity 2) je +. ■ Složené jméno objektu 3 je například 1 + 2 nebo (1 + 1) + 1. ■ Složené jméno objektu je i x + 2 nebo (x + 2) + (z + x). IB112 Základy matematiky: Základy matematické logiky 53/76 Termy ■ Termy jsou všechna možná označení objektů. Definice (Termy) Termy definujeme takto: D Každá proměnná je term. B Je-li f funkční symbol arity n a ri, , • • •, &? jsou termy pak i f(U,t2,...,tn)jeterm. B Nic jiného není term. ■ Z bodu (2) plyne, že konstanty (nulární funkce) jsou také termy. ■ Příklady termů: a, 0, x, f(x, 0, a), f(g(a, 0), 2, Ai(Ai(y))) IB112 Základy matematiky: Základy matematické logiky 54/76 Predikát ■ Nulární predikát je výrok (jako ve výrokové logice). ■ Unární predikát ■ popisuje vlastnost objektu, ■ odpovídá výroku, ze kterého odstraníme označení jednoho objektu. ■ Příklad: Predikát P odpovídá pojmu "být smrtelný" "Objekt x je smrtelný" P(x) "Sokrates je smrtelný" Q(x + 3,2) "x je menší než 7" x < 7 (infixová notace) ■ Predikát arity n popisuje vztah mezi n objekty. IB112 Základy matematiky: Základy matematické logiky 55/76 Kvantifikátory V - univerzální neboli obecný kvantifikátor ■ (Vx)P(x) říká, že pro všechny objekty x z domény platí P(x). ■ Pro konečnou doménu {a^, a2,..., an} je (Vx)P(x) ekvivalentní formuli P(a^) A P(a2) A ... A P(an). B - existenciální kvantifikátor ■ (3x)P(x) říká, že existuje (alespoň jeden) objekt x z domény, pro který platí P(x) (neboli P(x) platí pro některé objekty x). ■ Pro konečnou doménu ^, a2,..., an} je (3x)P(x) ekvivalentní formuli Pfa) v P(a2) v ... v P(an). Příklad ■ Nechť P odpovídá pojmu "být smrtelný". ■ Uvažujme doménu všech lidí. ■ (Vx)P(x) říká, že všichni lidé jsou smrtelní. ■ (3x)P(x) říká, že existuje smrtelný člověk (neboli někteří lidé jsou smrtelní). IB112 Základy matematiky: Základy matematické logiky 56/76 Predikátové formule Definice (Predikátové formule) Atomické predikátové formule definujeme takto: D Nechť P je predikátový symbol arity n a U,..., řn jsou termy Pak P(ři,..., tn) je atomická predikátová formule. B Jsou-li ři, t2 termy pak ři = t2 je atomická predikátová formule. B Nic jiného není atomická predikátová formule. Predikátové formule definujeme takto: D Každá atomická predikátová formule je predikátová formule. B Jsou-li (p, íp predikátové formule, pak i (pVíp,(pAíp,(p^íp,(p^íp jsou predikátové formule. B Je-li x proměnná a

P(x, z) ... vázaný/volný výskyt ■ Proměnná se nazývá volná (resp. vázaná), existuje-li v dané formuli její volný (resp. vázaný) výskyt. ■ Formule bez volných proměnných se nazývá sentence neboli uzavřená formule. ■ Formule bez kvantifikátorů se nazývá otevřená formule. ■ Zápis v?(x-|, x2,..., xn) označuje formuli p a zdůrazňuje, že všechny volné proměnné formule p jsou mezi x-|, x2,..., xn. IB112 Základy matematiky: Základy matematické logiky 59/76 Sémantika predikátové logiky K definici sémantiky potřebujeme určit množinu objektů (doménu) a dále dát význam funkčním a predikátovým symbolům. Proměnným je třeba přiřadit objekty. Definice (Realizace/interpretace) Realizace neboli interpretace I jazyka predikátové logiky je struktura obsahující ■ neprázdnou množinu D zvanou doména nebo univerzum, ■ funkci l(f) : Dn -> D pro každý n-ární funkční symbol f, ■ relaci /(P) c Dn pro každý n-ární relační symbol P. Definice (Ohodnocení/valuace proměnných) Ohodnocení neboli valuace proměnných je zobrazení V přiřazující každé proměnné prvek domény D. IB112 Základy matematiky: Základy matematické logiky 60/76 Příklad ■ Uvažme jazyk predikátové logiky obsahující: ■ konstantu 0 ■ unární funkci s ■ binární funkce +, * ■ binární relaci < ■ Standardní interpretace / tohoto jazyka: ■ doména N0 ■ /(O) je číslo 0 ■ l(s)(n) = n + 1 pro každé í)eN0 ■ /(+), /(*) jsou operace sčítání a násobení na N0 ■ /(<) je relace "menší než" na N0 ■ Nestandardní, ale taky možná interpretace /': ■ doména D = {a, b} ■ /'(O) je prvek a ■ //(s)(a) = b, ľ(s){b) = a ■ /7(+)(x,y) = a, /7(*)(x,y) = y pro všechna x,y e {a, £>} ■ //(<) = {(a,fe),(a,a)} IB112 Základy matematiky: Základy matematické logiky 61/76 Sémantika predikátové logiky Definice (Hodnota termu) Hodnotou termu t při interpretaci I a valuaci V rozumíme prvek |ř|/^ domény D definovaný dle tvaru termu takto: ■ Je-li t proměnná x, pak\t\iy = V(x). ■ Je-li t tvaru f(U, ř2, • • •, tn), pak t\i,v = 1(0 (\h \i,v, • • •, ■ Hodnota proměnné je tedy přímo dána valuaci této proměnné. ■ Hodnotu termu f(U, ř2, • • •, tn) získáme tak, že vezmeme hodnoty termů ři, ř2,..., řn a na tyto hodnoty aplikujeme funkci l(f) přiřazenou symbolu f interpretací /. ■ Hodnota termu závisí pouze na valuaci proměnných, které se v termu vyskytují. IB112 Základy matematiky: Základy matematické logiky 62/76 Určete hodnotu termu s(s(0)) * s(x + s(0)) při dříve definované interpretaci / a valuaci V(x) = 7. IB112 Základy matematiky: Základy matematické logiky Příklad Určete hodnotu termu s(s(0)) * s(x + s(0)) při dříve definované interpretaci / a valuaci V(x) = 7. m |0|/,„ = /(0) = 0 ■ |s(0)|,,„ = l(s)(\0\,,v) = /(s)(0) = 0 + 1=1 ■ \s(s(0))\,,v = /(s)(|s(0)|,,„) = /(s)(1) = 1+1=2 ■ \s(x + s(0))\i>v = /(s)( + 1) = /(s)(7 + 1) = 8 + 1 = 9 ■ |s(s(0))*s(x+s(0))|/y = |s(s(0))|/,Hs(x+s(0))|/)V = 2-9 = 18 IB112 Základy matematiky: Základy matematické logiky 64/76 Příklad Určete hodnotu termu s(s(0)) * s(x + s(0)) při dříve definované interpretaci / a valuaci V(x) = 7. m |0|/)U = /(0) = 0 ■ |s(0)|/,„ = l(s)(\0\,tV) = /(s)(0) = 0 + 1=1 ■ \s(s(0))\,,v = l(s)(\s(0)\,,v) = /(s)(1) = 1+1=2 ■ \s(x + s(0))\,iV = l(s){ V{x) + 1) = /(s)(7 + 1) = 8 + 1 = 9 ■ |s(s(0))*s(x+s(0))|/y = |s(s(0))|/,Hs(x+s(0))ky = 2-9 = 18 Totéž při interpretaci /' a valuaci V'(x) = b. IB112 Základy matematiky: Základy matematické logiky 65/76 Příklad Určete hodnotu termu s(s(0)) * s(x + s(0)) při dříve definované interpretaci / a valuaci V(x) = 7. ■ |0|/,y=/(0)=0 ■ \s{0)\i)V = l(s)(\0\i,v) = /(s)(0) = 0 + 1=1 ■ 15(5(0))!,, v = l(s)(\s(0)\,,v) = /(s)(1) = 1+1=2 ■ |s(x + s(0))|,,y = /(s)(l/(x) + 1) = /(s)(7 + 1) = 8 + 1 =9 ■ |s(s(0))*s(x+s(0))|/)V = |s(s(0))|/^-|s(x+s(0))|/)V = 2-9 = 18 Totéž při interpretaci /' a valuaci V'(x) = b. m \s(x + s(0))\,,,v, = l'(s)(a) = b ■ |s(s(0)) * s(x + s(0))|//,y/ = b IB112 Základy matematiky: Základy matematické logiky 66/76 Sémantika predikátové logiky l/[x/d] značí valuaci lišící se od V pouze tím, že proměnné x přiřazuje prvek d. Definice (Pravdivost predikátové formule) Formule

, ■ ^1 v a /, 1/ |= ^1 nebo /, 1/ |= ^2, ■ ^1 a íp2 a /, 1/ |= ^1 a /, 1/ |= íp2, ■ ^1 nebo /, V |= ■ ^ ^ ^2 a /, V |= ^1 a /, 1/ |= ^2, ^^jbo /, V ^ ^1 ^ /, 1/ ^ ^2, ■ (Vx)^ a /, \/[x/c/] |= í/j pro každé d z domény D, ■ (3x)í/j a /, \/[x/c/] |= í/j pro nějaké d z domény D. IB112 Základy matematiky: Základy matematické logiky Pravdivost formule ■ Snadno se ověří, že pravdivost formule

(Vx)(p(x) ^ (3x)-xp(x), ->(3x)(p(x) ^ (Vx)-np(x) ■ zaměnitelnost kvantifikátorů stejného typu: (Vx)(VyM*,y) (Vy)(Vx)^(x,y), (3x)(3y)(p{x, y) & (3y)(3x)(p{x,y) ■ distributivita kvantifikátorů: (\/x)((fi(x) a lp(x)) & (Vx)^(x) a (VX)^(X), (3x)( ■ ... princip indukce IB112 Základy matematiky: Základy matematické logiky 73/76 Axiomatický systém predikátové logiky Axiomy (A1)

p)) (A3) (-.^ -.y?) VO (A4) axiom kvantifikátoru (Vx)(p =4> -0) =4> =>► (Vx)VO, pokud x není volná ve