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á