Podcast na Formální a predikátová logika

Kapitoly

Úvod do formální logiky

Formulace a překlad

Kvantifikátory a spojky

Když symboly chybí

Teoretické otázky: Gödelovy věty

Definice: Interpretace a Term

Důkaz, korektnost a úplnost

Kouzlo distributivity

Velký úklid ve vzorcích

Hledání nejobecnějšího unifikátoru

Rezoluce: Hledání rozporu

PNF: Uklízíme kvantifikátory

Skolemizace: Konec existenci

Aktivní vs. pasivní zápis

Frustrace stranou

Kdo je kdo?

Závěr a rozloučení

Přepis

Anna: Takže kvantifikátory jsou v podstatě jenom super fancy způsob, jak říct „všichni“ nebo „někdo“? To je geniální!

Lukáš: Přesně tak! Formální logika zní děsivě, ale ve skutečnosti je to jen nástroj, jak být super přesný. A na zkouškách je přesnost klíčová.

Anna: Dobře, to musíme rozebrat. Posloucháte Studyfi Podcast. Dnes se s naším expertem Lukášem ponoříme do světa formální logiky.

Lukáš: Ahoj Anno, ahoj všichni. Nebojte se, nebude to tak hrozné, jak to zní. Vlastně je to docela zábava, když víte, jak na to.

Anna: Fajn, tak pojďme rovnou na příklad. Máme větu: „Mezi libovolnými dvěma různými sudými čísly leží liché číslo.“ Jak tohle, proboha, převedu do těch vašich symbolů?

Lukáš: Skvělá otázka! Rozbijeme si to na kousky. „Libovolnými dvěma“ nám říká, že budeme mluvit o všech možných dvojicích. Takže potřebujeme dva univerzální kvantifikátory. Značí se ∀. Takže začneme s ∀x ∀y.

Anna: Okej, jakože „pro všechna x“ a „pro všechna y“. Chápu. Co dál?

Lukáš: Teď musíme říct, že ta x a y jsou sudá. Takže přidáme podmínku: (even(x) ∧ even(y)). Ten stříškový symbol ∧ znamená „a zároveň“.

Anna: Takže: pro všechna x a pro všechna y platí, že x je sudé a zároveň y je sudé. Zatím to dává smysl. Ale ta věta mluví o *různých* číslech.

