Formální a predikátová logika

Ahoj studenti a všichni, kdo se potýkáte s formální a predikátovou logikou! Tato oblast matematiky a informatiky je klíčová pro pochopení principů uvažování a dokazování. V tomto článku si projdeme základní pojmy, metody a ukázky, které vám pomohou lépe se v této fascinující disciplíně zorientovat a uspět u zkoušek. Připravte se na komplexní rozbor a praktické příklady!

Základy Formální a Predikátové Logiky: Co vás čeká?

Formální logika se zabývá správností argumentů a usuzování, nezávisle na obsahu tvrzení. Predikátová logika (často označovaná jako logika 1. řádu) rozšiřuje výrokovou logiku o kvantifikátory a predikáty, což umožňuje pracovat s objekty a jejich vlastnostmi. Představuje mocný nástroj pro reprezentaci znalostí a automatické dokazování.

Následující kapitoly vám poskytnou ucelený přehled klíčových témat, se kterými se setkáte:

• Převod formulí do normálních forem (CNF, DNF)
• Pravdivostní tabulky
• Metoda nejobecnějšího unifikátoru (MGU)
• Pravidlo Modus Ponens
• Převod do prenexní normální formy (PNF)
• Skolemizace
• Teorie s axiomy a modely
• Formulace jazyka predikátové logiky
• Klíčové teoretické otázky
• Rezoluce

Převod formulí do CNF a DNF: Konjunktivní a Disjunktivní normální forma

Práce s formulemi v logice často vyžaduje jejich standardizovaný tvar. Konjunktivní normální forma (CNF) a Disjunktivní normální forma (DNF) jsou takové standardizované tvary. Zde si ukážeme, jak je konstruovat z pravdivostní tabulky a jak převádět složitější formule.

Jak převést formuli do CNF a DNF z tabulky

Disjunktivní normální forma (DNF)

Cílem je najít všechny řádky v pravdivostní tabulce, které mají na konci hodnotu 1. Pro každý takový řádek vytvoříme konjunkci literálů:

• Pokud je hodnota literálu 0, použijeme negaci (např. ¬x).
• Pokud je hodnota literálu 1, použijeme literál (např. x).
• Všechny takto vzniklé konjunkce spojíme disjunkcemi (OR).

Příklad: Pro řádek (¬x ∧ ¬y ∧ z) spojíme výsledné formule disjunkcemi.

Konjunktivní normální forma (CNF)

Cílem je najít všechny řádky v pravdivostní tabulce, které mají na konci hodnotu 0. Pro každý takový řádek vytvoříme disjunkci literálů (přesný opak DNF!):

• Pokud je hodnota literálu 1, použijeme negaci (např. ¬x).
• Pokud je hodnota literálu 0, použijeme literál (např. x).
• Všechny takto vzniklé disjunkce spojíme konjunkcemi (AND).

Příklad: Pro řádek (x ∨ y ∨ z) spojíme výsledné formule konjunkcemi.

Převod složitějších formulí do CNF

Pro převod složitějších logických výrazů do CNF používáme distribuční zákony a De Morganovy zákony. Cílem je mít formuli ve tvaru konjunkce disjunkcí literálů.

Příklad: ¬X ∨ (Y ∧ (¬Z ∨ ¬W)) ⇔ (¬X ∨ Y) ∧ (¬X ∨ ¬Z ∨ ¬W)

Důležitý tip: Vždy si pamatujte na zjednodušování výrazů! Například, (Y ∧ Y ∧ Z) ∨ (Y ∧ ¬Z ∧ ¬Y) lze zjednodušit na (Y ∧ Z) ∨ (0) což je (Y ∧ Z).

MGU: Nejobecnější unifikátor a jeho role

Nejobecnější unifikátor (MGU) je klíčový koncept v predikátové logice, zejména v automatickém dokazování. Cílem MGU je pomocí substituce proměnných z několika výrazů vytvořit jeden stejný výraz. Pokud taková substituce existuje, říkáme, že výrazy jsou unifikovatelné.

Pravidla substituce pro MGU

• Dvě proměnné: Obvykle se substituuje proměnná níže v abecedě za tu výše (např. x za u).
• Proměnná a funkční/predikátový symbol: Vždy substituujeme proměnnou za funkční/predikátový symbol nebo konstantu (např. x za f(y), nebo x za a).
• Dva různé funkční/predikátové symboly: Nelze unifikovat. MGU v takovém případě neexistuje (např. konstanta 'a' a funkce 'f(x)').

