Zkouška: kartičky | vyrokova-predikatova-logika

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í

Pojmy

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ý)

Pojmy

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)$

Pojmy

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)

Pojmy

Extenze teorie (jednoduchá, konzervativní), odpovídající sémantická kritéria

extenze teorie $T$ $T$ je libovolná teorie $T'$ $T^{'}$ v jazyce $\mathbb P'\supseteq\mathbb P$ $P^{'} \supseteq P$ splňující $\text{Csq}_{\mathbb P}(T)\subseteq\text{Csq}_{\mathbb P'}(T')$ $Csq_{P} (T) \subseteq Csq_{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$

Pojmy

Tablo z teorie, tablo důkaz

konečné tablo z teorie $T$ $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$ $T$ je sporné tablo z teorie $T$ $T$ s položkou $\text F\varphi$ $F φ$ 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

Pojmy

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)

Pojmy

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$ $A$ podle $\sim$ $\sim$ je struktura $A/_\sim$ $A /_{\sim}$ v témž jazyce, jejíž univerzum $A/_\sim$ $A /_{\sim}$ je množina všech rozkladových tříd $A$ $A$ podle $\sim$ $\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$ $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$

Pojmy

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$ $e : Var \to A$
- kde $\text{Var}$ je množina všech proměnných jazyka a $A$ je doména

Pojmy

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

Pojmy

Rezoluční důkaz a zamítnutí, rezoluční strom

rezoluční důkaz (odvození) klauzule $C$ $C$ z formule $S$ $S$ je konečná posloupnost klauzulí $C_0,C_1,\dots,C_n=C$ $C_{0}, C_{1}, \dots, C_{n} = C$ taková, že
- pro každé $i$ $i$ je buď $C_i\in S$ $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

Pojmy

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$ $S$
- LI-rezoluce není úplná pro obecné formule (ne každá nesplnitelná formule má LI-zamítnutí)
- LI-rezoluce je úplná pro Hornovy formule

Pojmy

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}}$ $⟨ R, F ⟩$ je trojice $\mathcal A=\braket{A,\mathcal{R^A,F^A}}$ $A = ⟨ A, 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}$ $F^{A}$ je množina interpretací jednotlivých funkčních symbolů (kde intepretace $n$ $n$ -árního funkčního symbolu odpovídá funkci přiřazující $n$ $n$ -tici prvků z $A$ $A$ jeden prvek z $A$ $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$

Pojmy

Atomická formule, formule, sentence, otevřené formule

termy jazyka $L$ $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$ $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

Pojmy

Instance formule, substituovatelnost, varianta formule

term $t$ $t$ je substituovatelný za proměnnou $x$ $x$ ve formuli $\varphi$ $φ$ , pokud po simultánním nahrazení všech volných výskytů $x$ $x$ ve $\varphi$ $φ$ za $t$ $t$ nevznikne ve $\varphi$ $φ$ žádný vázaný výskyt proměnné z $t$ $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)

Pojmy

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$

Pojmy

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}$ $A, B$ (v témž jazyce) jsou elementárně ekvivalentní, pokud v nich platí tytéž sentence (značíme $\mathcal A\equiv \mathcal B$ $A \equiv B$ )
- zjevně $\mathcal A\equiv \mathcal B\iff\text{Th}(\mathcal A)=\text{Th}(\mathcal B)$

Pojmy

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$ $A$ generovaná množinou $X$ $X$ se značí $\mathcal A\langle X\rangle$ $A ⟨ X ⟩$ , její univerzum je nejmenší podmnožina $A$ $A$ , která obsahuje množinu $X$ $X$ a je uzavřená na všechny funkce struktury $\mathcal A$ $A$ (tedy rovněž obsahuje všechny konstanty), tuto podmnožinu označme jako $B$ $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í)

Pojmy

Definovatelnost ve struktuře

množina definovaná formulí = množina uspořádaných $n$ $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$ $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$

Pojmy

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$ $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$

Pojmy

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)$ $(\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

Pojmy

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$ a $\mathcal B$ $B$ je bijekce $h:A\to B$ $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

Pojmy

Axiomatizovatelnost, konečná axiomatizovatelnost, otevřená axiomatizovatelnost

mějme třídu struktur $K\subseteq M_L$ v jazyce $L$
říkáme, že $K$ $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$ $L$ -teorii $T'$ $T^{'}$ říkáme, že je konečně/otevřeně axiomatizovatelná, pokud to platí o třídě modelů $K=M_L(T')$ $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

Pojmy

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

Pojmy

Rozhodnutelná a částečně rozhodnutelná teorie

o teorii $T$ $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}$ $φ_{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}$ $φ_{CNF}$ je duální k výroku $\varphi'_\text{DNF}$ $φ_{DNF}^{'}$ sestrojenému pro doplněk $M'=\overline M$ $M^{'} = \overline{M}$
  - nebo můžeme dokázat přímo – každá klauzule zakazuje právě jeden nemodel

Lehké otázky

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$ $G_{φ}^{*}$
  - 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í

Lehké otázky

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$ $ℓ = 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í

Lehké otázky

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$ $\overline{ℓ}$ 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

Lehké otázky

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]$

Lehké otázky

Vlastnosti extenze o definice

je-li $T'$ $T^{'}$ extenze teorie $T$ $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'$ $T^{'}$ je extenzí $T$ $T$ , právě když redukt každého modelu $T'$ $T^{'}$ na $L$ $L$ je modelem $T$ $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'$ $T^{'}$ extenzí $T$ $T$ a každý model $T$ $T$ lze expandovat do $L'$ $L^{'}$ na nějaký model $T'$ $T^{'}$ , potom je $T'$ $T^{'}$ konzervativní extenzí $T$ $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$ $T^{'} ⊨ φ^{'} \leftrightarrow φ$
  - pro relační symbol $R$ $R$
    - v definici máme ekvivalenci $R\leftrightarrow\psi$
    - $\varphi$ $φ$ vznikne tak, že nahradíme atomické podformule s novým symbolem $R$ $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$ $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$

