zkouska.md

Zkouška

výpisky neobsahují kompletní definice pojmů, pouze jejich zjednodušení; k pojmům je vhodné znát příklady

Pojmy

• Model ve výrokové logice, pravdivostní funkce výroku
  • model jazyka je určité pravdivostní ohodnocení proměnných
  • pravdivostní funkce výroku přiřazuje konkrétnímu ohodnocení proměnných nulu nebo jedničku, definuje se induktivně pomocí binárních funkcí
• Sémantické pojmy (pravdivost, lživost, nezávislost, splnitelnost) v logice, vzhledem k teorii
  • pravdivý výrok platí v každém modelu (jazyka/teorie)
    • je pravdivý v logice = platí v logice = je tautologie
    • je pravdivý v T = platí v T = je důsledek T
  • lživý (sporný) výrok neplatí v žádném modelu
  • nezávislý výrok platí v nějakém modelu a neplatí v jiném modelu
  • splnitelný výrok platí v nějakém modelu (tedy není lživý, je pravdivý nebo nezávislý)
• Ekvivalence výroků resp. výrokových teorií, T-ekvivalence
  • výroky/teorie jsou ekvivalentní, když se rovnají jejich množiny modelů
  • výroky/teorie jsou T-ekvivalentní, když se rovnají jejich množiny modelů vzhledem k teorii T
    • $\varphi\sim_T\psi\equiv M_\mathbb P(T,\varphi)=M_\mathbb P(T,\psi)$
    • kde $M_\mathbb P(T,\varphi)\equiv M_\mathbb P(T\cup\set{\varphi})$, což odpovídá $M_\mathbb P(T)\cap M_\mathbb P(\varphi)$
• Sémantické pojmy o teorii (sporná, bezesporná, kompletní, splnitelná)
  • teorie je sporná, jestliže… (ekvivalentně)
    • v ní platí spor
    • nemá žádný model
    • v ní platí všechny výroky
  • teorie je bezesporná (splnitelná), pokud není sporná, tj. má nějaký model
  • teorie je kompletní jestliže není sporná a každý výrok (respektive sentence) je v ní pravdivý nebo lživý (tj. nemá žádné nezávislé výroky), ekvivalentně, pokud má právě jeden model (až na elementární ekvivalenci v predikátové logice)