Postup krok za krokem při hledání MGU

Podívejme se na příklad unifikace tří výrazů: P(x, g(v), v), P(w, z, a) a P(h(u), u, y).

1. Vyberte dva výrazy: Začneme s P(x, g(v), v) a P(w, z, a).
2. Unifikujte zleva doprava:

• Porovnejte první pozice: x a w. Substituujte x za w. Nové výrazy: P(w, g(v), v) a P(w, z, a). Substituce: G1=[x/w].
• Porovnejte druhé pozice: g(v) a z. Substituujte z za g(v). Nové výrazy: P(w, g(v), v) a P(w, g(v), a). Substituce: G2=[x/w, z/g(v)].
• Porovnejte třetí pozice: v a a (konstanta!). Substituujte v za a. Nezapomeňte nahradit v i uvnitř g(v), takže g(v) se stane g(a). Nové výrazy: P(w, g(a), a) a P(w, g(a), a). Substituce: G3=[x/w, z/g(v), v/a].

3. Vezměte výsledek a unifikujte s dalším výrazem: Nyní máme P(w, g(a), a) a třetí výraz P(h(u), u, y).
4. Pokračujte zleva doprava:

• Porovnejte první pozice: w a h(u). Substituujte w za h(u). Nové výrazy: P(h(u), g(a), a) a P(h(u), u, y). Substituce: G4=[x/w, z/g(v), v/a, w/h(u)].
• Porovnejte druhé pozice: g(a) a u. Substituujte u za g(a). Nezapomeňte nahradit u i uvnitř h(u), takže h(u) se stane h(g(a)). Nové výrazy: P(h(g(a)), g(a), a) a P(h(g(a)), g(a), y). Substituce: G5=[x/w, z/g(v), v/a, w/h(u), u/g(a)].
• Porovnejte třetí pozice: a (konstanta!) a y. Substituujte y za a. Nové výrazy: P(h(g(a)), g(a), a) a P(h(g(a)), g(a), a). Substituce: G6=[x/w, z/g(v), v/a, w/h(u), u/g(a), y/a].

Výsledný nejobecnější unifikátor (MGU) je G6.

Modus Ponens: Základ odvozování v logice

Modus Ponens je jedním z nejdůležitějších odvozovacích pravidel ve výrokové i predikátové logice. Jeho princip je jednoduchý: pokud máme tvrzení A a máme implikaci A → B (tj. „jestliže A, pak B“), pak můžeme odvodit tvrzení B. Symbolicky: z A a A → B odvodíme B.

Příklad použití Modus Ponens v důkazu

Předpokládejme, že máme následující řádky a axiomy (zjednodušený příklad): A1: A → (B → A), A3: (¬B → ¬A) → ((¬B → A) → B).

1. E (předpoklad)
2. E → (¬D → E) (axiom A1, kde A je E, B je ¬D)
3. (¬D → ¬E) → ((¬D → E) → D) (axiom A3, kde A je E, B je D)
4. (¬D → E) (odvozeno z MP(1,2): A=E, A→B = E→(¬D→E), tedy B=(¬D→E))
5. (¬D → ¬E) (předpoklad)
6. ((¬D → E) → D) (odvozeno z MP(5,3): A=(¬D → ¬E), A→B = (¬D → ¬E) → ((¬D→E)→D), tedy B=((¬D→E)→D))
7. D (odvozeno z MP(6,4): A=(¬D → E), A→B = ((¬D → E) → D), tedy B=D)

Prenexní normální forma (PNF) a Skolemizace

Tyto techniky jsou klíčové pro práci s kvantifikátory v predikátové logice a jsou často prvním krokem při přípravě formulí pro rezoluční dokazování.

Převedení do Prenexní normální formy (PNF)

PNF je forma, kde jsou všechny kvantifikátory umístěny na začátku formule, před zbytek výrazu. Proces zahrnuje přesouvání kvantifikátorů přes logické spojky a přejmenování proměnných, aby nedocházelo ke kolizím.

Příklad: Převod formule (prime(x) ∨ odd(z)) → ∀y ((∀z(z = x + y)) → x < y) do PNF.

1. Odstraňte implikace: A → B ⇔ ¬A ∨ B
2. Přesuňte negace: ¬∀x P(x) ⇔ ∃x ¬P(x) a ¬∃x P(x) ⇔ ∀x ¬P(x)
3. Přesuňte kvantifikátory na začátek: Pokud se kvantifikovaná proměnná nevyskytuje ve výrazu, přesuneme kvantifikátor. Pokud se vyskytuje, přejmenujeme ji.