Lehké otázky

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$ $\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)]$ $⟺ A ⊨ φ [(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)]$ $⟺ A ⊨ φ [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$

Lehké otázky

Tablo metoda v jazyce s rovností

chceme, aby v nějakém modelu $\mathcal A$ $A$ teorie $T$ $T$ v jazyce s rovností byla relace $=^\mathcal A$ $=^{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$ $=^{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^*$

Lehké otázky

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$ $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$ $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)}$

Lehké otázky

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$ $i > 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

Lehké otázky

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]$ $A ⊨ A_{1} σ [e]$ , potom $\mathcal A\nvDash\neg A_1\sigma [e]$ $A ⊭ \neg A_{1} σ [e]$ a musí být $\mathcal A\vDash C_2'\sigma[e]$ $A ⊨ C_{2}^{'} σ [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é

Lehké otázky

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}$ $V^{'} = (V ∖ {\overline{ℓ}}) \cup {ℓ}$ splňuje každou $C\in S$ $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)

Lehké otázky

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$

Lehké otázky

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é

Lehké otázky

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$ $n > 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$ $ψ_{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

Lehké otázky

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}}$ $T_{0} = T \cup {\neg p 1 = 0 ∣ p je prvo \overset{c}{ˇ} \overset{ı}{ˊ} 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$ $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

Lehké otázky

Kritérium otevřené axiomatizovatelnosti

pozorování: je-li $\mathcal B\subseteq\mathcal A$ $B \subseteq A$ , potom pro každou otevřenou formuli $\varphi$ $φ$ a ohodnocení $e:\text{Var}\to B$ $e : Var \to B$ platí $\mathcal B\models\varphi[e]\iff\mathcal A\models\varphi[e]$ $B ⊨ φ [e] ⟺ A ⊨ φ [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í

Lehké otázky

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čí

Lehké otázky

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

Lehké otázky

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$ $T$ rekurzivně axiomatizovaná extenze Robinsonovy aritmetiky a je-li navíc $\underline{\mathbb N}$ $\underline{N}$ modelem teorie $T$ $T$ , potom $T$ $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})$ $Th (\underline{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}$ $Co n_{T}$ … sentence vyjadřující bezespornost (konzistence) teorie $T$ $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$
  - $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

Těžké otázky

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é

Těžké otázky

Věta o úplnosti tablo metody ve výrokové logice

lemma: kanonický model pro bezespornou dokončenou větev $V$ $V$ se shoduje s $V$ $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$

Těžké otázky

Věta o úplnosti tablo metody v predikátové logice

lemma: kanonický model pro bezespornou dokončenou větev $V$ $V$ se shoduje s $V$ $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$

Těžké otázky

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$ $T ⊢ φ$ , potom existuje konečný tablo důkaz $\varphi$ $φ$ z $T$ $T$
- důkaz: při konstrukci $\tau$ ignorujeme kroky, které by prodloužily spornou větev
důsledek: pokud $T\vdash\varphi$ $T ⊢ φ$ , potom systematické tablo je konečným tablo důkazem $\varphi$ $φ$ z $T$ $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

Těžké otázky

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$ $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$ $T$ pro $S^p\vdash_R\square$ $S^{p} ⊢_{R} □$ vypěstujeme strom $\widehat T$ $T$ pro $S\vdash_R\neg p$ $S ⊢_{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$

Těžké otázky

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$ $G^{p} = □$ , potom $G=\set{\neg p}$ $G = {\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}$ $T \cup {G}$ začínající $G$ $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$

Těžké otázky

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$

Těžké otázky

Skolemova věta

lemma: pro $L$ $L$ -sentenci $\varphi$ $φ$ a její Skolemovu variantu $\varphi'$ $φ^{'}$ platí, že $L$ $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

Těžké otázky

Herbrandova věta

definice (Herbrandův model)
- mějme jazyk $L=\braket{\mathcal{R,F}}$ s alespoň jedním konstantním symbolem
- $L$ $L$ -struktura $\mathcal A=\braket{A,\mathcal{R^A,F^A}}$ $A = ⟨ A, 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á

Těžké otázky

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$ $L$ spočetný jazyk bez rovnosti, potom ke každé $L$ $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$ $L$ spočetný jazyk s rovností, potom každá bezesporná $L$ $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$ $L$ spočetný jazyk s rovností, potom ke každé nekonečné $L$ $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

Těžké otázky

Vztah izomorfismu a elementární ekvivalence

tvrzení: bijekce $h:A\to B$ $h : A \to B$ je izomorfismus $\mathcal A$ $A$ a $\mathcal B$ $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$

Těžké otázky

$\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í

Těžké otázky

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$ $T$ pro položku $\text F\bot$ $F ⊥$
  - 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$

Těžké otázky

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$

Těžké otázky

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$ $T$ a (postupně) tablo důkazy $\neg\varphi$ $\neg φ$ ze všech kompletních jednoduchých extenzí $T_1,T_2,\dots$ $T_{1}, T_{2}, \dots$ teorie $T$ $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

Těžké otázky

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)$ $(\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$ $\underline{N} ⊨ φ ⟺ Q ⊢ φ$
  - $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$ $Q ⊢ φ ⟺ ψ_{Q} ⊢ φ ⟺ ⊢ ψ_{Q} \to φ ⟺ ⊨ ψ_{Q} \to φ$
  - 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