• Extenze teorie (jednoduchá, konzervativní), odpovídající sémantická kritéria
  • extenze teorie $T$ je libovolná teorie $T'$ v jazyce $\mathbb P'\supseteq\mathbb P$ splňující $\text{Csq}{\mathbb P}(T)\subseteq\text{Csq}{\mathbb P'}(T')$
    • kde $\text{Csq}_\mathbb P(T)$ je množina všech důsledků teorie (výroků/sentencí pravdivých v teorii $T$ v jazyce $\mathbb P$)
  • extenze je jednoduchá, pokud $\mathbb P'=\mathbb P$
  • extenze je konzervativní, pokud $\text{Csq}{\mathbb P}(T)=\text{Csq}{\mathbb P}(T')=\text{Csq}{\mathbb P'}(T')\cap\text{VF}\mathbb P$
  • sémantický význam (v řeči modelů)
    • mějme teorii $T$ v jazyce $\mathbb P$ a teorii $T'$ v jazyce $\mathbb P'$, kde $\mathbb P\subseteq\mathbb P'$
    • $T'$ je jednoduchou extenzí $T$, právě když $\mathbb P'=\mathbb P$ a $M_\mathbb P(T')\subseteq M_\mathbb P(T)$
    • $T'$ je extenzí $T$, právě když $M_{\mathbb P'}(T')\subseteq M_{\mathbb P'}(T)$
    • $T'$ je konzervativní extenzí $T$, pokud je extenzí a navíc platí, že každý model $T$ lze nějak expandovat na model $T'$
    • $T'$ je extenzí $T$ a zároveň $T$ je extenzí $T'$, právě když $T'\sim T$ (jazyky a množiny modelů se rovnají)
    • kompletní jednoduché extenze $T$ jednoznačně až na ekvivalenci odpovídají modelům $T$
• Tablo z teorie, tablo důkaz
  • konečné tablo z teorie $T$ je uspořádaný, položkami označkovaný strom zkonstruovaný aplikací konečně mnoha následujících pravidel:
    • jednoprvkový strom označkovaný libovolnou položkou je tablo z teorie $T$
    • pro libovolnou položku $P$ na libovolné větvi $V$ můžeme na konec větve $V$ připojit atomické tablo pro položku $P$
    • na konec libovolné větve můžeme připojit položku $\text T\alpha$ pro libovolný axiom teorie $\alpha\in T$
  • tablo je konečné nebo nekonečné, každopádně vzniklo ve spočetně mnoha krocích
  • tablo pro položku $P$ je tablo s položkou $P$ v kořeni
  • tablo důkaz výroku $\varphi$ z teorie $T$ je sporné tablo z teorie $T$ s položkou $\text F\varphi$ v kořeni
    • pokud existuje, je $\varphi$ tablo dokazatelný z $T$, píšeme $T\vdash\varphi$
    • podobně definujeme tablo zamítnutí s $\text T\varphi$ v kořeni, tablo zamítnutelnost se značí $T\vdash \neg\varphi$
  • tablo je sporné, pokud je každá jeho větev sporná
  • větev je sporná, pokud obsahuje položky $\text T\psi$ a $\text F\psi$ pro nějaký výrok $\psi$, jinak je bezesporná
  • tablo je dokončené, pokud je každá jeho větev dokončená
  • větev je dokončená…
    • pokud je sporná
    • nebo pokud je každá její položka na této větvi redukovaná a pokud větev zároveň obsahuje položku s T pro každý axiom teorie
  • položka je redukovaná na dané větvi, pokud obsahuje pouze výrokovou proměnnou nebo se na dané větvi vyskytuje jako kořen atomického tabla (tedy došlo k jejímu rozvoji na dané větvi)
  • v predikátové logice navíc řešíme kvantifikátory – položky typu svědek a všichni
• Kanonický model
  • ve výrokové logice
    • je-li $V$ bezesporná větev dokončeného tabla, potom kanonický model pro $V$ je model definovaný předpisem $v(p) = \begin{cases} 1 &\text{pokud }V\text{ obsahuje T}p \ 0 &\text{jinak}\end{cases}$
  • v predikátové logice
    • doména $A$ je množina všech konstantních $L_C$-termů (tzn. s termy zacházíme jako s řetězci)
    • termy jsou v relaci, právě když daná relace je na větvi $V$ s T
    • funkce jsou definovány přímočaře, f("a", "b") = "f(a, b)"
    • konstantní symboly jsou definovány přímočaře
    • u jazyků s rovností definujeme kanonický model jako faktorstrukturu (přičemž tablo je z teorie rozšířené o axiomy rovnosti)
• Kongruence struktury, faktorstruktura, axiomy rovnosti
  • kongruence
    • mějme ekvivalenci $\sim$ na množině $A$, funkci $f:A^n\to A$ a relaci $R\subseteq A^n$
    • říkáme, že $\sim$ je kongruencí pro funkci $f$, pokud pro všechna $x_i,y_i\in A$ taková, že $x_i\sim y_i$ platí $f(x_1,\dots,x_n)\sim f(y_1,\dots,y_n)$
    • říkáme, že $\sim$ je kongruencí pro relaci $R$, pokud pro všechna $x_i,y_i\in A$ taková, že $x_i\sim y_i$ platí $R(x_1,\dots,x_n)$, právě když $R(y_1,\dots,y_n)$
  • kongruence struktury $\mathcal A$ je ekvivalence $\sim$ na množině $A$, která je kongruencí pro všechny funkce a relace $\mathcal A$
  • faktorstruktura
    • mějme strukturu $\mathcal A$ a její kongruenci $\sim$
    • faktorstruktura (podílová struktura) $\mathcal A$ podle $\sim$ je struktura $A/\sim$ v témž jazyce, jejíž univerzum $A/\sim$ je množina všech rozkladových tříd $A$ podle $\sim$ a jejíž funkce a relace jsou definované pomocí reprezentantů, tj.:
      • $f^{\mathcal A/\sim}([x_1]\sim,\dots,[x_n]\sim)=[f^\mathcal A(x_1,\dots,x_n)]\sim$, pro každý $n$-ární funkční symbol $f$
      • $R^{\mathcal A/\sim}([x_1]\sim,\dots,[x_n]_\sim)$, právě když $R^\mathcal A(x_1,\dots,x_n)$, pro každý $n$-ární relační symbol $R$
  • axiomy rovnosti pro jazyk $L$ s rovností jsou
    • $x=x$
    • $x_1=y_1\land\dots\land x_n=y_n\to f(x_1,\dots,x_n)=f(y_1,\dots,y_n)$ pro každý $n$-ární funkční symbol $f$ jazyka $L$
    • $x_1=y_1\land\cdots\land x_n=y_n\to \left(R(x_1,\dots,x_n)\to R(y_1,\dots,y_n)\right)$ pro každý $n$-ární relační symbol $R$ jazyka $L$ včetně rovnosti
  • z 1. a 3. axiomu plyne, že relace $=^\mathcal A$ je ekvivalence na $A$ (symetrie a tranzitivita plyne z 3. axiomu)
  • 2. a 3. axiom vyjadřují, že $=^\mathcal A$ je kongruencí $\mathcal A$
• CNF a DNF, Hornův tvar. Množinová reprezentace CNF formule, splňující ohodnocení
  • tvary výroků
    • literál je prvovýrok nebo negace prvovýroku
      • pro literál $\ell$ označuje $\overline\ell$ literál k němu opačný (tedy jeho negaci)
    • klauzule je disjunkce literálů
      • jednotková klauzule je samotný literál
      • prázdná klauzule je $\bot$
    • výrok je v konjunktivní normální formě (CNF), pokud je konjunkcí klauzulí
      • prázdný výrok v CNF je $\top$
    • elementární konjunkce je konjunkce literálů
      • jednotková elementární konjunkce je samotný literál
      • prázdná elementární konjunkce je $\top$
    • výrok je v disjunktivní normální formě (DNF), pokud je disjunkcí elementárních konjunkcí
      • prázdný výrok v DNF je $\bot$
    • výrok je hornovský (v Hornově tvaru), pokud je konjunkcí hornovských klauzulí, tj. klauzulí obsahujících nejvýše jeden pozitivní literál
  • množinová reprezentace
    • klauzule je konečná množina literálů
      • prázdnou klauzuli označíme $\square$, není nikdy splněna
    • CNF formule je (konečná nebo nekonečná) množina klauzulí
      • prázdná formule $\emptyset$ je vždy splněna
  • ohodnocení ve výrokové logice
    • v množinové reprezentaci odpovídají modely množinám literálů, které obsahují pro každou výrokovou proměnnou $p$ právě jeden z literálů $p,\neg p$
    • (částečné) ohodnocení $\mathcal V$ je libovolná množina literálů, která je konzistentní, tj. neobsahuje dvojici opačných literálů
    • ohodnocení je úplné, pokud obsahuje pozitivní nebo negativní literál pro každou výrokovou proměnnou
    • ohodnocení $\mathcal V$ splňuje formuli $S$, píšeme $\mathcal V\models S$, pokud $\mathcal V$ obsahuje nějaký literál z každé klauzule v $S$, tj.: $\forall C\in S:\mathcal V\cap C\neq\emptyset$
    • splňující ohodnocení nemusí být úplné, ale lze jej rozšířit libovolným literálem pro chybějící proměnné
  • ohodnocení v predikátové logice je funkce $e:\text{Var}\to A$
    • kde $\text{Var}$ je množina všech proměnných jazyka a $A$ je doména
• Rezoluční pravidlo, unifikace, nejobecnější unifikace
  • rezoluční pravidlo ve výrokové logice
    • mějme klauzule $C_1,C_2$ a literál $\ell$, přičemž $\ell\in C_1$ a $\overline\ell\in C_2$
    • potom rezolventa klauzulí $C_1$ a $C_2$ přes literál $\ell$ je klauzule $C=(C_1\setminus\set{\ell})\cup(C_2\setminus\set{\overline\ell})$
  • rezoluční pravidlo v predikátové logice
    • mějme klauzule $C_1,C_2$ s disjunktními množinami proměnných
    • v klauzuli $C_1$ jsou mj. výrazy $A_1,\dots,A_n$
    • v klauzuli $C_2$ jsou mj. výrazy $\neg B_1,\dots,\neg B_m$
    • množina výrazů $S=\set{A_1,\dots,A_n,B_1,\dots,B_m}$ má nejobecnější unifikaci $\sigma$ takovou, že $S\sigma=\set{A_1\sigma}$
    • rezolventa klauzulí $C_1$ a $C_2$ je klauzule $C=C'1\sigma\cup C_2'\sigma$, kde $C'*$ odpovídá zbytku klauzule po odstranění výrazů $A_i$, respektive $\neg B_i$
  • substituce
    • substituce je konečná množina $\sigma=\set{x_1/t_1,\dots,x_n/t_n}$, kde $x_i$ jsou navzájem různé proměnné a $t_i$ jsou termy, přičemž vyžadujeme, aby $t_i\neq x_i$
    • substituce je základní, jsou-li všechny $t_i$ konstantní
    • substituce je přejmenování proměnných, jsou-li všechny $t_i$ navzájem různé proměnné
    • substituce lze skládat (klasicky v pořadí zleva doprava), skládání je asociativní
  • unifikace
    • mějme konečnou množinu výrazů $S=\set{E_1,\dots,E_n}$
    • substituce $\sigma$ je unifikace pro $S$, pokud $E_1\sigma=E_2\sigma=\dots=E_n\sigma$, neboli $S\sigma$ obsahuje jediný výraz
    • pokud existuje, říkáme, že $S$ je unifikovatelná
  • nejobecnější unifikace
    • unifikace $\sigma$ pro $S$ je nejobecnější, pokud pro každou unifikaci $\tau$ pro $S$ existuje substituce $\lambda$ taková, že $\tau=\sigma\lambda$
    • nejobecnějších unifikací může být více, liší se přejmenováním proměnných
• Rezoluční důkaz a zamítnutí, rezoluční strom
  • rezoluční důkaz (odvození) klauzule $C$ z formule $S$ je konečná posloupnost klauzulí $C_0,C_1,\dots,C_n=C$ taková, že
    • pro každé $i$ je buď $C_i\in S$
      • v predikátové logice dovolujeme přejmenování proměnných: $C_i=C_i'\sigma$ pro $C'_i\in S$ a přejmenování proměnných $\sigma$
    • nebo $C_i$ je rezolventou nějakých $C_j,C_k$, kde $j\lt i$ a $k\lt i$
  • pokud rezoluční důkaz existuje, říkáme, že $C$ je rezolucí dokazatelná z $S$ a píšeme $S\vdash_R C$
  • rezoluční zamítnutí formule $S$ je rezoluční důkaz $\square$ z $S$, v tom případě je $S$ rezolucí zamítnutelná
  • rezoluční strom klauzule $C$ z formule $S$ je konečný binární strom s vrcholy označenými klauzulemi, kde v kořeni je $C$, v listech jsou klauzule z $S$ a v každém vnitřním vrcholu je rezolventa klauzulí ze synů tohoto vrcholu
• Vysvětlete rozdíl mezi rezolučním důkazem, lineárním důkazem, a LI-důkazem
  • lineární důkaz i LI-důkaz jsou zvláštními případy rezolučního důkazu
  • lineární důkaz vypadá tak, že vždy nějakou centrální klauzuli rezolvujeme s boční klauzulí, čímž vznikne další centrální klauzule
    • centrální klauzule vznikají rezolucí předchozí dvojice klauzulí
    • boční klauzule jsou z $S$ nebo se jedná o minulé centrální klauzule (vzniklé rezolucí)
  • LI-důkaz požaduje, aby všechny boční klauzule byly z $S$
    • LI-rezoluce není úplná pro obecné formule (ne každá nesplnitelná formule má LI-zamítnutí)
    • LI-rezoluce je úplná pro Hornovy formule
• Signatura a jazyk predikátové logiky, struktura daného jazyka
  • signatura je dvojice $\braket{\mathcal {R,F}}$, kde $\mathcal{R,F}$ jsou disjunktní množiny symbolů (relační a funkční, ty zahrnují konstantní) spolu s danými aritami a neobsahují symbol $=$
  • do jazyka patří…
    • spočetně mnoho proměnných
    • relační, funkční a konstantní symboly ze signatury a symbol $=$, jde-li o jazyk s rovností
    • univerzální a existenční kvantifikátory pro každou proměnnou
    • symboly pro logické spojky a závorky
  • struktura v signatuře $\braket{\mathcal{R,F}}$ je trojice $\mathcal A=\braket{A,\mathcal{R^A,F^A}}$, kde…
    • $A$ je neprázdná množina, říkáme jí doména (také universum)
    • $\mathcal {R^A}$ je množina interpretací jednotlivých relačních symbolů (kde interpretace $n$-árního relačního symbolu je množina uspořádaných $n$-tic prvků z $A$)
    • $\mathcal {F^A}$ je množina interpretací jednotlivých funkčních symbolů (kde intepretace $n$-árního funkčního symbolu odpovídá funkci přiřazující $n$-tici prvků z $A$ jeden prvek z $A$)
      • speciálně pro konstantní symbol $c\in\mathcal F$ je $c^\mathcal A\in A$
  • model jazyka $L$ nebo také $L$-struktura je libovolná struktura v signatuře jazyka $L$
  • třídu všech modelů jazyka označíme $M_L$
• Atomická formule, formule, sentence, otevřené formule
  • termy jazyka $L$ jsou konečné nápisy definované induktivně
    • proměnná je term
    • konstantní symbol je term
    • pro $n$-ární funkční symbol $f$ a termy $t_1,\dots,t_n$ je nápis $f(t_1,\dots,t_n)$ také term
  • atomická formule jazyka $L$ je nápis $R(t_1,\dots,t_n)$, kde $R$ je $n$-ární relační symbol z $L$ (v jazyce s rovností to může být i rovnost) a $t_i$ je $L$-term
  • formule jazyka $L$ jsou konečné nápisy definované induktivně
    • atomická formule je formule
    • negace formule je formule
    • spojením dvou formulí binární logickou spojkou dostaneme formuli
    • přidáním kvantifikátoru před formuli dostaneme formuli
  • výskyt proměnné je vázaný, pokud jí odpovídá nějaký kvantifikátor, jinak je výskyt volný
  • proměnná je volná, pokud má volný výskyt, je vázaná, pokud má vázaný výskyt
  • formule je otevřená, neobsahuje-li žádný kvantifikátor
  • formule je uzavřená (= sentence), pokud nemá žádnou volnou proměnnou
• Instance formule, substituovatelnost, varianta formule
  • term $t$ je substituovatelný za proměnnou $x$ ve formuli $\varphi$, pokud po simultánním nahrazení všech volných výskytů $x$ ve $\varphi$ za $t$ nevznikne ve $\varphi$ žádný vázaný výskyt proměnné z $t$
    • v tom případě říkáme vzniklé formuli instance $\varphi$ vzniklá substitucí $t$ za $x$ a označujeme ji $\varphi(x/t)$
  • má-li formule $\varphi$ podformuli tvaru $(Qx)\psi$ a je-li $y$ proměnná taková, že $y$ je substituovatelná za $x$ do $\psi$ a $y$ nemá volný výskyt v $\psi$, potom nahrazením podformule $(Qx)\psi$ formulí $(Qy)\psi(x/y)$ vznikne varianta formule $\varphi$ v podformuli $(Qx)\psi$
  • poznámka: substituce = dosazování za volné výskyty proměnných, naopak varianty formulí vznikají přejmenováním vázaných výskytů (volné výskyty nelze přejmenovat, aby se nezměnilo „rozhraní“ neuzavřené formule)
• Pravdivostní hodnota formule ve struktuře při ohodnocení, platnost formule ve struktuře
  • hodnota termu vyplývá jednoduše z ohodnocení (u konstant nezávisí na ohodnocení, u proměnných přímo z ohodnocení, u funkcí se dosadí hodnoty termů a získá se výsledná hodnota)
  • pravdivostní hodnoty formule při ohodnocení
    • pravdivostní hodnota je rovna nule nebo jedné
    • pravdivostní hodnota atomické formule vyplývá z toho, zda je daná $n$-tice (pro určité hodnoty termů) prvkem odpovídající množiny z $R^\mathcal A$
    • pro logické spojky se pravdivostní hodnota určuje standardně
    • obecný kvantifikátor lze chápat jako hledání minima z pravdivostních hodnot (nebo jako konjunkci přes všechny prvky struktury)
    • podobně existenční kvantifikátor hledá maximum / je to disjunkce
  • platnost ve struktuře
    • mějme formuli $\varphi$ a strukturu $\mathcal A$
    • je-li $e$ ohodnocení a $\text{PH}^\mathcal A(\varphi)[e]=1$, potom říkáme, že $\varphi$ platí v $\mathcal A$ při ohodnocení $e$ a píšeme $A\models\varphi[e]$
    • pokud $\varphi$ platí v $\mathcal A$ při každém ohodnocení $e:\text{Var}\to A$, potom říkáme, že $\varphi$ je pravdivá (platí) v $\mathcal A$, a píšeme $\mathcal A\models\varphi$
    • naopak pokud $\mathcal A\models\neg\varphi$, tj. $\varphi$ neplatí v $\mathcal A$ při žádném ohodnocení, pak je lživá v $\mathcal A$
• Kompletní teorie v predikátové logice, elementární ekvivalence
  • teorie je kompletní, je-li bezesporná a každá sentence je v ní buď pravdivá, nebo lživá
  • pozorování: teorie je kompletní, právě když má právě jeden model až na elementární ekvivalenci
  • struktury $\mathcal{A,B}$ (v témž jazyce) jsou elementárně ekvivalentní, pokud v nich platí tytéž sentence (značíme $\mathcal A\equiv \mathcal B$)
    • zjevně $\mathcal A\equiv \mathcal B\iff\text{Th}(\mathcal A)=\text{Th}(\mathcal B)$
• Podstruktura, generovaná podstruktura, expanze a redukt struktury
  • $\mathcal B$ je (indukovaná) podstruktura $\mathcal A$, když je $B$ neprázdnou podmnožinou $A$, každá množina odpovídající interpretaci relace je omezena na $n$-tice z $B$ a podobně funkce směřují z $B$ do $B$, zároveň interpretace všech konstantních symbolů musí být v $B$
  • pozorování: univerzum podstruktury musí být uzavřené na všechny funkce původní struktury
  • podstruktura struktury $\mathcal A$ generovaná množinou $X$ se značí $\mathcal A\langle X\rangle$, její univerzum je nejmenší podmnožina $A$, která obsahuje množinu $X$ a je uzavřená na všechny funkce struktury $\mathcal A$ (tedy rovněž obsahuje všechny konstanty), tuto podmnožinu označme jako $B$
    • takovou podstrukturu lze také zapsat jako $\mathcal A\restriction B$
    • pokud $\mathcal A$ nemá žádné funkce ani konstanty (např. je to graf nebo uspořádání), tak není čím generovat, tedy $\mathcal A\langle X\rangle=\mathcal A\restriction X$
  • expanze a redukt jsou dvě struktury se stejnou doménou, kde expanze je nad větším jazykem, přičemž všechny symboly z menšího jazyka jsou v obou strukturách interpretovány stejně (jako relační/funkční/konstantní)
• Definovatelnost ve struktuře
  • množina definovaná formulí = množina uspořádaných $n$-tic, které splňují danou formuli
    • $\varphi^\mathcal A(\overline x)=\set{\overline a\in A^n\mid\mathcal A\models\varphi[e(\overline x/\overline a)]}$
    • kde $|\overline x|=n$, $\varphi$ má $n$ volných proměnných $x_1,\dots,x_n$
    • příklady
      • $\neg(\exists y)E(x,y)$ … izolované vrcholy v grafu
      • $x\leq y\land \neg(x=y)$ … relace ostrého uspořádání
  • množina definovaná formulí s parametry = množina uspořádaných $n$-tic, které splňují danou formuli s určenými parametry
    • $\varphi^{\mathcal A,\overline b}(\overline x,\overline y)=\set{\overline a\in A^n\mid\mathcal A\models\varphi[e(\overline x/\overline a,\overline y/\overline b)]}$
    • kde $|\overline x|=n$, $|\overline y|=k$, $\varphi$ má $n+k$ volných proměnných
    • příklad: pro $\varphi(x,y)=E(x,y)$ je $\varphi^{\mathcal G,v}(x,y)$ množina všech sousedů vrcholu $v$
  • pro strukturu $\mathcal A$ a podmnožinu $B\subseteq A$ označíme $\text{Df}^n(\mathcal A, B)$ množinu všech množin definovatelných ve struktuře $\mathcal A$ s parametry pocházejícími z $B$
• Extenze o definice
  • definice relačního symbolu
    • $T$ a $\psi$ jsou v jazyce $L$
    • rozšíříme jazyk o nový relační symbol $R$, dostaneme $L'$
    • extenze teorie $T$ o definici $R$ formulí $\psi$ je $L'$-teorie $T'=T\cup\set{R(x_1,\dots,x_n)\leftrightarrow\psi(x_1,\dots,x_n)}$
    • např. $x_1\leq x_2\leftrightarrow(\exists y)(x_1+y=x_2)$
  • definice funkčního symbolu
    • mějme $T$ a formuli $\psi(x_1,\dots,x_n,y)$ v jazyce $L$
    • rozšíříme $L$ o funkční symbol $f$, dostaneme $L'$
    • nechť v $T$ platí…
      • axiom existence $(\exists y)\psi(x_1,\dots,x_n,y)$
      • axiom jednoznačnosti $\psi(x_1,\dots,x_n,y)\land\psi(x_1,\dots,x_n,z)\to y=z$
    • potom extenze teorie $T$ o definici $f$ formulí $\psi$ je $L'$-teorie $T'=T\cup\set{f(x_1,\dots,x_n)=y\leftrightarrow\psi(x_1,\dots,x_n,y)}$
    • např. $x_1-_b x_2=y\leftrightarrow x_1+(-x_2)=y$
  • definice konstantního symbolu
    • jako funkční symbol
    • axiom existence $(\exists y)\psi(y)$
    • axiom jednoznačnosti $\psi(y)\land\psi(z)\to y=z$
    • $T'=T\cup\set{c=y\leftrightarrow\psi(y)}$
    • např. $1/2=y\leftrightarrow y\cdot (1+1)=1$
  • $T'$ je extenzí $T$ o definice, pokud vznikla z $T$ postupnou extenzí o definice relačních a funkčních (případně konstantních) symbolů
  • vlastnosti extenzí o definice
    • každý model teorie $T$ lze jednoznačně expandovat na model $T'$
    • $T'$ je konzervativní extenze $T$
    • pro každou $L'$-formuli $\varphi'$ existuje $L$-formule $\varphi$ taková, že $T'\models\varphi'\leftrightarrow\varphi$
• Prenexní normální forma, Skolemova varianta
  • PNF = kvantifikátory jsou před formulí, formule se dělí na kvantifikátorový prefix a otevřené jádro
  • převod na PNF – postupně kvantifikátory vytahuju (podle pravidel), v případě potřeby přejmenuju proměnnou, tím vznikne varianta (pokud je v druhé části formule volná proměnná se stejným názvem)
  • Skolemova varianta sentence vzniká z původní PNF sentence skolemizací
    • skolemizace spočívá v tom, že tyto kroky iterujeme přes všechny existenční kvantifikátory $(\exists y_i)$
      • odstraníme z prefixu existenční kvantifikátor $(\exists y_i$)
      • za proměnnou $y_i$ substituujeme term $f_i(x_1,\dots,x_{n_i})$, kde $x_1,\dots,x_{n_i}$ jsou proměnné, jejichž univerzální kvantifikátory předcházejí $(\exists y_i)$
    • začínáme s $L$-sentencí v PNF, jejíž všechny vázané proměnné jsou různé
    • dostaneme $L'$-sentenci v PNF, kde $L'$ je rozšíření $L$ o nové $n_i$-ární funkční symboly
• Izomorfismus struktur, izomorfní spektrum, $\omega$-kategorická teorie
  • izomorfismus struktur
    • mějme struktury $\mathcal{A,B}$ jazyka $L=\braket{\mathcal{R,F}}$
    • izomorfismus $\mathcal{A}$ a $\mathcal B$ je bijekce $h:A\to B$ splňující následující vlastnosti:
      • $(\forall f\in\mathcal F)(\forall a_i\in A):h(f^\mathcal A(a_1,\dots,a_n))=f^\mathcal B(h(a_1),\dots,h(a_n))$
      • $(\forall R\in\mathcal R)(\forall a_i\in A):$ $R^\mathcal A(a_1,\dots,a_n)\iff R^\mathcal B(h(a_1),\dots,h(a_n))$
    • pak píšeme $\mathcal A\simeq \mathcal B$
  • izomorfní spektrum
    • izomorfní spektrum teorie $T$ je počet $I(\kappa,T)$ modelů $T$ kardinality $\kappa$ až na izomorfismus pro každou kardinalitu $\kappa$
    • teorie $T$ je $\kappa$-kategorická, pokud $I(\kappa,T)=1$
    • např.
      • $I(\kappa,DeLO^*)=0$ pro $\kappa\in\mathbb N$
      • $I(\omega,DeLO^*)=4$
      • $I(\omega,DeLO)=1\implies DeLO$ je $\omega$-kategorická
  • $\omega$-kategorická teorie má jeden spočetně nekonečný model až na izomorfismus
• Axiomatizovatelnost, konečná axiomatizovatelnost, otevřená axiomatizovatelnost
  • mějme třídu struktur $K\subseteq M_L$ v jazyce $L$
  • říkáme, že $K$ je…
    • axiomatizovatelná, pokud existuje $L$-teorie $T$ taková, že $M_L(T)=K$
    • konečně axiomatizovatelná, pokud je axiomatizovatelná konečnou teorií
    • otevřeně axiomatizovatelná, pokud je axiomatizovatelná otevřenou teorií
  • o $L$-teorii $T'$ říkáme, že je konečně/otevřeně axiomatizovatelná, pokud to platí o třídě modelů $K=M_L(T')$
    • tzn. existuje nějaká teorie, která má danou vlastnost (je konečná/otevřená) a popisuje danou třídu modelů
  • příklady
    • grafy nebo částečná uspořádání jsou konečně i otevřeně axiomatizovatelné
    • tělesa jsou konečně, ale ne otevřeně axiomatizovatelná
    • nekonečné grupy jsou axiomatizovatelné, ale ne konečně
    • konečné grafy nejsou axiomatizovatelné
      • jsme schopni axiomatizovat grafy na $k$ vrcholech, ale ne všechny konečné grafy