Výsledek v PNF by vypadal například: ∀y ∃v ((¬prime(x) ∧ ¬odd(z)) ∨ ¬(v = x + y) ∨ x < y)

Skolemizace: Odstranění existenčních kvantifikátorů

Skolemizace je proces, jehož cílem je odstranit všechny existenční kvantifikátory (∃) z formule, aniž by se změnila její splnitelnost. Toho dosáhneme nahrazením existenčně kvantifikovaných proměnných Skolemovými konstantami nebo Skolemovými funkcemi.

• Pokud je ∃ kvantifikátor na začátku formule a nepředchází mu žádný ∀ kvantifikátor, nahradíme proměnnou Skolemovou konstantou.
• Pokud ∃ kvantifikátoru předchází jeden nebo více ∀ kvantifikátorů, nahradíme proměnnou Skolemovou funkcí, jejíž argumenty jsou všechny univerzálně kvantifikované proměnné, které předcházely danému existenčnímu kvantifikátoru.

Příklad: ∀x ∀y ∃z(z · y – x = 0 ∧ z + x > 42)

Zde je ∃z, před nímž jsou ∀x a ∀y. Proto z nahradíme Skolemovou funkcí f_z(x,y).

Výsledek: ∀x ∀y (f_z(x,y) · y – x = 0 ∧ f_z(x,y) + x > 42)

Rezoluce: Metoda dokazování sporem

Rezoluce je mocná dokazovací technika, která se používá pro ověření logické platnosti formule (obvykle ve CNF) tím, že se snaží odvodit spor. Základní myšlenka je najít dva klauzule (disjunkce literálů), které obsahují vzájemně negované literály, a ty zrušit. Postupně tak vytváříme nové klauzule, dokud nedosáhneme prázdné klauzule (reprezentující spor).

Cílem je najít dva stejné výrazy, kde jeden z nich je v negaci. Pokud výrazy nejsou stejné, musíme je upravit pomocí substituce, aby byly až na negaci stejné a mohly se navzájem vyrušit.

Příklad: Pokud máme (A ∨ B) a (¬B ∨ C), rezolucí získáme (A ∨ C).

Teorie, modely a jejich vlastnosti

V predikátové logice je teorie množina formulí (axiomů). Model teorie je taková interpretace jazyka (doména a přiřazení symbolům), ve které jsou všechny axiomy teorie pravdivé. Studium modelů nám pomáhá pochopit vlastnosti teorií.

Co je interpretace jazyka predikátové logiky 1. řádu?

Je to dvojice (D, α), kde D je množina (doména) a α je zobrazení, které:

• Každé proměnné přiřazuje hodnotu z domény.
• Každému predikátovému symbolu přiřazuje n-ární relaci na D.
• Každému funkčnímu symbolu přiřazuje funkci z D^n do D.

Je modelem vs. Není modelem

• Je modelem: Prokážeme, že všechny axiomy platí v dané interpretaci. Často se testuje s jedno-prvkovou doménou.
• Není modelem: Stačí najít jeden axiom, který v dané interpretaci neplatí. Často to vyžaduje více-prvkovou doménu.

Další vlastnosti teorií

• Bezesporná teorie: Pokud má alespoň jeden model.
• Úplná teorie: Pokud má (až na izomorfismus) jediný model. Pokud má více modelů, není úplná.

Formulace jazyka predikátové logiky

Jazyk predikátové logiky nám umožňuje formalizovat tvrzení z přirozeného jazyka. Je důležité správně identifikovat predikáty, funkční symboly, konstanty a kvantifikátory.

Klíčové tipy pro formulaci

• Kvantifikátory:
• ∀ (pro všechny) se často pojí s implikací (→).
• ∃ (existuje) se často pojí s konjunkcí (∧).
• Identifikace symbolů: Vždy si ujasněte, které funkční a predikátové symboly máte k dispozici z definice jazyka. Pokud něco chybí (např. 'liché číslo' když máme jen 'sudé'), je třeba to odvodit (např. ¬sudé(x)).
• Různé proměnné: Pamatujte na rozlišení proměnných (např. x < y).

Příklad: „Mezi každými dvěma různými sudými čísly existuje liché číslo.“

∀x ∀y ((even(x) ∧ even(y) ∧ x < y) → ∃z (odd(z) ∧ x < z ∧ z < y))

Teoretické otázky a osobnosti Formální logiky

