Ernest 2004
1. Predikátová logika jako prost edek
reprezentace znalostí
1.1 Historie výrokové logiky Problém explicitních znalostí a údaj , kterých je obrovské množství, vedl ke vzniku výrokové logiky. lov k si obecn nepamatuje všechny informace, jen ty nejd ležit jší. Mnohdy kombinuje své znalosti tak, že z nich odvodí nová tvrzení. Pojem d kazu, který používali již anti tí filozofové a myslitelé, ovlivnil výrazn rozvoj matematického a v deckého myšlení, jak jej známe dnes. Na jeho základech je budována matematika jako induktivní v da, která vychází z n kolika axiom a logických pravidel, pomocí kterých pak vytvá í d kazy dalších tvrzení. Metodami argumentace, studiem a formalizací tohoto zpracování informací se zabývá logika. Mezi prvotní zakladatele této matematické disciplíny se adí e tí filozofové Platon a Sokrates a matematik Euklides. Možnosti a meze logiky se blíže poda ilo ur it až ve 20. století díky významným pracím v dc jako D. Hilberta, K. Gödela, B. Russela a A. Tarského. Již dva tisíce let nazp t je znám výrok krétského myslitele Epistemida: „Co íká Kré an, je lež“. Jedná se o tzv. Russel v paradox v teorii množin, logice a reprezentaci p irozeného jazyka do jazyka matematické logiky. Nap íklad Kurt Gödel ve 30. letech devatenáctého století ukázal, že problém formalizace jisté oblasti myšlení není pouhou otázkou vhodné restrikce jazyka a volby axiom . Gödelova v ta upozor uje na to, že nem že existovat žádná kone n axiomatizovaná teorie obsahující prost edky pro popis elementární matematiky, v níž by byla odvoditelná všechna pravdivá tvrzení o p irozených íslech. Další Gödelova v ta, v ta o nedokazatelné a nevyvratitelné formuli, odhaluje marnost hledání úplného axiomatického systému. Dokazuje totiž, že v každé axiomatizovatelné teorii obsahující aritmetiku lze formulovat takové tvrzení, že v dané teorii není dokazatelné ono samo, ani jeho pop ení (tzv. nerozhodnutelná tvrzení).
Ernest 2004
V dalších kapitolách budou osv tleny základní pojmy a metody matematické logiky, zejména predikátová logika 1. ádu, nebo ta má v matematice výsadní postavení.
1.2 Jazyk predikátové logiky Základní prvky jazyka predikátové logiky 1. konstanty, prom nné (konkrétní nebo abstraktní objekty) 2. funkce (složené objekty) 3. predikáty (relace mezi objekty) Objekty jazyka – termy • jednoduché termy konstanty prom nné • složené termy – aplikace funkcí na termy Vztahy mezi objekty – formule • atomická formule – predikát aplikovaný na termy • složená formule – libovolné složené formule predikátové logiky 1. ádu vznikají z atomických formulí pomocí logických spojek a kvantifikátor Za základní spojky se obvykle berou: & (konjunkce) ∨ (disjunkce) (implikace) ¬ (negace) Za základní kvantifikátory se obvykle berou ∀ (pro všechna) ∃ (existuje)
Ernest 2004
Nech a, b jsou formule, potom následující konstrukce jsou také formule: ¬ a, a & b, a ∨ b, a b, ∀Xa, ∃Xb (X je lib. prom nná) Ekvivalentní úpravy formulí: a b a b ¬ (a ∨ b) ¬ (a & b) ¬¬ a (a1 & a2) b a (b1 & b2)
¬a∨b ¬b ¬a ¬a &¬b ¬a ∨¬b A a1 (a2 b) (a b1) & (a
b2)
P eklad z p irozeného jazyka: „Všechny ervené houby jsou jedovaté“ ∀X( ervený(X) & houba(X) jedovatá(X)) ∀X( ervený(X) (houba(X) jedovatá(X))) ím se matematická logika zabývá? • Co lze vyjád it? (jazyk) • Co lze odvodit? (axiomy, odvozovací pravidla) • Co je pravdivé? (platí ve všech modelech – sémantický pojem) Výroková logika: výrok, pravdivost, tautologie spojky – charakterizace tabulkou Predikátová logika 1. ádu: • Mluví o objektech, jejich relacích – predikáty • Vztah k typ m, zobecn ní ∀X(P(X)) • Význam formule je p esn definován
Ernest 2004
Úlohy 1. Uve te vhodný p íklad konstanty, prom nné, funkce a predikátu. 2. Uve te vhodný p íklad atomické a složené formule. 3. Dokažte užitím pravdivostní tabulky ekvivalenci mezi formulemi a) ¬ (a & b) ⇔ ¬ a ∨ ¬ b, b) (a1 & a2) b ⇔ a1 (a2 b), c) ¬ (a ∨ b) ⇔ ¬ a & ¬ b. 4. Prove te p eklad tvrzení: „Houba je jedovatá, jen když je ervená“, do jazyku predikátové logiky.
1.3 Formální systém a d kazové prost edky Axiomy: • Axiomy výrokové logiky (A1) a (b a) (A2) (a (b c)) ((a b) ¬ a) (a b) (A3) (¬ b
(a
c))
Odvozovací pravidla: • Modus ponens (MP) Dovoluje ze dvou formulí a a a
b odvodit formuli b.
• Pravidlo generalizace (GEN) Pro libovolnou prom nnou X odvo z formule a formuli ∀Xa.
Ernest 2004
D kaz formule ve formálním systému:
a1 , a2 ,....an
b zápis zna í: formule a1 , a2 ,....an dokazují formuli b
V ta o dedukci:
ψ práv tehdy, když platí Je-li ϕ uzav ená formule, pak T, ϕ T ϕ ψ. (d kaz indukcí podle délky d kazu formule ψ) V ta o sporu: Abychom dokázali n jakou formuli ψ, nutný p edpoklad pro ψ nech je ϕ. P edpokládáme, že ϕ neplatí, a ukážeme, že tento p edpoklad vede ke sporu tj. ¬ϕ → (ϕ → ψ ) . (d kaz užitím axiom A1 a A3) Lemna pro formální systém: Nech a, a1, a2, a3, b, b1, b2 a c jsou libovolné formule, pak platí tato tvrzení (L1)
(L2) (L3) (L4) (L5)
a&b a&b a, b ¬ (a & b) ¬ (a & b) a → b, b → c a & b → c, b a1 & a2 & a3 → b, a2, a3 a → (b1 ∨ b2), b2 → c a1 → b1, a2 → b2 a → b ∨ c , a → ¬c a ∨ b, a → c
a b a&b a → (a ∨ b) a→¬b ¬a∨¬b a→c a→c a1 → b a → (b1 ∨ c) (a1 ∨ a2) → (b1 ∨ b2) a→b b∨c
Ernest 2004
Úlohy 1. Dokažte užitím pravdivostní tabulky axiom a) A1, b) A2, c) A3. 2. Dokažte v tu o sporu. 3. Dokažte užitím axiom a d kazových prost edk systému tvrzení a) L2, b) L3.
formálního
Použitá literatura [1] [2] [3] [4]
Ma ík, Št pánková, Lažanský a kol., Um lá inteligence 1, Academia, 1993. Kotek, Vysoký, Zdráhal, Kybernetika, SNTL, 1990. Demlová, Pond lí ek, Matematická logika, skriptum VUT, 1997. Stránky p edm tu – p ednášky http://gerstner.felk.cvut.cz.