• Rekurzivní axiomatizace, rekurzivní axiomatizovatelnost, rekurzivně spočetná kompletace
  • teorie $T$ je rekurzivně axiomatizovaná, pokud existuje algoritmus, který pro každou vstupní formuli $\varphi$ doběhne a odpoví, zda $\varphi\in T$
  • třída $L$-struktur $K\subseteq M_L$ je rekurzivně axiomatizovatelná, pokud existuje rekurzivně axiomatizovaná $L$-teorie $T$ taková, že $K=M_L(T)$
  • teorie $T'$ je rekurzivně axiomatizovatelná, pokud je rekurzivně axiomatizovatelná třída jejích modelů, neboli pokud je $T'$ ekvivalentní nějaké rekurzivně axiomatizované teorii
  • řekneme, že teorie $T$ má rekurzivně spočetnou kompletaci, pokud (nějaká) množina (až na ekvivalenci) všech jednoduchých kompletních extenzí teorie $T$ je rekurzivně spočetná, tj. existuje algoritmus, který pro danou vstupní dvojici přirozených čísel $(i,j)$ vypíše na výstup $i$-tý axiom $j$-té extenze (v nějakém pevně daném uspořádání), nebo odpoví, že takový axiom už neexistuje
• Rozhodnutelná a částečně rozhodnutelná teorie
  • o teorii $T$ říkáme, že je…
    • rozhodnutelná, pokud existuje algoritmus, který pro každou vstupní formuli $\varphi$ doběhne a odpoví, zda $T\models\varphi$
    • částečně rozhodnutelná, pokud existuje algoritmus, který pro každou vstupní formuli $\varphi$…
      • pokud $T\vDash\varphi$, doběhne a odpoví „ano“
      • pokud $T\nvDash\varphi$, buď nedoběhne, nebo doběhne a odpoví „ne“

Lehké otázky

• Množinu modelů nad konečným jazykem lze axiomatizovat výrokem v CNF, výrokem v DNF
  • tvrzení
    • mějme konečný jazyk $\mathbb P$ a libovolnou množinu modelů $M\subseteq M_\mathbb P$
    • potom existuje výrok $\varphi_\text{DNF}$ v DNF a výrok $\varphi_\text{CNF}$ v CNF takový, že $M=M_\mathbb P(\varphi_\text{DNF})=M_\mathbb P(\varphi_\text{CNF})$
    • konkrétně
      • $\varphi_\text{DNF}=\bigvee_{v\in M}\bigwedge _{p\in\mathbb P} p^{v(p)}$
      • $\varphi_\text{CNF}=\bigwedge_{v\in \overline M}\bigvee_{p\in\mathbb P} \overline{p^{v(p)}}$
  • důkaz
    • pro $\varphi_\text{DNF}$ jednoduché, každá elementární konjunkce popisuje jeden model
      • stejný mechanismus se používá pro důkaz univerzálnosti $\set{\neg,\land,\lor}$
    • výrok $\varphi_\text{CNF}$ je duální k výroku $\varphi'_\text{DNF}$ sestrojenému pro doplněk $M'=\overline M$
      • nebo můžeme dokázat přímo – každá klauzule zakazuje právě jeden nemodel