Pro hlubší pochopení formální a predikátové logiky je dobré znát klíčové teoretické pojmy a osobnosti, které formovaly tuto disciplínu.

Významné teoretické koncepty

• První Gödelova věta o neúplnosti: Žádná efektivní a bezesporná teorie zahrnující Peanovu aritmetiku nemůže být úplná.
• Druhá Gödelova věta o neúplnosti: V žádném bezesporném a efektivním logickém systému zahrnujícím Peanovu aritmetiku není možné dokázat jeho vlastní bezespornost.
• Term predikátové logiky 1. řádu: Proměnná je term. Pokud je f funkční symbol arity n a t1,..., tn jsou termy, potom je f(t1,..., tn) term. Nic jiného není term.
• Důkaz formule φ ve výrokové logice (Hilbertovský): Sekvence formulí končící φ, kde každá formule je buď axiom, nebo je z předchozích odvozena odvozovacím pravidlem.
• Korektnost logického systému: Systém je korektní, pokud vše dokazatelné je platné (⊢φ ⇒ φ|=φ).
• Úplnost (sémantická) logického systému: Systém je úplný, pokud vše platné je dokazatelné (φ|=φ ⇒ ⊢φ).
• Efektivní logický systém: Pokud můžeme ověřit korektnost logického argumentu/důkazu (např. pomocí programu Ověřovač).
• Formule predikátové logiky 1. řádu: Je-li p predikátový symbol s aritou n a t1,...,tn jsou termy, potom je řetězec „p(t1,...,tn)“ formule.
• Rezoluce (ve výrokové logice): Důkaz formule φ z množiny předpokladů P je sekvence formulí patřících buď do P nebo odvozených z předchozích rezolučním pravidlem.

Klíčové postavy Formální logiky

Poznávání těchto osobností je důležité pro pochopení historického kontextu vývoje logiky:

• Kurt Gödel: Známý pro své věty o neúplnosti. Obvykle s kulatými brýlemi, bez vousů.
• David Hilbert: Významný matematik, často bez vlasů, s kulatými brýlemi. Vypadá jako „Mike z Breaking Bad“.
• Bertrand Russell: Filozof a logik, často s dýmkou, šedými vlasy a fotky většinou ze stáří.
• Gottlob Frege: Jeden ze zakladatelů moderní logiky, známý svými dlouhými vousy.

Často kladené otázky k Formální a Predikátové Logice

Co je to term v predikátové logice a proč je důležitý?

Term je základní stavební prvek formule, který reprezentuje objekty. Může to být proměnná, konstanta nebo funkční symbol aplikovaný na jiné termy. Důležitý je, protože umožňuje mluvit o objektech a jejich vztazích v rámci logických výrazů.

Jaký je rozdíl mezi DNF a CNF a kdy se používají?

DNF (Disjunktivní normální forma) je disjunkce konjunkcí literálů, zatímco CNF (Konjunktivní normální forma) je konjunkce disjunkcí literálů. DNF se často používá pro zjednodušování logických obvodů a pro ověření splnitelnosti. CNF je zase klíčová pro rezoluční dokazování, protože většina rezolučních algoritmů vyžaduje, aby formule byly v CNF.

Proč je Modus Ponens tak základní odvozovací pravidlo?

Modus Ponens je základní, protože umožňuje přímo odvozovat nové informace z daných předpokladů. Představuje přirozenou formu usuzování, kterou denně používáme: „Pokud platí A a z A vyplývá B, pak musí platit i B.“ Je stavebním kamenem mnoha formálních důkazů a logických systémů.

Co je to Skolemizace a k čemu slouží?

Skolemizace je metoda pro odstranění existenčních kvantifikátorů (∃) z logických formulí. Slouží k transformaci formulí do tvaru, který je vhodný pro automatické dokazovací techniky, jako je rezoluce. Místo existenčních proměnných zavádí nové konstanty nebo funkce (Skolemovy symboly), což usnadňuje manipulaci s formulemi.

Jak Gödelovy věty o neúplnosti ovlivnily logiku a matematiku?

Gödelovy věty o neúplnosti dramaticky změnily chápání limit formálních systémů. Ukázaly, že žádný dostatečně silný formální systém (který obsahuje aritmetiku) nemůže být současně úplný (schopný dokázat nebo vyvrátit každé pravdivé tvrzení) a bezesporný (neodvodí rozpor). To má hluboké důsledky pro filozofii matematiky a limity lidského poznání.