Lukáš: Přesně! Musíme to upřesnit. Přidáme další podmínku: x < y. Celé to teď vypadá takhle: ∀x ∀y((even(x) ∧ even(y) ∧ x < y) ... a teď přijde ta druhá část věty.

Anna: Ta část, kde se říká, že „mezi nimi leží liché číslo“.

Lukáš: Ano. „Leží“ nebo „existuje“ nám naznačuje, že použijeme existenční kvantifikátor, ∃. Takže naše formule bude pokračovat šipkou, která značí implikaci, a pak ∃z.

Anna: Takže jestli platí ta první část o dvou různých sudých číslech, PAK existuje nějaké 'z'?

Lukáš: Perfektně řečeno. A teď už jen dodefinujeme, co to 'z' je. Musí být liché, takže (odd(z)).

Anna: A musí ležet *mezi* x a y.

Lukáš: Správně. Takže x < z a zároveň z < y. Když to všechno spojíme, dostaneme finální formuli.

Anna: Takže: ∀x ∀y((even(x) ∧ even(y) ∧ x < y) → ∃z(odd(z) ∧ x < z ∧ z < y)). Páni. Když to člověk vidí takhle rozebrané, tak to najednou není taková magie.

Lukáš: Vůbec ne. Je to jako skládačka. Každé slovo má svůj symbol a své místo.

Anna: Zmínil jsi takový malý tip, který by se mohl hodit. Něco o tom, jak se kvantifikátory kamarádí se spojkami.

Lukáš: Jo, to je dobrá pomůcka. Univerzální kvantifikátor ∀, tedy „pro všechny“, se nejčastěji pojí s implikací, tedy tou šipkou →. Říkáme tím: „PRO VŠECHNY prvky platí, že POKUD splňují podmínku A, PAK splňují i podmínku B.“

Anna: Jasně, jako v našem příkladě. POKUD jsou x a y dvě různá sudá čísla, PAK mezi nimi leží liché.

Lukáš: Přesně. A naopak, existenční kvantifikátor ∃, tedy „existuje“, se většinou pojí s konjunkcí ∧, tedy „a zároveň“.

Anna: Protože říkáme: „EXISTUJE prvek, který má vlastnost A A ZÁROVEŇ vlastnost B.“

Lukáš: Trefa. Jako v našem příkladu to z: EXISTUJE z, které je liché A ZÁROVEŇ je větší než x A ZÁROVEŇ menší než y. Tohle je fakt užitečná berlička.

Anna: Co když ale v zadání nemám všechny potřebné symboly? Třeba tady máme even a odd, ale co kdybychom měli definované jen sudé?

Lukáš: Výborný postřeh. To se stává často. Musíme si umět poradit s tím, co máme. Kdybychom měli jen predikát even(x), tak liché číslo bychom prostě zapsali jako jeho negaci: ¬even(x).

Anna: Aha! Takže „není sudé“. To je chytré. To je jako v programování, když něco definuješ přes negaci.

Lukáš: Přesně tak. Nebo si představ, že máš v zadání jen množinu adresářů, dir(x). Ale úkol po tobě chce pracovat se soubory. Jak bys zapsala, že 'x' je soubor?

Anna: No... jednoduše bych řekla, že to není adresář? Takže ¬dir(x)?

Lukáš: Bingo! Logika je o tomhle. Pracovat s tím, co je definované, a zbytek si chytře odvodit. Ne vždy je všechno naservírované na stříbrném podnose.

Anna: Dobře, praxi bychom měli. Ale na zkouškách jsou i teoretické otázky. A některé znějí… no, dost děsivě. Třeba: Formulujte první Gödelovu větu o neúplnosti.

Lukáš: Ach, Gödel. Velký strašák. Ale my se ho bát nebudeme. Zkusme to jednoduše. První věta v podstatě říká, že jakýkoliv dostatečně silný a bezesporný matematický systém – jako je třeba aritmetika, kterou známe ze školy – bude vždy obsahovat tvrzení, která jsou pravdivá, ale v rámci toho systému je nelze dokázat.

Anna: Počkej, počkej. Takže existují matematické pravdy, které prostě nemůžeme dokázat pomocí matematiky, kterou používáme?

Lukáš: Přesně! Je to naprosto ohromující myšlenka. Vždycky budou existovat hranice toho, co můžeme dokázat. Systém nikdy nemůže být zároveň dostatečně silný, bezesporný a úplný.

Anna: To je… trochu znepokojující. A co ta druhá věta?

Lukáš: Ta na to navazuje. Druhá Gödelova věta říká, že žádný takový systém nemůže dokázat svou vlastní bezespornost. Jinými slovy, matematika nemůže dokázat, že v ní samotné nejsou žádné rozpory.

Anna: Takže musíme prostě věřit, že 2+2=4 a že se nám celý systém někde nezhroutí?

Lukáš: V podstatě ano. Musíme předpokládat, že je bezesporný, protože to zevnitř dokázat nejde. Je to filozofický přesah matematiky, který fascinuje lidi už skoro sto let.

Anna: Dobře, Gödel je filozofie. Ale co ty sušší definice? Třeba: „Definujte pojem interpretace jazyka predikátové logiky 1. řádu.“

Lukáš: Zní to složitě, ale představ si to jako slovník. Interpretace je dvojice (D, α). 'D' je doména – to je svět, o kterém mluvíme. Třeba množina všech lidí nebo všech čísel.

Anna: A to 'α'?

Lukáš: 'α' je to zobrazení, ten překladač. Říká nám, co jednotlivé symboly v našem světě 'D' znamenají. Každé proměnné přiřadí konkrétní prvek z domény, každému predikátovému symbolu přiřadí nějaký vztah a každému funkčnímu symbolu nějakou funkci.

Anna: Takže interpretace je v podstatě klíč k tomu, jak číst naši formuli ve skutečném světě? Bez ní jsou to jen prázdné symboly.

Lukáš: Přesně. A s tím souvisí i další pojem: term. Co je to term?

Anna: To zní jako něco z Terminátora.

Lukáš: Blízko. Term je v podstatě cokoliv, co může označovat nějaký objekt v naší doméně. Nejjednodušší term je proměnná. A pak, pokud máme nějaký funkční symbol 't' a nějaké termy 't1' až 'tn', tak i 't(t1, ..., tn)' je zase term.

Anna: Takže třeba 'x' je term. A když máme funkci 'otec(x)', tak 'otec(x)' je taky term? Protože označuje konkrétní osobu – otce osoby x.

Lukáš: Přesně tak! Termy jsou jména pro objekty. Formule jsou pak celá tvrzení o těchto objektech.

Anna: Pojďme na další. Důkaz formule ve výrokové logice, takzvaný Hilbertovský důkaz.

Lukáš: To je jednoduché. Je to posloupnost formulí, která končí tou formulí, kterou chceme dokázat. A teď to důležité: každá formule v té posloupnosti musí být buď axiom – tedy nějaká základní, daná pravda – nebo musí být odvozena z předchozích formulí pomocí nějakého odvozovacího pravidla, typicky Modus Ponens.

Anna: Takže je to jako stavět zeď. Každá cihla (formule) musí buď stát na pevném základu (axiom), nebo musí být podepřená jinými, už položenými cihlami (odvození).

Lukáš: Perfektní analogie! A s tím souvisí dva klíčové pojmy: korektnost a úplnost systému.

Anna: To zní důležitě.

Lukáš: Jsou to nejdůležitější vlastnosti. Systém je *korektní*, pokud všechno, co v něm dokážeme, je skutečně pravda. Jinými slovy, náš systém neprodukuje žádné lži. Dokazatelné implikuje platné.

Anna: A úplnost?

Lukáš: *Úplnost* je druhá strana mince. Systém je úplný, pokud každá pravda, která v něm platí, je v něm zároveň i dokazatelná. Tedy, že nám žádná pravda neuteče, že na všechno můžeme přijít.

Anna: Aha! Takže korektnost znamená „nedokazujeme nesmysly“ a úplnost znamená „dokážeme všechny pravdy“.

Lukáš: Přesně. Ideální logický systém je korektní a úplný. Ale jak nám ukázal Gödel, u složitějších systémů, jako je aritmetika, té úplnosti nikdy nedosáhneme.

Anna: Páni. Formální logika je nakonec mnohem hlubší, než se zdá. Není to jen o symbolech, je to o hranicích našeho poznání.

Lukáš: Přesně tak. A pochopit tyhle základy vám dá obrovskou výhodu, nejen u zkoušky, ale i v kritickém myšlení obecně. A o tom si povíme víc hned po krátké pauze.

Anna: Takže když už máme formuli v nějakém základním tvaru, to ještě není konec, že? Narazila jsem třeba na zákon distributivity, který vypadal... no, docela divoce.

Lukáš: Jo, ten umí potrápit, ale princip je vlastně jednoduchý. Je to podobné, jako když na základce roznásobuješ závorky v matematice.

Anna: Roznásobuješ? To zní povědomě.

Lukáš: Přesně tak. Představ si, že máš výraz A nebo (B a C). Zákon distributivity ti dovolí to „nebo“ distribuovat do závorky. Takže dostaneš (A nebo B) a (A nebo C).

Anna: Aha! Takže to platí i pro ten složitější příklad, co jsem viděla? Bylo to něco jako ne-X nebo (Y a (ne-Z nebo ne-W)).

Lukáš: Přesně! Vezmeš to ne-X a v podstatě ho „přidáš“ ke každému členu v té velké závorce. Výsledek je (ne-X nebo Y) a zároveň (ne-X nebo ne-Z nebo ne-W). Tímhle krokem se dostáváme k takzvané konjunktivní normální formě, neboli CNF.

Anna: Super, to je mnohem jasnější. Ale co když mi po takové úpravě vznikne v závorce nějaký chaos?

Lukáš: Dobrá otázka. Po každém kroku je klíčové výraz zjednodušit. To je skoro nejdůležitější část.

Anna: Takže takový logický úklid?

Lukáš: Přesně tak. Když máš třeba v závorce (Y a Y a Z), je to zbytečně dlouhé. Můžeš to zkrátit jen na (Y a Z).

Anna: To dává smysl. A co nějaký složitější případ?

Lukáš: Tak co třeba (Y a ne-Z a ne-Y)? Tady se děje něco zajímavého. Máš tam Y a zároveň jeho negaci ne-Y.

Anna: Ty dvě věci přece nemůžou platit najednou.

Lukáš: Bingo! Je to spor. Celá ta závorka je tedy nepravdivá, logická nula. A když máš něco spojené s nulou, často to zjednoduší celý výraz. Takže z chaosu je najednou... nic.

Anna: Zmizí to jako pára nad hrncem. Skvělé. Teď ale odbočím k něčemu, co zní jako tajný kód... MGU. Co to proboha je?

Lukáš: MGU, neboli Most General Unifier. Česky nejobecnější unifikátor. Cílem je vzít několik různých výrazů a pomocí nahrazování proměnných z nich udělat jeden, naprosto identický výraz.

Anna: Takže sjednocování výrazů. Jak to funguje v praxi?

Lukáš: Ukážeme si to na příkladu. Máme tři predikáty: P(x, g(v), v), pak P(w, z, a) a nakonec P(h(u), u, y). Začneme s prvními dvěma.

Anna: Dobře, jsem připravená.

Lukáš: Jdeme zleva doprava. Porovnáme první pozice: x a w. Jednoduché, nahradíme x za w. Teď máme P(w, g(v), v) a P(w, z, a).

Anna: Super, první kousek shodný. Co dál?

Lukáš: Druhé pozice: g(v) a z. Takže nahradíme proměnnou z celým tím výrazem g(v). A poslední pozice: v a konstanta a. Nahradíme tedy v za a. A pozor, musíme to nahradit všude, takže i uvnitř g(v), ze kterého se stane g(a).

Anna: Takže po první fázi máme z obou výrazů jeden stejný: P(w, g(a), a)?

Lukáš: Přesně tak! A teď tenhle nový výraz porovnáme s tím třetím, P(h(u), u, y). A jedeme znovu zleva.

Anna: Takže w nahradím za h(u). Pak mám g(a) a u, takže u nahradím za g(a). A nakonec a a y, takže y nahradím za konstantu a.

Lukáš: Perfektní! Zvládla jsi to na jedničku. A všechny ty substituce, co jsme udělali, dohromady tvoří ten hledaný nejobecnější unifikátor. Je to vlastně takový recept, jak ty výrazy sjednotit.

Anna: Chápu. Je to takové postupné skládání puzzle. A k čemu přesně je tohle dobré v praxi? To si asi necháme na příště, co?

Anna: Takže unifikace nám pomáhá najít společnou řeč mezi různými výrazy. Ale k čemu to vlastně vede? Co je ten další krok?

Lukáš: Skvělá otázka! Ten další krok je super silná metoda, které se říká rezoluce. Je to vlastně takový logický detektiv.

Anna: Logický detektiv? To zní zajímavě. Co přesně vyšetřuje?

Lukáš: Hledá rozpory! Pointa je najít dva stejné výrazy, kde jeden je v negaci. Třeba P(f(x)) a zároveň ¬P(f(x)). Protože platit obojí najednou je nesmysl, navzájem se vyruší.

Anna: Jasně, jako plus pět a mínus pět. A co když ty výrazy nejsou úplně stejné?

Lukáš: Tak přesně tam nastupuje ta naše unifikace! Použijeme substituci, abychom je sjednotili, a pak je můžeme vyrušit. Ale pozor, musí jít o stejný predikát! Nemůžeš vyrušit P(něco) a ¬S(něco). To by bylo jako sčítat jablka a negované hrušky.

Anna: Dobře, jablka s hruškami ne. Ukaž mi příklad.

Lukáš: Tak třeba máme dva řádky: v jednom je ¬P(f(x,y)) ∨ Q(y) a ve druhém ¬Q(z). Vidíš tam něco, co by se dalo pošťouchnout?

Anna: No, Q(y) a ¬Q(z) vypadají podezřele. Kdybychom za 'z' dosadili 'y'...

Lukáš: Přesně! Substituce z za y, a najednou máme Q(y) a ¬Q(y). Ty se vyruší a zbyde nám jen ¬P(f(x,y)). Jednoduché, že?

Anna: To dává smysl. Ale co když nám tam překáží ty kvantifikátory, to 'pro všechna' a 'existuje'?

Lukáš: Výborný postřeh. Než se pustíme do složitějších rezolucí, musíme si ve vzorcích uklidit. A na to máme Prenexní normální formu, zkráceně PNF.

Anna: Další zkratka! Co znamená?

Lukáš: Cílem je dostat všechny kvantifikátory úplně na začátek formule. Prostě je všechny vystrkáme před závorky.

Anna: A to jde jen tak? Beztrestně je přesouvat?

Lukáš: Skoro. Většinou ano, ale musíš si dát pozor na jednu věc. Pokud přesouváš kvantifikátor, třeba ∃z, přes část formule, kde už nějaké 'z' je, musíš ho přejmenovat. Třeba na 'v'. Jinak by v tom byl zmatek.

Anna: Takže prostě zajistím, aby každé jméno proměnné bylo unikátní v daném kontextu. Logické.

Lukáš: Přesně. A jakmile máme všechny kvantifikátory hezky v řadě na začátku, přichází poslední krok čištění: Skolemizace.

Anna: To zní skoro jako nějaké zaklínadlo.

Lukáš: Trochu. Skolemizací se zbavujeme všech existenčních kvantifikátorů, tedy těch '∃'. Prostě je smažeme.

Anna: Počkat, jen tak je smažeme? To přece změní význam, ne?

Lukáš: Změní, ale kontrolovaně! Místo proměnné, která tam byla, třeba 'z', dosadíme takzvanou Skolemovu funkci. Značíme ji třeba fz. A do závorky té funkce dáme všechny proměnné z '∀' kvantifikátorů, které stály před tím naším '∃z'.

Anna: Aha! Takže pokud bylo na začátku ∀x ∀y ∃z, tak místo 'z' teď budeme psát fz(x,y)?

Lukáš: Bingo! Úplně přesně. A pokud by náhodou žádné '∀' před '∃' nebylo, stane se z toho konstanta. Je to elegantní způsob, jak se zbavit existence a připravit si půdu pro samotnou rezoluci. A právě k té se teď vrátíme u složitějších příkladů.

Anna: ...přesně tak. A to nás skvěle přivádí k dalšímu tématu, kterým jsou studijní poznámky. Mám pocit, že spousta studentů si jen pasivně zapisuje, co slyší.

Lukáš: To je obrovská chyba! Pasivní poznámky jsou skoro k ničemu. Je to jako poslouchat hudbu, ale neslyšet melodii.

Anna: Dobře, tak jak na to jít "aktivně"? Co to přesně znamená v praxi?

Lukáš: Znamená to přemýšlet o tom, co píšeš. Místo doslovného opisování z prezentace se snaž hlavní myšlenky přeformulovat vlastními slovy. Je to obrovský rozdíl.

Anna: Takže moje poznámky, co na střední vypadaly spíš jako abstraktní umění plné šipek a vlastních zkratek, byly vlastně správně?

Lukáš: Přesně tak! Pokud ti to pomohlo si to zapamatovat, bylo to geniální. Cílem není mít krásný sešit pro Instagram, ale funkční poznámky pro tvůj mozek.

Anna: A co takové ty výkřiky do tmy jako "nesnáším tenhle předmět" napsané přes celou stránku? To asi moc nepomůže, co?

Lukáš: To opravdu ne. To je jen ventilace frustrace, ne efektivní učení. Klíčové je oddělit emoce od faktů a snažit se strukturovat i informace, které tě zrovna nebaví.

Anna: Chápu. Takže shrnuto: přemýšlet, přeformulovat a nekreslit si do sešitu naštvané smajlíky. Pojďme se teď podívat na konkrétní metody...

Anna: Tak a na závěr poslední rychlovka. Taková poznávačka. Jsi připravený?

Lukáš: Jsem! Doufám, že nepohořím.

Anna: Dobře. Kdo je ten typický nerd s kulatými brýlemi, který na žádné fotce nemá vousy?

Lukáš: To bude určitě Kurt Gödel. Jasný případ.

Anna: Přesně tak! A co ten, co vypadá trochu jako Mike z Breaking Bad? Plešatý, taky kulaté brýle...

Lukáš: Tenhle popis sedí dokonale na Davida Hilberta. To je skvělá asociace!

Anna: Viď? Dobře, kdo je často vidět s dýmkou, většinou jako starší pán s šedými vlasy?

Lukáš: To je Bertrand Russell. Klasik. Jeho fotky s dýmkou jsou ikonické.

Anna: Perfektní. A poslední... ze všech má nejdelší vousy. A je to snad jediná fotka, kde má vlasy.

Lukáš: Gottlob Frege! Ten jeho plnovous je nezapomenutelný.

Anna: Super, zvládl jsi to na jedničku! A tím jsme na konci dnešního dílu.

Lukáš: Přesně tak. Probrali jsme toho opravdu hodně, od základů výrokové logiky až po slavné logiky a jejich... vousy.

Anna: Přesně tak. Doufáme, že jste si to užili a něco nového se naučili. Díky za poslech!

Lukáš: Mějte se krásně a u dalšího dílu Studyfi Podcastu zase na slyšenou.