• 2-SAT, Algoritmus implikačního grafu, jeho korektnost
  • výrok $\varphi$ je v $k$-CNF, pokud je v CNF a každá klauzule má nejvýše $k$ literálů
  • $k$-SAT se ptá, zda je formule v $k$-CNF splnitelná
  • algoritmus implikačního grafu pro 2-SAT
    • klauzuli $a\lor b$ vyjádříme jako dvě implikace $\overline a\to b,;\overline b\to a$
    • jednotkovou klauzuli $c$ zapíšeme jako $\overline c\to c$
    • implikační graf $\mathcal G_\varphi$ je orientovaný graf, jehož vrcholy jsou všechny literály a hrany jsou dané implikacemi (viz výše)
    • v grafu najdeme komponenty silné souvislosti
      • všechny literály v jedné komponentě musí být ohodnoceny stejně
    • provedeme kontrakci komponent, dostaneme orientovaný acyklický graf $\mathcal G^*_\varphi$
      • postupujeme podle topologického uspořádání, vezmeme nejlevější neohodnocenou komponentu, ohodnotíme ji 0, opačnou komponentu ohodnotíme 1
  • algoritmus běží v lineárním čase, protože komponenty silné souvislosti i topologické uspořádání lze nalézt v čase $O(n+m)$
  • korektnost plyne z tvrzení, že výrok je splnitelný, právě když žádná komponenta silné souvislosti neobsahuje dvojici opačných literálů
    • implikaci $\implies$ lze nahlédnout obměnou
      • kdyby komponenta obsahovala dvojici opačných literálů, existovala by implikace $1\to 0$
    • opačná implikace
      • model jsme získali postupem uvedeným výše (pomocí topologického uspořádání grafu komponent)
      • kdyby v tomto modelu původní výrok neplatil, neplatila by některá z klauzulí
      • u jednotkových klauzulí máme hranu $\overline c\to c$ (stejná hrana je i na úrovni grafu komponent), tudíž jsme nutně ohodnotili $\overline c$ dříve než $c$, tedy $c=1$
      • u 2-klauzulí máme dvě hrany a čtyři různé literály, dvě různé proměnné – jednu z nich jsme ohodnotili jako první, ta zaručí platnost klauzule
      • tedy všechny klauzule platí
• Horn-SAT, Algoritmus jednotkové propagace, jeho korektnost
  • výrok je hornovský, pokud je konjunkcí hornovských klauzulí, tj. klauzulí obsahujících nejvýše jeden pozitivní literál
  • algoritmus
    • pokud $\varphi$ obsahuje dvojici opačných jednotkových klauzulí, není splnitelný
    • pokud $\varphi$ neobsahuje žádnou jednotkovou klauzuli, je splnitelný, ohodnotíme všechny zbývající proměnné nulou
    • pokud $\varphi$ obsahuje jednotkovou klauzuli $\ell$, ohodnotíme literál $\ell$ hodnotou 1, provedeme jednotkovou propagaci a postup opakujeme
  • jednotková propagace pro $\ell=1$
    • každou klauzuli obsahující $\ell$ odstraníme (protože je takto splněna)
    • $\overline\ell$ odstraníme ze všech klauzulí, které ho obsahují (protože $\overline\ell$ nemůže zajistit splnění dané klauzule)
  • korektnost
    • korektnost jednotkové propagace je popsána výše
    • ohodnocení zbývajících proměnných nulou je zjevně korektní, neboť každá hornovská „nejednotková“ klauzule obsahuje negativní literál, který tak zajistí splnění klauzule
  • Horn-SAT lze řešit v lineárním čase
    • kvadratický horní odhad lze nahlédnout tak, že v každém kroku výrok procházíme jednou a jednotková propagace ho vždy zkrátí
• Algoritmus DPLL pro řešení SAT
  • literál $\ell$ má čistý výskyt ve $\varphi$, pokud se $\ell$ vyskytuje ve $\varphi$ a opačný literál $\overline\ell$ se ve $\varphi$ nevyskytuje
    • takový literál můžu nastavit na 1
    • to neovlivní splnitelnost výroku, ale zmenší to množinu modelů, které jsem schopen nalézt
  • algoritmus
    • dokud $\varphi$ obsahuje jednotkovou klauzuli $\ell$, ohodnoť $\ell=1$ a proveď jednotkovou propagaci
    • dokud existuje literál $\ell$, který má ve $\varphi$ čistý výskyt, ohodnoť $\ell=1$ a odstraň klauzule obsahující $\ell$
    • pokud $\varphi$ neobsahuje žádnou klauzuli, je splnitelný
    • pokud $\varphi$ obsahuje prázdnou klauzuli, není splnitelný
    • jinak zvol dosud neohodnocenou výrokovou proměnnou $p$ a zavolej algoritmus rekurzivně na $\varphi\land p$ a na $\varphi\land\neg p$
  • algoritmus běží v exponenciálním čase
• Věta o konstantách
  • věta
    • mějme formuli $\varphi$ v jazyce $L$ s volnými proměnnými $x_1,\dots,x_n$
    • označme $L'$ rozšíření jazyka o nové konstantní symboly $c_1,\dots,c_n$ a buď $T'$ stejná teorie jako $T$, ale v jazyce $L'$
    • potom platí $T\models\varphi$, právě když $T'\models\varphi(x_1/c_1,\dots,x_n/c_n)$
  • poznámka: funguje to, protože nové konstantní symboly můžou být v modelech interpretovány jako libovolné prvky
  • důkaz $\implies$
    • je-li $\mathcal A'$ model teorie $T'$, nechť $\mathcal A$ je jeho redukt na $L$
    • jelikož $\mathcal A\models\varphi[e]$ pro každé ohodnocení $e$, pak to platí i pro ohodnocení, kde hodnoty proměnných odpovídají konstantám z $\mathcal A'$
  • důkaz $\impliedby$
    • je-li $\mathcal A$ model teorie $T$ a $e$ libovolné ohodnocení, nechť $\mathcal A'$ je expanze $\mathcal A$ na $L'$ o konstanty $c_i^{A'}=e(x_i)$
    • jelikož $\mathcal A'\models\varphi(x_1/c_1,\dots,x_n/c_n)[e']$ pro libovolné $e'$, platí i $\mathcal A'\models\varphi[e]$
    • protože konstantní symboly jsou nové, platí i $\mathcal A\models\varphi[e]$
• Vlastnosti extenze o definice
  • je-li $T'$ extenze teorie $T$ o definice, potom platí:
    • každý model teorie $T$ lze jednoznačně expandovat na model $T'$
    • $T'$ je konzervativní extenze $T$
    • pro každou $L'$-formuli $\varphi'$ existuje $L$-formule $\varphi$ taková, že $T'\models\varphi'\leftrightarrow\varphi$
  • důkaz
    • k expanzi modelu stačí přidat odpovídající relační a funkční symboly
    • konzervativní extenze – vyplývá z tvrzení:
      • mějme jazyky $L\subseteq L'$, teorii $T$ v $L$ a teorii $T'$ v $L'$
      • (i) $T'$ je extenzí $T$, právě když redukt každého modelu $T'$ na $L$ je modelem $T$
        • důkaz $\implies$
          • mějme $\mathcal A'\models T'$ a $\mathcal A$, což je redukt $\mathcal A'$ na jazyk $L$
          • $T'$ je extenzí $T$, takže v $T'$ platí každý axiom $\varphi\in T$
          • tudíž $\mathcal A'\models\varphi$
          • proto i $\mathcal A\models\varphi$, neboť $\varphi$ obsahuje jen symboly z $L$
          • takže $\mathcal A\models T$
        • důkaz $\impliedby$
          • mějme $L$-sentenci $\varphi$ takovou, že $T\models\varphi$
          • pro libovolný model $\mathcal A'\models T'$ víme, že jeho $L$-redukt $\mathcal A$ je modelem $T$
          • tedy $\mathcal A\models\varphi$
          • proto $\mathcal A'\models\varphi$
          • tedy i $T'\models\varphi$
      • (ii) pokud je $T'$ extenzí $T$ a každý model $T$ lze expandovat do $L'$ na nějaký model $T'$, potom je $T'$ konzervativní extenzí $T$
        • důkaz $\implies$
          • vezměme libovolnou $L$-sentenci $\varphi$, která platí v $T'$
          • každý model $\mathcal A\models T$ lze expandovat na nějaký model $\mathcal A'\models T'$
          • víme, že $\mathcal A'\models\varphi$
          • takže i $\mathcal A\models\varphi$
          • tudíž $T\models\varphi$
    • $T'\models\varphi'\leftrightarrow\varphi$
      • pro relační symbol $R$
        • v definici máme ekvivalenci $R\leftrightarrow\psi$
        • $\varphi$ vznikne tak, že nahradíme atomické podformule s novým symbolem $R$ formulí $\psi'$, což je varianta $\psi$ zaručující substituovatelnost všech termů
          • tedy $R(t_1,\dots,t_n)$ nahradíme $\psi'(x_1/t_1,\dots,x_n/t_n)$
        • substituovatelnost se dá zaručit třeba přejmenováním všech vázaných proměnných $\psi$ na zcela nové
      • pro funkční symbol $f$
        • v definici máme $f(x_1,\dots,x_n)=y\leftrightarrow\psi(x_1,\dots,x_n,y)$
        • u více výskytů $f$ aplikujeme tento postup několikrát, v případě vnoření postupujeme od vnitřních
        • jako $\varphi^*$ označíme formuli vzniklou z $\varphi'$ nahrazením termu $f(t_1,\dots,t_n)$ novou proměnnou $z$
        • $\varphi$ dostaneme takto: $(\exists z)(\varphi^*\land\psi'(x_1/t_1,\dots,x_n/t_n,y/z))$
        • opět $\psi'$ je varianta zaručující substituovatelnost
        • díky této konstrukci a vlastnostem $T$ (axiomům jednoznačnosti a existence $z$) platí $T'\models\varphi'\leftrightarrow\varphi$
• Vztah definovatelných množin a automorfismů
  • tvrzení
    • je-li $D\subseteq A^n$ definovatelná ve struktuře $\mathcal A$, potom pro každý automorfismus $h\in\text{Aut}(\mathcal A)$ platí $h[D]=D$, kde $h[D]$ značí $\set{h(\overline a)\mid\overline a\in D}$
    • je-li $D$ definovatelná s parametry $\overline b$, platí totéž pro automorfismy identické na $\overline b$, tj. takové, že $h(\overline b)=\overline b$ (neboli $\forall i:h(b_i)=b_i$)
  • důkaz (pro verzi s parametry)
    • nechť $D=\varphi^{\mathcal A,\overline b}(\overline x,\overline y)$
    • potom pro každé $\overline a \in A^n$ platí
      • $\overline a\in D$
      • $\iff\mathcal A\models\varphi[e(\overline x/\overline a,\overline y/\overline b)]$
      • $\iff\mathcal A\models\varphi[(e\circ h)(\overline x/\overline a,\overline y/\overline b)]$
        • protože to je izomorfismus
      • $\iff\mathcal A\models\varphi[e(\overline x/h(\overline a),\overline y/h(\overline b))]$
      • $\iff\mathcal A\models\varphi[e(\overline x/h(\overline a),\overline y/\overline b)]$
        • protože na $\overline b$ je v tomhle automorfismu identita (z předpokladů tvrzení)
      • $\iff h(\overline a)\in D$
• Tablo metoda v jazyce s rovností
  • chceme, aby v nějakém modelu $\mathcal A$ teorie $T$ v jazyce s rovností byla relace $=^\mathcal A$ kongruencí
    • toho docílíme tak, že k teorii $T$ přidáme axiomy rovnosti – tablo sestavíme z výsledné teorie $T^*$
  • kongruence nám ale nestačí, chceme, aby rovnost byla identita, proto budeme všechny $=^\mathcal A$-ekvivalentní prvky „identifikovat“ do jednoho
    • tak vznikne faktorstruktura podle kongruence $=^\mathcal A$
  • definice
    • je-li $T$ teorie v jazyce $L$ s rovností, potom označme jako $T^*$ rozšíření teorie $T$ o generální uzávěry axiomů rovnosti pro jazyk $L$
    • tablo důkaz z teorie $T$ je tablo důkaz z $T^*$, podobně pro tablo zamítnutí (a obecně jakékoliv tablo)
  • pozorování: jestliže $\mathcal A\models T^$, potom platí i $\mathcal A/_{=^\mathcal A}\models T^$
• Věta o kompaktnosti a její aplikace
  • věta: teorie má model, právě když každá její konečná část má model
  • důkaz
    • $\implies:$ model teorie je zřejmě modelem každé její části
    • $\impliedby$ obměnou, chceme: pokud $T$ nemá model, existuje její konečná část, která nemá model
      • pokud $T$ nemá model, je sporná, tedy $T\vdash\bot$
      • vezměme nějaký konečný tablo důkaz $\bot$ z $T$
        • podle věty o konečnosti sporu
      • k jeho konstrukci stačí konečně mnoho axiomů $T$
      • ty tvoří konečnou podteorii $T'\subseteq T$, která nemá model
  • aplikace
    • popíšeme požadovanou vlastnost nekonečného objektu pomocí (nekonečné) výrokové teorie
    • z konečné části teorie sestrojíme konečný podobjekt mající danou vlastnost
  • příklad
    • spočetně nekonečný graf je bipartitní $\iff$ každý jeho konečný podgraf je bipartitní
      • $T=\set{p_u\to\neg p_v\mid\set{u,v}\in E(G)}$
• Věta o korektnosti rezoluce ve výrokové logice
  • věta: je-li formule $S$ rezolucí zamítnutelná, potom je $S$ nesplnitelná
  • důkaz
    • nechť $S\vdash_R\square$ a vezměme nějaký rezoluční důkaz $C_0,C_1,\dots,C_n=\square$
    • předpokládejme pro spor, že $S$ je splnitelná
    • tedy $\mathcal V\models S$ pro nějaké ohodnocení $\mathcal V$
    • indukcí podle $i$ dokážeme, že $\mathcal V\models C_i$
    • pro $i=0$ to platí, neboť $C_0\in S$
    • pro $i\gt 0$ máme dva případy
      • $C_i\in S$, potom $\mathcal V\models C_i$ plyne z předpokladu, že $\mathcal V\models S$
      • $C_i$ je rezolventou nějakých dvou předchozích klauzulí, pro obě z nich z indukčního předpokladu platí, že ohodnocení $\mathcal V$ je splňuje, takže $\mathcal V\models C_i$ plyne z korektnosti rezolučního pravidla
    • indukcí dojdeme k tomu, že $\mathcal V\models\square$, což je spor
• Věta o korektnosti rezoluce v predikátové logice
  • korektnost rezolučního pravidla
    • v klauzuli $C_1$ jsou mj. výrazy $A_1,\dots,A_n$
    • v klauzuli $C_2$ jsou mj. výrazy $\neg B_1,\dots,\neg B_m$
    • množina výrazů $S=\set{A_1,\dots,A_n,B_1,\dots,B_m}$ má nejobecnější unifikaci $\sigma$ takovou, že $S\sigma=\set{A_1\sigma}$
    • $C_1,C_2$ jsou otevřené formule platné v $\mathcal A$, takže platí i jejich instance po substituci, proto $\mathcal A\vDash C_1\sigma$ a $\mathcal A\vDash C_2\sigma$
    • pokud $\mathcal A\vDash A_1\sigma[e]$, potom $\mathcal A\nvDash\neg A_1\sigma [e]$ a musí být $\mathcal A\vDash C_2'\sigma[e]$
      • kde $C'_2$ je část formule bez negací $B_i$
    • tedy $\mathcal A\vDash C[e]$
    • podobně to funguje i naopak – pokud $\mathcal A\nvDash A_1\sigma[e]$
  • věta: pokud je CNF formule $S$ rezolucí zamítnutelná, potom je nesplnitelná
  • důkaz
    • víme, že $S\vdash_R\square$, vezměme tedy nějaký rezoluční důkaz $\square$ z $S$
    • kdyby existoval model $\mathcal A\models S$, díky korektnosti rezolučního pravidla bychom mohli dokázat indukcí podle délky důkazu, že i $\mathcal A\models\square$, což ale není možné
• Souvislost stromu dosazení a splnitelnosti CNF formule
  • lemma: $S$ je splnitelná, právě když je splnitelná $S^\ell$ nebo $S^{\overline{\ell}}$
  • důkaz lemmatu
    • $\implies$
      • mějme ohodnocení $\mathcal V\models S$
      • to nemůže obsahovat $\ell$ i $\overline\ell$ (musí být konzistentní)
      • BÚNO $\overline\ell\notin\mathcal V$
      • vezmeme klauzuli v $S^\ell$, ta je ve tvaru $C\setminus\set{\overline\ell}$ pro klauzuli $C\in S$ neobsahující $\ell$
      • víme, že $\mathcal V\models C$
      • $\mathcal V$ neobsahuje $\overline\ell$, takže $\mathcal V$ splnilo nějaký jiný literál $C$, takže platí i $\mathcal V\models C\setminus\set{\overline\ell}$
    • $\impliedby$
      • BÚNO existuje $\mathcal V\models S^\ell$
      • $\overline\ell$ se nevyskytuje v $S^\ell$, takže platí $\mathcal V\setminus\set{\overline\ell}\models S^\ell$
      • ohodnocení $\mathcal V'=(\mathcal V\setminus\set{\overline\ell})\cup\set{\ell}$ splňuje každou $C\in S$
        • pokud $\ell\in C$, klauzule je splněna díky $\ell$ v $\mathcal V'$
        • pokud $\ell\notin C$, pak $\mathcal V\setminus\set{\overline\ell}\models C\setminus\set{\overline\ell}\in S^\ell$
  • tvrzení: formule $S$ (nad spočetným jazykem) je nesplnitelná, právě když každá větev stromu dosazení obsahuje prázdnou klauzuli $\square$
  • důkaz tvrzení
    • pro konečnou formuli lze dokázat indukcí podle počtu proměnných pomocí lemmatu
    • pro nekonečnou formuli
      • je-li $S$ nekonečná a splnitelná, potom má splňující ohodnocení
      • to se shoduje s odpovídající nekonečnou větví ve stromu dosazení
      • je-li $S$ nekonečná a nesplnitelná, potom podle věty o kompaktnosti existuje nesplnitelná konečná část $S'\subseteq S$
      • po dosazení pro všechny proměnné bude v každé větvi $\square$ (po konečně mnoha krocích)
• Nestandardní model přirozených čísel
  • nechť $\underline{\mathbb N}=\braket{\mathbb N,S,+,\cdot,0,\leq}$ je standardní model přirozených čísel
  • označme $\text{Th}(\underline{\mathbb N})$ množinu všech sentencí pravdivých v $\underline{\mathbb N}$ (tzv. teorii struktury $\underline{\mathbb N}$)
  • pro $n\in\mathbb N$ definujme $n$-tý numerál jako term $\underline n=S(S(\dots S(0)\dots))$, kde $S$ je aplikováno $n$-krát
  • vezměme nový konstantní symbol $c$ a vyjádřeme, že je ostře větší než každý $n$-tý numerál: $T=\text{Th}(\underline{\mathbb N})\cup\set{\underline n\lt c\mid n\in\mathbb N}$
  • každá konečná část $T$ má model
  • podle věty kompaktnosti má i $T$ model, říkáme mu nestandardní model
  • platí v něm tytéž sentence, jako ve standardním modelu, ale zároveň obsahuje prvek $c^\mathcal A$, který je větší než každé $n\in\mathbb N$
• Kompletní jednoduché extenze DeLO*
  • teorie hustého lineárního uspořádání (DeLO*) je extenze teorie uspořádání (reflexivita, antisymetrie, tranzitivita) o axiom linearity (dichotomie) a axiom hustoty (mezi libovolnými dvěma prvky existuje třetí), někdy se přidává axiom netriviality (zakazuje jednoprvkový model)
  • mějme sentenci $\varphi$ vyjadřující existenci minimálního prvku a sentenci $\psi$ vyjadřující existenci maximálního prvku
  • následující čtyři teorie jsou právě všechny kompletní jednoduché extenze teorie DeLO*
    • $DeLO=DeLO^*\cup\set{\neg\varphi,\neg\psi}$
    • $DeLO^+=DeLO^*\cup\set{\neg\varphi,\psi}$
    • $DeLO^-=DeLO^*\cup\set{\varphi,\neg\psi}$
    • $DeLO^\pm=DeLO^*\cup\set{\varphi,\psi}$
  • stačí ukázat, že tyto čtyři teorie jsou kompletní – potom žádná další kompletní jednoduchá extenze DeLO* nemůže existovat
  • jejich kompletnost plyne z toho, že jsou $\omega$-kategorické
• Existence spočetného algebraicky uzavřeného tělesa
  • těleso je algebraicky uzavřené, pokud každý polynom nenulového stupně v něm má kořen
  • nespočetné těleso $\mathbb C$ je algebraicky uzavřené ($\mathbb R,\mathbb Q$ nejsou)
  • algebraickou uzavřenost pro každé $n\gt 0$ vyjádříme sentencí $\psi_n=(\forall x_{n-1})\dots(\forall x_0)(\exists y)(y^n+x_{n-1}\cdot y^{n-1}+\dots+x_1\cdot y+x_0)=0$
    • kde $y^k$ je zkratka za term $\underbrace{y\cdot y\cdot\ldots\cdot y}_{k}$
    • $y$ tady odpovídá hledanému kořenu polynomu (obvykle se označuje jako $x$), naopak $x_i$ odpovídají koeficientům
  • z Löwenheim-Skolemovy věty s rovností vyplývá důsledek, že ke každé nekonečné $L$-struktuře (kde $L$ je spočetný jazyk s rovností) existuje elementárně ekvivalentní spočetně nekonečná struktura
  • tedy existuje spočetně nekonečná struktura $\mathcal A$ elementárně ekvivalentní tělesu $\mathbb C$
  • $\mathbb C$ je těleso a $\forall n\gt 0:\mathbb C\models\psi_n\implies\mathcal A$ je algebraicky uzavřené těleso
• Tělesa charakteristiky 0 nejsou konečně axiomatizovatelná
  • těleso charakteristiky 0 … sečtením prvočíselného počtu jedniček nikdy nedostanu nulu
    • $T$ … teorie těles
    • $T_0$ … teorie axiomatizující třídu těles charakteristiky 0
    • $T_0=T\cup\set{\neg p1=0\mid p \text{ je prvo\v{c}íslo}}$
      • $p1$ … $\underbrace{1+1+\dots+1}_p$
  • tvrzení: třída $K$ těles charakteristiky 0 není konečně axiomatizovatelná
  • důkaz
    • podle věty o konečné axiomatizovatelnosti stačí ukázat, že $\overline K$ (tělesa nenulové charakteristiky a netělesa) není axiomatizovatelná
    • sporem: $\overline K=M(S)$
    • potom $S'=S\cup T_0$ má model, neboť každá konečná část má model
      • pro konečné části $S$ jednoduché
      • pro konečné části $T_0$ vezmeme těleso prvočíselné charakteristiky větší než jakékoliv $p$ z axiomu $T_0$ tvaru $\neg p1=0$
    • nechť $\mathcal A$ je model $S'$
    • potom je i modelem $S$, takže $\mathcal A\in\overline K$
    • zároveň je ale modelem $T_0$, takže $\mathcal A\in K$, což je spor
• Kritérium otevřené axiomatizovatelnosti
  • pozorování: je-li $\mathcal B\subseteq\mathcal A$, potom pro každou otevřenou formuli $\varphi$ a ohodnocení $e:\text{Var}\to B$ platí $\mathcal B\models\varphi[e]\iff\mathcal A\models\varphi[e]$
    • protože prvky z $B$ jsou i v $A$
    • lze dokázat indukcí podle struktury formule
  • tvrzení: je-li $T$ otevřeně axiomatizovatelná, potom je každá podstruktura modelu $T$ také modelem $T$
  • důkaz
    • buď $T'$ otevřená axiomatizace $T$, $\mathcal A$ model $T'$, $\mathcal {B\subseteq A}$
    • pro každou $\varphi\in T'$ platí $\mathcal B\models\varphi$ ($\varphi$ je otevřená, použijeme pozorování)
    • tedy i $\mathcal B\models T'$
  • příklady
    • DeLO není otevřeně axiomatizovatelná – konečná podstruktura nemůže být hustá
    • teorie těles není otevřeně axiomatizovatelná – podstruktura $\mathbb Z$ nemá inverzní prvek k 2 vůči násobení
• Rekurzivně axiomatizovaná teorie je částečně rozhodnutelná, kompletní je rozhodnutelná
  • tvrzení: je-li $T$ rekurzivně axiomatizovaná, potom je částečně rozhodnutelná, je-li navíc kompletní, je rozhodnutelná
  • důkaz
    • rekurzivní axiomatizovanost → částečná rozhodnutelnost
      • algoritmus konstruuje systematické tablo z $T$ pro $\text F\varphi$
      • pokud $T\vDash\varphi$, konstrukce skončí v konečně mnoha krocích
      • jinak konstrukce nemusí skončit
    • rekurzivní axiomatizovanost & kompletnost → rozhodnutelnost
      • z kompletnosti plyne, že buď $T\vdash\varphi$ nebo $T\vdash\neg\varphi$
      • algoritmus současně konstruuje tablo pro $\text F\varphi$ a tablo pro $\text T\varphi$
      • jedna z konstrukcí po konečně mnoha krocích skončí
• Teorie konečné struktury v konečném jazyce s rovností je rozhodnutelná
  • tvrzení: je-li $\mathcal A$ konečná struktura v konečném jazyce s rovností, potom je teorie $\text{Th}(\mathcal A)$ rekurzivně axiomatizovatelná
  • důkaz
    • očíslujme prvku domény jako $A=\set{a_1,\dots,a_n}$
    • $\text{Th}(\mathcal A)$ lze axiomatizovat sentencí, která je tvaru „existuje právě $n$ prvků $a_1,\dots,a_n$ splňujících právě ty základní vztahy o funkčních hodnotách a relacích, které platí v $\mathcal A$“
  • $\text{Th}(\mathcal A)$ (množina všech $L$-sentencí platných v $\mathcal A$) je zjevně kompletní (podle pozorování 9.1.3)
  • rekurzivní axiomatizovanost & kompletnost → rozhodnutelnost
• Gödelovy věty o neúplnosti a jejich důsledky (bez důkazů)
  • První věta o neúplnosti: Pro každou bezespornou rekurzivně axiomatizovanou extenzi $T$ Robinsonovy aritmetiky existuje sentence, která je pravdivá v $\underline{\mathbb N}$, ale není dokazatelná v $T$.
  • důsledek 1.1: je-li $T$ rekurzivně axiomatizovaná extenze Robinsonovy aritmetiky a je-li navíc $\underline{\mathbb N}$ modelem teorie $T$, potom $T$ není kompletní
    • pro sentenci, která není dokazatelná v $T$, nemůže být dokazatelná ani její negace (byl by to spor s její pravdivostí v $\underline{\mathbb N}$)
  • důsledek 1.2: teorie $\text{Th}(\underline{\mathbb N})$ není rekurzivně axiomatizovatelná
    • kdyby byla, nemohla by být kompletní – ale ona kompletní je
  • věta (Rosserův trik): v každé bezesporné rekurzivně axiomatizované extenzi Robinsonovy aritmetiky existuje nezávislá sentence – tedy taková není kompletní
    • v podstatě plyne z důsledku 1.1, jen se zbavuje $\underline{\mathbb N}$
  • Druhá věta o neúplnosti: Pro každou bezespornou rekurzivně axiomatizovanou extenzi $T$ Peanovy aritmetiky platí, že $\mathit{Con_T}$ není dokazatelná v $T$.
  • $\mathit{Con_T}$ … sentence vyjadřující bezespornost (konzistence) teorie $T$
    • $\mathit{Con_T}=\neg(\exists y)\mathit{Prf_{T}}(\underline{0=S(0)},y)$
    • $\mathit{Prf_{T}}(x,y)$ … $y$ je důkaz $x$ v $T$
  • důsledek 2.1: existuje model Peanovy aritmetiky (PA), ve kterém platí sentence $(\exists y)\mathit{Prf_{PA}}(\underline{0=S(0)},y)$
  • důsledek 2.2: existuje bezesporná rekurzivně axiomatizovaná extenze $T$ Peanovy aritmetiky, která dokazuje svou spornost, tj. taková, že $T\vdash\neg \mathit{Con_T}$
  • důsledek 2.3: je-li teorie množin ZFC bezesporná, nemůže být sentence $\mathit{Con_{ZFC}}$ v teorii ZFC dokazatelná

Těžké otázky

• Věta o korektnosti tablo metody ve výrokové logice
  • potřebujeme lemma: shoduje-li se model teorie $T$ s položkou v kořeni tabla z teorie $T$, potom se shoduje s nějakou větví
  • důkaz lemmatu
    • mějme postup vytváření tabla
    • indukcí sestrojíme větev, se kterou se model shoduje
    • díváme se na rozdíl mezi dvěma verzemi tabla
      • pokud nová verze vznikla bez prodloužení naší větve, necháme ji tak
      • pokud nová verze vznikla připojením axiomu z teorie na konec naší větve, prodloužíme o něj naši větev
        • model se s axiomem nutně shoduje
      • pokud nová verze vznikla připojením atomického tabla na konec naší větve…
        • model se nutně shoduje s kořenem atomického tabla
        • model se tedy shoduje i s některou z větví atomického tabla
        • naši větev prodloužíme o tuto větev
  • věta o korektnosti: je-li výrok $\varphi$ tablo dokazatelný z teorie $T$, potom je $\varphi$ pravdivý v $T$, tj. $T\vdash\varphi\implies T\vDash\varphi$
  • důkaz sporem
    • nechť $\varphi$ v $T$ neplatí, tj. existuje protipříklad = model $v$, v němž $\varphi$ neplatí
    • výrok $\varphi$ je dokazatelný z $T$, tedy existuje tablo důkaz (sporné tablo s $\text F\varphi$ v kořeni)
    • model $v$ se shoduje s $\text F\varphi$, tedy podle lemmatu se shoduje s nějakou větví $V$
    • všechny větve jsou sporné, tedy i $V$
      • $V$ obsahuje $\text T\psi$ a $\text F\psi$
    • model $v$ se s těmito položkami shoduje
    • proto $v\vDash\psi$ a $v\nvDash\psi$, což je spor
• Věta o korektnosti tablo metody v predikátové logice
  • lemma: shoduje-li se model $\mathcal A$ teorie $T$ s položkou v kořeni tabla z teorie $T$ (v jazyce $L$), potom lze $\mathcal A$ expandovat do jazyka $L_C$ tak, že se shoduje s některou větví v tablu
  • důkaz
    • podobně jako ve výrokové logice postupně vytváříme větev
    • navíc postupně expandujeme model $\mathcal A$ o konstanty $c^\mathcal A\in C$
  • věta o korektnosti: je-li sentence $\varphi$ tablo dokazatelná z teorie $T$, potom je $\varphi$ pravdivá v $T$, tj. $T\vdash\varphi\implies T\vDash\varphi$
  • důkaz sporem
    • nechť $T\nvDash\varphi$, tj. existuje $\mathcal A\models T$ takový, že $\mathcal A\nvDash\varphi$
    • protože $T\vdash\varphi$, existuje sporné tablo z $T$ s $\text F\varphi$ v kořeni
    • model $\mathcal A$ se shoduje s $\text F\varphi\implies$ podle lemmatu lze $\mathcal A$ expandovat do jazyka $L_C$ tak, že se expanze shoduje s nějakou větví
    • všechny větve jsou ale sporné
• Věta o úplnosti tablo metody ve výrokové logice
  • lemma: kanonický model pro bezespornou dokončenou větev $V$ se shoduje s $V$
    • důkaz se konstruuje indukcí, jejímž základem jsou položky s prvovýroky
  • věta: je-li výrok $\varphi$ pravdivý v teorii $T$, potom je tablo dokazatelný z $T$, tj. $T\vDash\varphi\implies T\vdash\varphi$
  • důkaz sporem
    • kdyby tablo z $T$ s položkou $\text F\varphi$ v kořeni nebylo sporné, existovala by bezesporná (dokončená) větev $V$
    • $V$ obsahuje $\text T\alpha$ pro všechny axiomy $\alpha\in T$
    • uvažme kanonický model $v$ pro větev $V$
    • $v$ se podle lemmatu shoduje se všemi položkami na $V$
    • splňuje tedy všechny axiomy a máme $v\vDash T$
    • $v$ se ale shoduje i s položkou $\text F\varphi$ v kořeni, tedy $v\nvDash\varphi$, tudíž i $T\nvDash\varphi$, což je spor
    • tablo tedy muselo být sporné, tj. být tablo důkazem $\varphi$ z $T$
• Věta o úplnosti tablo metody v predikátové logice
  • lemma: kanonický model pro bezespornou dokončenou větev $V$ se shoduje s $V$
    • důkaz se konstruuje indukcí, jejímž základem jsou položky s atomickými sentencemi
  • věta: je-li sentence $\varphi$ pravdivá v teorii $T$, potom je tablo dokazatelná z $T$, tj. $T\vDash\varphi\implies T\vdash\varphi$
  • důkaz sporem
    • uvažujme dokončené tablo z $T$ s položkou $\text F\varphi$ v kořeni, které není sporné
    • v takovém tablu bude dokončená větev $V$
    • mějme kanonický model $\mathcal A_C$ pro tuto větev, jako $\mathcal A$ označme jeho redukt na jazyk $L$
    • $V$ obsahuje $\text T\alpha$ pro všechny axiomy $\alpha\in T$
    • $\mathcal A_C$ se podle lemmatu shoduje se všemi položkami na $V$
    • splňuje tedy všechny axiomy a máme i $\mathcal A\vDash T$
    • $\mathcal A_C$ se ale shoduje i s položkou $\text F\varphi$ v kořeni, tedy i $\mathcal A\nvDash\varphi$, tudíž $T\nvDash\varphi$ což je spor
    • tablo tedy muselo být sporné, tj. být tablo důkazem $\varphi$ z $T$
• Věta o konečnosti sporu, důsledky o konečnosti a systematičnosti důkazů
  • Königovo lemma: nekonečný, konečně větvící strom má nekonečnou větev
  • věta: je-li $\tau=\bigcup_{i\geq 0}\tau_i$ sporné tablo, potom existuje $n\in\mathbb N$ takové, že $\tau_n$ je sporné konečné tablo
  • důkaz
    • uvažme množinu $S$ všech vrcholů stromu $\tau$, které nad sebou neobsahují spor, tj. dvojici položek $\text T\psi,\text F\psi$
    • kdyby $S$ byla nekonečná, podle Königova lemmatu bychom měli nekonečnou bezespornou větev v $S$
    • tedy bychom měli bezespornou větev v $\tau$, což je ve sporu s tím, že $\tau$ je sporné
    • $S$ je tedy konečná
    • proto existuje $d\in\mathbb N$ takové, že $S$ leží v hloubce nejvýše $d$
    • zvolme $n$ tak, že $\tau_n$ už obsahuje všechny vrcholy $\tau$ z prvních $d+1$ úrovní, každá větev v $\tau_n$ je tedy sporná
  • důsledek: pokud při konstrukci tabla neprodlužujeme sporné větve, potom je sporné tablo konečné
    • důkaz: máme $\tau=\tau_n$, sporné tablo už neměníme
  • důsledek: pokud $T\vdash\varphi$, potom existuje konečný tablo důkaz $\varphi$ z $T$
    • důkaz: při konstrukci $\tau$ ignorujeme kroky, které by prodloužily spornou větev
  • důsledek: pokud $T\vdash\varphi$, potom systematické tablo je konečným tablo důkazem $\varphi$ z $T$
    • důkaz
      • pokud $T\vdash \varphi$, potom $T\models\varphi$ (dle věty o korektnosti) = neexistuje protipříklad
      • kdyby systematické tablo mělo bezespornou větev, existoval by protipříklad
• Věta o úplnosti rezoluce ve výrokové logice
  • věta: je-li $S$ nesplnitelná, je rezolucí zamítnutelná (tj. $S\vdash_R\square$)
  • důkaz
    • předpokládejme, že $S$ je konečná
      • nekonečná $S$ by měla konečnou nesplnitelnou část, přičemž její rezoluční zamítnutí by bylo rezolučním zamítnutím $S$
    • postupujeme indukcí podle počtu proměnných v $S$
    • pro nula proměnných je jediná nesplnitelná formule $S=\set{\square}$
    • jinak vybereme $p\in\text{Var}(S)$
    • podle lemmatu o stromu dosazení jsou $S^p$ i $S^{\overline{p}}$ nesplnitelné
    • mají o jednou proměnnou méně, tedy podle indukčního předpokladu existují rezoluční stromy $T$ a $T'$ s rezolučním zamítnutím
    • ze stromu $T$ pro $S^p\vdash_R\square$ vypěstujeme strom $\widehat T$ pro $S\vdash_R\neg p$
      • na každém listu je klauzule $C\in S^p$
      • pro tuhle klauzuli platí buď $C\in S$, nebo $C\cup\set{\neg p}\in S$
      • v druhém případě přidáme do $C$ a do všech klauzulí nad tímto listem literál $\neg p$
    • podobně vypěstujeme $\widehat{T'}$ pro $S\vdash_R p$ a oba stromy připojíme ke kořeni $\square$
• Věta o úplnosti LI-rezoluce pro výrokové Hornovy formule
  • pozorování: pokud je Hornova formule (která neobsahuje prázdnou klauzuli) nesplnitelná, pak obsahuje fakt i cíl
    • fakt = pozitivní jednotková klauzule
    • cíl = neprázdná klauzule bez pozitivního literálu
    • kdyby neobsahovala fakt, ohodnotíme všechny proměnné 0
    • kdyby neobsahovala cíl, ohodnotíme všechny proměnné 1
  • věta: je-li Hornova formule $T$ splnitelná a $T\cup\set{G}$ je nesplnitelná pro cíl $G$, potom $T\cup\set{G}\vdash_{LI}\square$, a to LI-zamítnutím, které začíná cílem $G$
  • důkaz
    • podobně jako ve větě o úplnosti rezoluce můžeme díky větě o kompaktnosti předpokládat konečnost
    • důkaz provedeme indukcí podle počtu proměnných v $T$
    • z pozorování plyne, že $T$ obsahuje fakt $\set p$ pro nějakou proměnnou $p$
    • $T\cup\set G$ je nesplnitelná $\implies$ podle lemmatu je nesplnitelná také $(T\cup\set G)^p=T^p\cup\set{G^p}$, kde $G^p=G\setminus\set{\neg p}$
    • základ indukce: pokud $G^p=\square$, potom $G=\set{\neg p}$
      • víme, že $\set p\in T$, takže máme jednokrokové LI-zamítnutí
    • jinak je $T^p$ splnitelná (stejným ohodnocením jako $T$, protože to musí obsahovat $p$ kvůli faktu $\set p$) a má méně proměnných než $T$
    • podle IP existuje LI-odvození $\square$ z $T^p\cup\set{G^p}$ začínající $G^p$
    • LI-zamítnutí $T\cup\set{G}$ začínající $G$ zkonstruujeme obdobně jako ve větě o úplnosti rezoluce
      • nejprve přidáme $\neg p$ do všech listů, které nejsou v $T\cup\set G$, a do všech vrcholů nad nimi
      • tím dostaneme $T\cup\set G\vdash_{LI}\neg p$
      • na závěr přidáme boční klauzuli $\set p$ a odvodíme $\square$
• Věta o úplnosti rezoluce v predikátové logice (Lifting lemma stačí vyslovit)
  • instance $\varphi(x_1/t_1,\dots,x_n/t_n)$ otevřené formule $\varphi$ je základní, jsou-li všechny termy $t_1,\dots,t_n$ konstantní
  • Lifting lemma (ukazuje, že rezoluční důkaz na úrovni výrokové logiky je možné zvednout na úroveň predikátové logiky)
    • mějme klauzule $C_1,C_2$ s disjunktními množinami proměnných
    • jsou-li $C_1^$ a $C_2^$ základní instance klauzulí $C_1$ a $C_2$ a je-li $C^$ rezolventou $C_1^$ a $C_2^$, potom existuje rezolventa $C$ klauzulí $C_1,C_2$ taková, že $C^$ je základní instancí $C$
  • důsledek Lifting lemmatu
    • mějme CNF formuli $S$ a množinu všech jejích základních instancí $S^*$
    • pokud $S^\vdash_R C^$ pro nějakou základní klauzuli $C^$, potom existuje klauzule $C$ a základní substituce $\sigma$ taková, že $C^=C\sigma$ a $S\vdash_R C$
  • věta: je-li CNF formule S nesplnitelná, potom je zamítnutelná rezolucí
  • důkaz
    • označme $S^*$ množinu všech základních instancí klauzulí z $S$
    • $S$ je nesplnitelná → díky Herbrandově větě je nesplnitelná i $S^*$
    • z věty o úplnosti výrokové rezoluce víme, že $S^*\vdash_R\square$
    • z důsledku Lifting lemmatu dostáváme $C$ a $\sigma$ takové, že $C\sigma=\square$ a $S\vdash_R C$
    • ale protože prázdná klauzule $\square$ je instancí $C$, musí být $C=\square$
    • tím jsme našli rezoluční zamítnutí $S\vdash_R\square$
• Skolemova věta
  • lemma: pro $L$-sentenci $\varphi$ a její Skolemovu variantu $\varphi'$ platí, že $L$-redukt každého modelu $\varphi'$ je modelem $\varphi$ a že každý model $\varphi$ lze expandovat na model $\varphi'$
    • model $\varphi'$ v univerzu obsahuje prvek, který splňuje existenční kvantifikátor (je to ten prvek, který vrací funkce $f$, kterou jsme existenční kvantifikátor nahradili)
    • expanzi modelu $\varphi$ na model $\varphi'$ provedeme tak, že funkci $f$ nadefinujeme tak, aby vracela prvky, které splňují existenční kvantifikátor
  • věta: každá teorie má otevřenou konzervativní extenzi
  • důkaz
    • mějme $L$-teorii $T$
    • každý axiom nahradíme jeho generálním uzávěrem a převedeme do PNF, tím získáme ekvivalentní teorii $T'$
    • každý axiom teorie $T'$ nahradíme jeho Skolemovou variantou, tím získáme teorii $T''$ v rozšířeném jazyce $L'$
    • z lemmatu plyne, že $L$-redukt každého modelu $T''$ je modelem $T'$, tedy $T''$ je extenzí $T'$, a že každý model $T'$ lze expandovat do jazyka $L'$ na model $T''$, tedy jde o konzervativní extenzi
    • $T''$ je axiomatizována univerzálními sentencemi, tedy odstraněním kvantifikátorových prefixů dostaneme otevřenou teorii $T'''$, která je ekvivalentní s $T''$, a tedy je také konzervativní extenzí $T$
  • důsledek: ke každé teorii můžeme pomocí skolemizace najít ekvisplnitelnou otevřenou teorii
    • tu pak můžeme převést do CNF
• Herbrandova věta
  • definice (Herbrandův model)
    • mějme jazyk $L=\braket{\mathcal{R,F}}$ s alespoň jedním konstantním symbolem
    • $L$-struktura $\mathcal A=\braket{A,\mathcal{R^A,F^A}}$ je Herbrandův model, jestliže…
      • $A$ je množina všech konstantních $L$-termů (tzv. Herbrandovo univerzum)
      • pro každý $n$-ární funkční symbol $f\in\mathcal F$ a konstantní termy $''t_1'',\dots,{''t_n''}\in A$ platí $f^\mathcal A(''t_1'',\dots,{''t_n''})={''f(t_1,\dots,t_n)''}$
      • speciálně, pro každý konstantní symbol $c\in\mathcal F$ je $c^\mathcal A={''c''}$
    • na interpretace relačních symbolů neklademe žádné podmínky
  • Herbrandova věta
    • mějme otevřenou teorii $T$ v jazyce $L$ bez rovnosti a s alespoň jedním konstantním symbolem
    • potom buď má $T$ Herbrandův model, nebo existuje konečně mnoho základních instancí axiomů $T$, jejichž konjunkce je nesplnitelná
  • důkaz
    • označme jako $T_\text{ground}$ množinu všech základních instancí axiomů teorie $T$
    • zkonstruujeme tablo (takové, kde neprodlužujeme sporné větve – třeba to systematické) z teorie $T_\text{ground}$ s položkou $\text F\bot$ v kořeni, ale z jazyka $L$ (tedy bez rozšíření o pomocné konstantní symboly na jazyk $L_C$, nejsou totiž potřeba, protože $T$ je otevřená)
    • pokud tablo obsahuje bezespornou větev, potom je kanonický model pro tuto větev (opět bez přidání pomocných konstantních symbolů) Herbrandovým modelem $T$
    • v opačném případě máme tablo důkaz sporu, tedy $T_\text{ground}$ i $T$ jsou nesplnitelné
    • tablo důkaz je konečný, takže existuje konečně mnoho základních instancí axiomů $T$, jejichž konjunkce je nesplnitelná
• Löwenheim-Skolemova věta včetně varianty s rovností, jejich důsledky
  • věta: je-li $L$ spočetný jazyk bez rovnosti, potom každá bezesporná $L$-teorie má spočetně nekonečný model
  • důkaz
    • vezměme nějaké dokončené tablo z teorie $T$ s položkou $\text F\bot$ v kořeni
    • $T$ je bezesporná → není v ní dokazatelný spor → tablo obsahuje bezespornou větev
    • hledaný spočetně nekonečný model je $L$-redukt kanonického modelu pro tuto větev
  • důsledek: je-li $L$ spočetný jazyk bez rovnosti, potom ke každé $L$-struktuře existuje elementárně ekvivalentní spočetně nekonečná struktura
    • mějme $L$-strukturu $\mathcal A$
    • teorie $\text{Th}(\mathcal A)$ je bezesporná (má model $\mathcal A$)
    • tedy dle Löwenheim-Skolemovy věty má spočetně nekonečný model $\mathcal B\models\text{Th}(\mathcal A)$
    • to znamená, že $\mathcal B\equiv\mathcal A$
  • věta s rovností: je-li $L$ spočetný jazyk s rovností, potom každá bezesporná $L$-teorie má spočetný model (tj. konečný nebo spočetně nekonečný)
    • spočetně nekonečný model najdeme stejným způsobem jako v případě varianty bez rovnosti, pak ho faktorizujeme podle kongruence $=^\mathcal A$
  • důsledek: je-li $L$ spočetný jazyk s rovností, potom ke každé nekonečné $L$-struktuře existuje elementárně ekvivalentní spočetně nekonečná struktura
    • opět najdeme spočetně nekonečnou $\mathcal B\equiv\mathcal A$
    • v $\mathcal A$ neplatí žádná sentence vyjadřující „existuje nejvýše $n$ prvků“, takže neplatí ani v $\mathcal B$, proto $\mathcal B$ nemůže být konečná struktura
  • důsledek: existuje spočetné algebraicky uzavřené těleso
• Vztah izomorfismu a elementární ekvivalence
  • tvrzení: bijekce $h:A\to B$ je izomorfismus $\mathcal A$ a $\mathcal B$, právě když…
    • pro každý $L$-term $t$ a ohodnocení proměnných $e:\text{Var}\to A$ platí $h(t^\mathcal A[e])=t^\mathcal B[e\circ h]$
    • pro každou $L$-formuli $\varphi$ a ohodnocení proměnných $e:\text{Var}\to A$ platí $A\models\varphi[e]$ právě když $\mathcal B\models\varphi[e\circ h]$
  • důkaz
    • je-li $h$ izomorfismus, vlastnosti dokážeme indukcí podle struktury termu/formule
    • je-li $h$ bijekce splňující vlastnosti, dosazením $f$ za $t$ a $R$ za $\varphi$ dostáváme vlastnosti z definice izomorfismu
  • důsledek: $\mathcal {A\simeq B}\implies\mathcal {A\equiv B}$
  • obrácená implikace obecně neplatí, protože uspořádané množiny racionálních a reálných čísel jsou elementárně ekvivalentní, ale neexistuje mezi nimi bijekce, tedy nejsou izomorfní (jedna je spočetná, druhá nespočetná)
  • tvrzení: je-li $L$ jazyk s rovností a $\mathcal{A,B}$ konečné $L$-struktury, potom platí $\mathcal{A\simeq B\iff A\equiv B}$
  • důkaz $\implies$ výše
  • důkaz $\impliedby$
    • předpokládejme, že $\mathcal {A,B}$ jsou elementárně ekvivalentní (ukážeme, že jsou izomorfní)
    • $L$ je s rovností, takže můžeme vyjádřit sentencí, že „existuje právě $n$ prvků“
    • proto $|A|=|B|$
    • expanzi $\mathcal A$ o jména prvků z $A$ označíme jako $\mathcal A'$, pro každý prvek v podstatě přidáme konstantu
    • ukážeme, že lze $\mathcal B$ expandovat na $L'$-strukturu $\mathcal B'$ tak, že $\mathcal A'\equiv\mathcal B'$
    • to se (asi) dělá tak, že konkrétní prvek $a\in A$ zajišťuje platnost určitých sentencí – tyto sentence jakýmsi způsobem definují zobrazení prvku $a$ do $B$
• $\omega$-kategorické kritérium kompletnosti
  • věta
    • mějme $\omega$-kategorickou teorii $T$ ve spočetném jazyce $L$
    • pokud
      • $L$ je bez rovnosti
      • nebo $L$ je s rovností a $T$ nemá konečné modely
    • potom je teorie $T$ kompletní
  • důkaz
    • bez rovnosti
      • použijeme důsledky Löwenheim-Skolemovy věty – ke každé $L$-struktuře existuje elementárně ekvivalentní spočetně nekonečná struktura
      • z $\omega$-kategoricity vyplývá, že spočetně nekonečný model dané teorie je právě jeden (až na izomorfismus)
    • důsledek Löwenheim-Skolemovy pro jazyk s rovností by umožňoval konečné modely, ale ty jsme zakázali
    • všechny modely $T$ jsou tedy elementárně ekvivalentní právě jednomu spočetně nekonečnému modelu, což znamená, že $T$ je kompletní
• Neaxiomatizovatelnost konečných modelů
  • věta
    • pokud má teorie libovolně velké konečné modely, potom má i nekonečný model
    • v tom případě není třída všech jejích konečných modelů axiomatizovatelná (tohle je zjevný důsledek, ten nedokazujeme)
  • důkaz
    • pro jazyk bez rovnosti stačí vzít kanonický model pro některou bezespornou větev v tablu z $T$ pro položku $\text F\bot$
      • tenhle trik se používá i v jiných důkazech
      • $T$ je bezesporná, neboť má „libovolně velké konečné modely“, tedy tablo není sporné
      • kanonický model bude nekonečný, protože pomocných konstantních symbolů jsme přidali spočetně nekonečno
    • pro jazyk s rovností mějme extenzi $T'$ teorie $T$ do jazyka rozšířeného o spočetně mnoho konstantních symbolů $c_i$
    • $T'=T\cup\set{\neg c_i=c_j\mid i\neq j\in \mathbb N}$
    • každá konečná část teorie $T'$ má zjevně model → dle věty o kompaktnosti má $T'$ model, ten je nutně nekonečný
    • jeho redukt na původní jazyk je nekonečným modelem $T$
• Věta o konečné axiomatizovatelnosti
  • věta: $K\subseteq M_L$ je konečně axiomatizovatelná, právě když $K$ i $\overline K$ jsou axiomatizovatelné
  • důkaz $\implies$
    • pokud $K$ axiomatizují sentence $\varphi_1,\dots,\varphi_n$, pak $\overline K$ axiomatizuje $\neg(\varphi_1\land\dots\land\varphi_n)$
  • důkaz $\impliedby$
    • nechť $T$ a $S$ jsou teorie takové, že $M(T)=K$ a $M(S)=\overline K$
    • uvažme teorii $T\cup S$, ta je sporná, neboť $M(T\cup S)=M(T)\cap M(S)=K\cap \overline K=\emptyset$
    • podle věty o kompaktnosti existují konečné podteorie $T'\subseteq T$ a $S'\subseteq S$ takové, že $\emptyset=M(T'\cup S')=M(T')\cap M(S')$
    • platí $M(T)\subseteq M(T')\subseteq\overline{M(S')}\subseteq\overline{M(S)}=M(T)$
    • tedy $M(T)=M(T')$, tedy $T'$ je hledanou konečnou axiomatizací $K$
• Rekurzivně axiomatizovaná teorie s rekurzivně spočetnou kompletací je rozhodnutelná
  • tvrzení: pokud je teorie $T$ rekurzivně axiomatizovaná a má rekurzivně spočetnou kompletaci, potom je $T$ rozhodnutelná
  • důkaz
    • pro danou sentenci $\varphi$ buď $T\vdash\varphi$, nebo existuje protipříklad $\mathcal A\nvDash\varphi$, tedy existuje kompletní jednoduchá extenze $T_i$ teorie $T$ taková, že $T_i\nvdash\varphi$
    • z kompletnosti plyne, že $T_i\vdash\neg\varphi$
    • náš algoritmus bude paralelně konstruovat tablo důkaz $\varphi$ z $T$ a (postupně) tablo důkazy $\neg\varphi$ ze všech kompletních jednoduchých extenzí $T_1,T_2,\dots$ teorie $T$
      • pomocí dovetailingu
    • víme, že alespoň jedno z paralelně konstruovaných tabel je sporné a můžeme předpokládat, že je i konečné (když neprodlužujeme sporné větve), takže ho algoritmus po konečně mnoha krocích zkonstruuje
• Nerozhodnutelnost predikátové logiky
  • mějme formuli $\varphi$ ve tvaru $(\exists x_1)\dots(\exists x_n) ;p(x_1,\dots,x_n)=q(x_1,\dots,x_n)$
    • kde $p$ a $q$ jsou polynomy s přirozenými koeficienty
  • věta (bez důkazu): problém existence celočíselného řešení dané diofantické rovnice s celočíselnými koeficienty je (algoritmicky) nerozhodnutelný
  • důsledek: neexistuje algoritmus, který by pro danou dvojici polynomů s přirozenými koeficienty rozhodl, zda mají přirozené řešení, tj. zda platí $\underline{\mathbb N}\vDash\varphi$
  • důkaz důsledku
    • každé celé číslo lze vyjádřit jako rozdíl dvojice přirozených čísel
    • každé přirozené číslo lze vyjádřit jako součet čtyř čtverců
    • každou diofantickou rovnici lze tedy transformovat na rovnici z důsledku a naopak
  • věta: neexistuje algoritmus, který by pro danou vstupní formuli $\varphi$ rozhodl, zda je logicky platná (tedy zda je tautologie)
  • důkaz
    • dle tvrzení 10.2.3 (bez důkazu) platí $\underline{\mathbb N}\vDash\varphi\iff Q\vdash\varphi$
      • $Q$ … Robinsonova aritmetika
      • tvrzení se dá použít, protože $\varphi$ je existenční formule a hledáme přirozená řešení
    • konjunkci (generálních uzávěrů) všech axiomů $Q$ označme jako $\psi_Q$
    • zřejmě $Q\vdash\varphi\iff\psi_Q\vdash\varphi\iff\vdash\psi_Q\to\varphi\iff\vDash\psi_Q\to\varphi$
      • poslední ekvivalence dle věty o úplnosti
    • tedy $\underline{\mathbb N}\vDash\varphi\iff\vDash\psi_Q\to\varphi$
    • pokud by existoval algoritmus rozhodující logickou platnost, bylo by to ve sporu s důsledkem výše