Výroková a predikátová logika (WIP)

[Edit]

Tento článek je stále nedokončený může obsahovat obsahuje spoustu chyb. Pokud naleznete nějakou chybu, můžete jí opravit pomocí tlačítka edit.

Značení - výroková logika

Výroková logika

Definition

Booleovská funkce

Booleovská funkce je nn-ární funkce na 2={0,1}2=\{0,1\}, tj. f:{0,1}n{0,1}f:\{0,1\}^{n} \rightarrow\{0,1\}.

Definition

Ohodnocení

Ohodnocení prvovýroků je funkce v:P{0,1}v: \P \rightarrow\{0,1\}, tj. vP2v \in{ }^{\P} 2.

Definition

Sémantické pojmy

Výrok φnadP\varphi \operatorname{nad} \P je

Výroky φ\varphi a ψ\psi jsou logicky ekvivalentní, pokud vˉ(φ)=vˉ(ψ)\bar{v}(\varphi)=\bar{v}(\psi) pro každé vP2v \in{ }^{\P} 2, tj. výrok φψ\varphi \leftrightarrow \psi je pravdivý.

Definition

Model jazyka

Model jazyka nad P\P je ohodnocení z P{ }^{\P} 2. Třída všech modelů jazyka nad P\P se značí M(P)M(\P), tedy M(P)=P2M(\P)={ }^{P_{2}}. Výrok φ\varphi nad P(\P( je ))

Výroky φ\varphi a ψ\psi jsou logicky ekvivalentní, pokud mají stejné modely.

Definition

Univerzálnost spojek

Množina spojek je univerzální, pokud lze každou Booleovskou funkci reprezentovat nějaký z nich (dobře) vytvořeným výrokem.

Definition

Literál

Literál je prvovýrok nebo jeho negace. Je-li pp prvovýrok, označíme p0p^{0} literál ¬p\neg p a p1p^{1} literál pp. Je-li ll literál, označíme lˉ\bar{l} literál opačný k ll.

Definition

Klauzule

Klauzule je disjunkce literálů. Prázdnou klauzulí rozumíme \perp.

Definition

CNF

Výrok je v konjunktivně normálním tvaru (Conjunctive N Form),jelikonjunkcıˊklauzulıˊ.PraˊzdnyˊmvyˊrokemvCNFrozumıˊme, je-li konjunkcí klauzulí. Prázdným výrokem v **CNF** rozumímeT$$.

Definition

Elementární konjunkce

Elementární konjunkce je konjunkce literálů, prázdnou konjunkcí je \top.

Definition

DNF

Výrok je v disjunktivně normálním tvaru (Disjuctive Normal Form), je-li disjunkcí elementárních konjunkcí. Prázdným výrokem v DNF rozumíme \perp.

Definition

k-CNF

Výrok je v k-CNF, je-li v CNF a každá jeho klauzule má nejvýše kk literálů.

Definition

k-SAT

kk-SAT je pro pevné k>0k>0 problém hledání, zda je výrok φvk\varphi \mathrm{v} k-CNF splnitelný.

Definition

Implikační graf

Implikační graf výroku φ\varphi v 2-CNF je orientovaný graf GφG_{\varphi}, v němž

Definition

Jednotková klauzule

Jednotková klauzule je klauzule obsahující jediný literál.

Definition

Hornova klauzule

Hornova klauzule je klauzule obsahující nejvýše jeden pozitivní literál.

Hornův výrok

Hornův výrok je konjunkcí Hornových klauzulí.

Horn-SAT

Horn-SAT je problém splnitelnosti daného Hornova výroku.

Definition

Teorie

Výroková teorie nad jazykem P\P je libovolná množina TT výroků z VFPV F_{P}. Výrokům z TT říkáme axiomy teorie TT. Je-li teorie konečná, lze ji nahradit konjunkcí jejích axiomů.

Definition

Model teorie

Model teorie TT nad P\P je ohodnocení vM(P)v \in M(\P) (tj. model jazyka), ve kterém platí všechny axiomy z TT, značíme vTv \models T.

Definition

Třída modelů

Třída modelů TT je MP(T)={vM(P)vφM^{\P}(T)=\{v \in M(\P) \mid v \models \varphi pro každé φT}\varphi \in T\}.

Definition

Sémantika vzhledem k\mathrm{k} teorii

Nechť TT je teorie nad P\P. Výrok φ\varphi nad P\P je

Výroky φ\varphi a ψ\psi jsou ekvivalentní v TT ( T-ekvivalentní), pokud každý model teorie TT je modelem φ\varphi právě když je modelem ψ\psi.

Důsledek teorie

Důsledek teorie TT je θP(T)={φVFPTφ}\theta^{\P}(T)=\left\{\varphi \in \operatorname{VF}_{\P} \mid T \models \varphi\right\}, tj. množina θP(T)\theta^{\P}(T) všech výroků pravdivých v TT.

Vlastnosti teorií

Nechť TT je teorie nad P\P. Je-li φ\varphi dokazatelná z TT, řekneme, že φ\varphi je věta (teorém) teorie TT. Množinu vět teorie TT označme

ThmP(T)={φVFPTφ}.\operatorname{Thm}^{\P}(T)=\left\{\varphi \in \mathrm{VF}_{\P} \mid T \vdash \varphi\right\} .

Výroková teorie TT nad P\P je

Jinými slovy je teorie TT splnitelná (bezesporná), když má model, kompletní, právě když má jediný model, extenze TT^{\prime}, právě když modely TT jsou podmnožinou modelů TT^{\prime}, ekvivalentní s TT^{\prime}, pokud mají stejné modely.

Analýza teorií nad konečně prvovýroky

Nechť TT je bezesporná teorie nad PP, kde P=nN+\|\P\| = n \in \N^{+}a m=MP(T)m=\left|M^{\P(T)}\right|. Pak

Formální dokazovací systémy

Ve standardních formálních dokazovacích systémech

Od formálního dokazovacího systému čekáme, že je

Definition

Tablo metoda

Předpokládáme pevný a spočetný jazyk (množina prvovýroků P\P je spočetná). Pak každá teorie nad P\P je spočetná.

Hlavní rysy tablo metody

Vrcholy tabla jsou označeny položkami. Položka je formule s příznakem T/FT / F, který reprezentuje předpoklad, že formule v nějakém modelu platí/neplatí.

Definition

Tablo

Konečné tablo je binární, položkami značkovaný strom daný předpisem

Tablo je posloupnost konečných tabel takových, že další tablo vznikne z předchozího pomocí pravidla číslo 2.2 .

Tablo důkaz

Nechť PP je položka na větvi VV tabla τ\tau. Řekneme, že

Tablo důkaz výrokové formule φ\varphi je sporné tablo s položkou FφvF \varphi \mathrm{v} kořeni. Formule φ\varphi je (tablo) dokazatelná, píšeme φ\vdash \varphi, má-li tablo důkaz.

Zamítnutí formule φ\varphi tablem je sporné tablo s položkou TφvT \varphi \mathrm{v} kořeni. Formule φ\varphi je (tablo) zamítnutelná, má-li zamítnutí tablem, tj. ¬φ\vdash \neg \varphi.

Tablo z teorie

Konečné tablo z teorie TT je binární, položkami značkovaný strom daný předpisem

Tablo z teorie TT je posloupnost konečných tabel z TT takových, že další tablo vznikne z předchozího pomocí pravidla číslo 2 nebo 3.

Tablo důkaz z teorie

Nechť PP je položka na větvi VV tabla τ\tau z teorie TT. Řekneme, že

Tablo důkaz formule φz\varphi \mathrm{z} teorie TT je sporné tablo z TT s položkou FφvF \varphi \mathrm{v} kořeni. Má-li φ\varphi tablo důkaz z TT, je (tablo) dokazatelná zTz T, píšeme TφT \vdash \varphi.

Zamítnutí formule φ\varphi tablem z teorie TT je sporné tablo z TT s položkou TφvT \varphi \mathrm{v} kořeni. Formule φ\varphi je (tablo) zamítnutelná z TT, má-li zamítnutí tablem z TT, tj. T¬φT \vdash \neg \varphi.

Systematické tablo

Konstrukce, která vede vždy k dokončenému tablu.

Nechť RR je položka a T={φ0,φ1,}T=\left\{\varphi_{0}, \varphi_{1}, \ldots\right\} je konečná či nekonečná teorie.

  1. Ta τ0\tau_{0} vezmi atomické tablo pro RR. Doku to lze, aplikuj následující kroky.
  2. Nechť PP je nejlevější položka v\mathrm{v} co nejmenší úrovni již daného tabla τn\tau_{n}, která není redukovaná na nějaké bezesporné větvi procházející skrze PP.
  3. Za τn\tau_{n}^{\prime} vezmi tablo vznikl z τn\tau_{n} přidáním atomického tabla pro PP na každou bezespornou větev skrze PP. (Neexistuje-li PP, vezmi τn=τn\tau_{n}^{\prime}=\tau_{n}.)
  4. Za τn+1\tau_{n+1} vezmi tablo vzniklé z τn\tau_{n}^{\prime} přidáním TφnT \varphi_{n} na každou bezespornou větev neobsahující TφnT \varphi_{n}. (Neexistuje-li φn\varphi_{n}, vezmi τn+1=τn\tau_{n+1}=\tau_{n}^{\prime}.)

Systematické tablo z teorie TT pro položku RR je výsledkem uvedené konstrukce.

Rezoluční metoda.

Hlavní rysy rezoluční metody

Definition

Klauzule

Klauzule CC je konečná množina literálů (“tvořících disjunkci”). Prázdná klauzule se značí \square, nikdy není splněna (neobsahuje splněný literál).

Definition

Formule

Formule SS je množina (i nekončená) klauzulí (“tvořících konjunkci”). Prázdná formule \emptyset je vždy splněna (neobsahuje nesplněnou klauzuli). Nekonečné formule reprezentují nekonečné teorie.

(Částečné) ohodnocení

Částečné ohodnocení V\mathcal{V} je libovolná konzistentní množina literálů, tj. neobsahující dvojici opačných literálů. Ohodnocení V\mathcal{V} je totální, obsahuje-li pozitivní či negativní literál od každé výrokové proměnné.

Definition

Rezolventa

Nechť C1,C2C_{1}, C_{2} jsou klauzule a lC1,lˉC2l \in C_{1}, \bar{l} \in C_{2} pro nějaký literál ll. Pak z C1C_{1} a C2C_{2} odvod’ pres literál ll klauzuli CC, kterou nazveme rezolventa, kde

C=(C1\{l})(C2\{lˉ}).C=\left(C_{1} \backslash\{l\}\right) \cup\left(C_{2} \backslash\{\bar{l}\}\right) .

Definition

Rezoluční důkaz

Formální popis rezolučního důkazu.

Rezoluční strom

Rezoluční strom klauzule CC z formule SS je konečný binární strom s vrcholy označenými klauzulemi takový, že

Rezoluční uzávěr

Rezoluční uzávěr R(s)\mathcal{R}(s) formule SS je nejmenší induktivní množina definovaná

Lineární rezoluce

Rezoluce jako lineární důkaz.

LI-rezoluce

Pro Hornovy formule můžeme lineární rezoluci dál omezit.

LI-rezoluce (linear input) z formule SS je lineární rezoluce z SS, ve které je každá boční klauzule BiB_{i} ze (vstupní) formule SS.

Predikátová logika

Definition

Jazyk

Jazyk prvního řádu obsahuje proměnné, množinu všech proměnných značíme Var, funkční symboly (včetně konstantních symbolů, což jsou nulární funkční symboly), relační symboly, případně symbol = jako speciální relační symbol, kvantifikátory, logické spojky, závorky. Každá funkční i relační symbol SS má danou aritu - ar(S)N\operatorname{ar}(S) \in \N.

Signatura jazyka

Proměnné, kvantifikátory, logické spojky a závorky jsou logické symboly, funkční a relační symboly jsou mimologické symboly. Rovnost případně uvažujeme zvlášť.

Signatura je dvojice R,F\langle\mathcal{R}, \mathcal{F}\rangle disjunktních relačních a funkčních symbolů s danými aritami, žádný z nich není rovnost. Signatura tedy určuje všechny mimologické symboly.

Jazyk je dám signaturou L=R,FL=\langle\mathcal{R}, \mathcal{F}\rangle a uvedením, zda jde o jazyk s rovností či bez. Jazyk musí obsahovat alespoň jeden relační symbol (mimologický či rovnost).

Term

Term je výraz reprezentující hodnoty (složených) funkcí. Konstantní (ground) term je term bez proměnných. Množinu všech termů jazyka LL značíme TermL\operatorname{Term}_{L}.

Termy jazyka LL jsou dány induktivně

Atomická formule

Atomická formule je nejjednodušší formule. Atomická formule jazyka LL je výraz R(t0,,tn1)R\left(t_{0}, \ldots, t_{n-1}\right), kde RR je nn-ární relační symbol jazyka LL a t0,,tn1t_{0}, \ldots, t_{n-1} jsou termy jazyka LL. Množinu všech atomických formulí jazyka LL značíme AFmL\mathrm{AFm}_{L}.

Formule

Formule jazyka LL jsou výrazy dané induktivně každá atomická formule jazyka LL je formule, jsou-li φ,ψ\varphi, \psi formule, pak i následující výrazy jsou formule

(¬φ),(φψ),(φψ),(φψ),(φψ),(\neg \varphi),(\varphi \wedge \psi),(\varphi \vee \psi),(\varphi \rightarrow \psi),(\varphi \leftrightarrow \psi),

je-li φ\varphi formule a xx proměnná, jsou výrazy ((x)φ)((\forall x) \varphi) a ((x)φ)((\exists x) \varphi) formule, každá formule vznikne konečným užitím předchozích pravidel.

Množinu všech formulí jazyka LL značíme FmL\mathrm{Fm}_{L}.

Výskyt proměnné

Nechť φ\varphi je formule a xx proměnná.

Otevřená a uzavřená formule

Formule je otevřená, pokud neobsahuje žádný kvantifikátor. Pro množinu OFmL\mathrm{OFm}_{L} všech otevřených formulí jazyka LL platí AFmFOFmLFmL\mathrm{AFm}_{F} \subsetneq \mathrm{OFm}_{L} \subsetneq \mathrm{Fm}_{L}.

Formule je uzavřená (sentence), pokud nemá žádnou volnou proměnnou, tj. všechny výskyty proměnných jsou vázané.

Formule může být uzavřená i otevřená zároveň, pak její termy jsou konstantní.

Instance a substituce

Pokud do formule za volnou proměnnou dosadíme term tt, požadujeme, aby nově vzniklá formule říkala o termu tt totéž, co předtím o proměnné.

Varianty

Kvantifikované proměnné lze za určitých podmínek přejmenovat tak, že vznikne ekvivalentní formule. Nechť (Qx)ψ(Q x) \psi je podformule ve φ\varphi, kde QQ značí \forall čí \exists, a yy je proměnná, tak že

  1. yy je substituovatelná za xx do ψ\psi, a
  2. yy nemá volný výskyt vψ\mathrm{v} \psi.

Nahrazením podformule (Qx)ψ(Q x) \psi za (Qy)ψ(x/y)(Q y) \psi(x / y) vznikne varianta formule φ\varphi podformuli (Qx)ψ(Q x) \psi.

Struktura pro jazyk

Nechť L=R,FL=\langle\mathcal{R}, \mathcal{F}\rangle je jazyk a AA je neprázdná množina.

Struktura pro jazyk LL (L-struktura) je trojice A=A,RA,FA\mathcal{A}=\left\langle A, \mathcal{R}^{A}, \mathcal{F}^{A}\right\rangle, kde

Strukturu pro jazyk LL nazýváme také model jazyka LL. Třída všech modelů se značí M(L)M(L).

Hodnota termu

Nechť tt je term jazyka L=R,FL=\langle\mathcal{R}, \mathcal{F}\rangle a A=A,RA,FA\mathcal{A}=\left\langle A, \mathcal{R}^{A}, \mathcal{F}^{A}\right\rangle je struktura pro LL.

xA[e]=e(x) pro kazˇdeˊ x Var, (f(t0,,tn1))A[e]=fA(t0A[e],,tn1A[e]) pro kazˇdeˊ fF.\begin{aligned} x^{\mathcal{A}}[e] &=e(x) \text { pro každé } x \in \text { Var, } \\ \left(f\left(t_{0}, \ldots, t_{n-1}\right)\right)^{\mathcal{A}}[e] &=f^{A}\left(t_{0}^{\mathcal{A}}[e], \ldots, t_{n-1}^{\mathcal{A}}[e]\right) \text { pro každé } f \in \mathcal{F} . \end{aligned}

Hodnota atomické formule

Nechť φ\varphi je atomická formule tvaru R(t0,,tn1)R\left(t_{0}, \ldots, t_{n-1}\right) jazyka L=R,FL=\langle\mathcal{R}, \mathcal{F}\rangle a A=A,RA,FA\mathcal{A}=\left\langle A, \mathcal{R}^{A}, \mathcal{F}^{A}\right\rangle je struktura pro LL.

HatA(R(t0,,tn1))[e]=1, pokud (t0A[e],,tn1A[e])RA, jinak 0,H_{a t}^{\mathcal{A}}\left(R\left(t_{0}, \ldots, t_{n-1}\right)\right)[e]=1, \text { pokud }\left(t_{0}^{\mathcal{A}}[e], \ldots, t_{n-1}^{\mathcal{A}}[e]\right) \in R^{A}, \text { jinak } 0,

přičemž =A={ }^{\mathcal{A}} je IdA\operatorname{Id}_{A}, tj. HatA(t0=t1)[e]=1H_{a t}^{\mathcal{A}}\left(t_{0}=t_{1}\right)[e]=1 pokud t0A[e]=t1A[e]t_{0}^{\mathcal{A}}[e]=t_{1}^{\mathcal{A}}[e], jinak 0 .

Platnost při ohodnocení

Formule φ\varphi je pravdivá (platí) ve struktuře A\mathcal{A} při ohodnocení ee, pokud HA(φ)[e]=1H^{\mathcal{A}}(\varphi)[e]=1. Pak píseme Aφ[e]\mathcal{A} \models \varphi[e], v opačném případě A⊭φ[e]\mathcal{A} \not \models \varphi[e].

Platnost ve struktuře

Nechť φ\varphi je formule jazyka LL a A\mathcal{A} je struktura pro LL.

Platnost v\mathbf{v} teorii

Teorie jazyka LL je libovolná množina TT formulí jazyka LL (tzv. axiomů). Model teorie TT je LL-struktura A\mathcal{A} taková, že Aφ\mathcal{A} \models \varphi pro každé φT\varphi \in T, značíme AT\mathcal{A} \models T. Třída modelů teorie TT je M(T)={AM(L)AT}M(T)=\{\mathcal{A} \in M(L) \mid \mathcal{A} \models T\}.

θL(T)={φFmLTφ a φ je sentence }.\theta^{L}(T)=\left\{\varphi \in \mathrm{Fm}_{L} \mid T \models \varphi \text { a } \varphi \text { je sentence }\right\} .

Vlastnosti teorií

Nechť TT je teorie jazyka LL. Je-li sentence φ\varphi pravdivá v TT, říkáme, že φ\varphi je věta teorie TT. Množinu vět teorie TT značíme ThmL(T)={φFmLTφ}\operatorname{Thm}^{L}(T)=\left\{\varphi \in \operatorname{Fm}_{L} \mid T \vdash \varphi\right\}. Teorie jazyka LL je sémanticky (syntakticky)

Struktury A,B\mathcal{A}, \mathcal{B} pro jazyk LL jsou elementárně ekvivalentní, značeno AB\mathcal{A} \equiv \mathcal{B}, platí-li v nich stejné formule.

Nechť TT a TT^{\prime} jsou teorie jazyka LL. Teorie TT je (sémanticky)

Podstruktura.

Nechť A=A,RA,FA\mathcal{A}=\left\langle A, \mathcal{R}^{A}, \mathcal{F}^{A}\right\rangle a B=B,RB,FB\mathcal{B}=\left\langle B, \mathcal{R}^{B}, \mathcal{F}^{B}\right\rangle jsou struktury pro jazyk L=R,FL=\langle\mathcal{R}, \mathcal{F}\rangle.

Řekneme, že B\mathcal{B} je (indukovaná) podstruktura A\mathcal{A}, značeno BA\mathcal{B} \subseteq \mathcal{A}, pokud

  1. BAB \subseteq A,
  2. RB=RABar(R)R^{B}=R^{A} \cap B^{\operatorname{ar}(R)} pro každé RRR \in \mathcal{R},
  3. fB=fA(Bar(f)×B)f^{B}=f^{A} \cap\left(B^{\operatorname{ar}(f)} \times B\right), tj. fBBar(f)f^{B} \mid B^{\operatorname{ar}(f)}, pro každé fFf \in \mathcal{F}.

Množina CAC \subseteq A je doménou nějaké podstruktury struktury A\mathcal{A}, právě když CC je uzavřená na všechny funkce struktury A\mathcal{A} (včetně konstant). Pak příslušnou podstrukturu značíme AC\mathcal{A}\lceil C a řkáme, že je to restrikce (parcializace) struktury A\mathcal{A} na CC. Množina CAC \subseteq A je uzavřená na funkcif : AnAA^{n} \rightarrow A, pokud f(x0,,xn1)Cf\left(x_{0}, \ldots, x_{n-1}\right) \in C pro každé x0,,xn1Cx_{0}, \ldots, x_{n-1} \in C.

Generovaná podstruktura, expanze, redukt.

Nechť A=A,RA,FA\mathcal{A}=\left\langle A, \mathcal{R}^{A}, \mathcal{F}^{A}\right\rangle je struktura a XAX \subseteq A. Označme BB nejmenší podmnožinu množiny AA obsahující XX, která je uzavřená na všechny funkce struktury A\mathbb{A} (včetně konstant). Pak strukturu AB\mathcal{A} \mid B značíme rovněž AX\mathcal{A}\langle X\rangle a podstruktura řkáme, že je to A\mathcal{A} generovaná množinou XX.

Nechť A\mathcal{A}^{\prime} je struktura pro jazyk LL^{\prime} a LLL \subseteq L^{\prime} je jazyk. Odebráním realizací symbolů, jež nejsou v LL, získáme z A\mathcal{A}^{\prime} strukturu A\mathcal{A}, kterou nazýváme redukt struktury A\mathcal{A}^{\prime} na jazyk LL. Obráceně, A\mathcal{A}^{\prime} je expanze struktury A\mathcal{A} do jazyka LL^{\prime}.

Definovatelné množiny

Množiny, které lze v dané struktuře definovat.

  1. Množina definovaná formulí φ(x1,,xn)\varphi\left(x_{1}, \ldots, x_{n}\right) ve struktuře A\mathcal{A} je množina

    φA(x1,,xn)={(a1,,an)AnAφ[e(x1/a1,,xn/an)]}.\varphi^{\mathcal{A}}\left(x_{1}, \ldots, x_{n}\right)=\left\{\left(a_{1}, \ldots, a_{n}\right) \in A^{n} \mid \mathcal{A} \models \varphi\left[e\left(x_{1} / a_{1}, \ldots, x_{n} / a_{n}\right)\right]\right\} .

    Zkráceně se dá x1,,xnx_{1}, \ldots, x_{n} zapsat jako xˉ\bar{x}, obdobně pro aa. Číslo nn je potom xˉ\|\bar{x}\|.

  2. Množina definovaná formulí φ(xˉ,yˉ)\varphi(\bar{x}, \bar{y}) s parametry bˉAyˉ\bar{b} \in A^{\|\bar{y}\|} ve struktuře A\mathcal{A} je

    φA,bˉ(xˉ,yˉ)={aˉAxˉAφ[e(xˉ/aˉ,yˉ,bˉ)]}.\varphi^{\mathcal{A}, \bar{b}}(\bar{x}, \bar{y})=\left\{\bar{a} \in A^{\|\bar{x}\|} \mid \mathcal{A} \models \varphi[e(\bar{x} / \bar{a}, \bar{y}, \bar{b})]\right\} .
  3. Pro strukturu A\mathcal{A}, množinu BAB \subseteq A a nNn \in \N označme Dfn(A,B)\operatorname{Df}^{n}(\mathcal{A}, B) třídu všech množin DAnD \subseteq A^{n} definovatelných ve struktuře As\mathcal{A} \mathrm{s} parametry z BB.

Tablo metoda v predikátové logice

Předpoklady:

  1. Dokazovaná formule φ\varphi je sentence. Není-li φ\varphi sentence, můžeme ji nahradit za její generální uzávěr φ\varphi^{\prime}, nebot pro každou teorii TT platí

    TφTφ.T \models \varphi \Leftrightarrow T \models \varphi^{\prime} .
  2. Dokazujeme z teorie v uzavřeném tvaru, tj. každý axiom je sentence. Nahrazením každého axiomu ψ\psi za jeho generální uzávér ψ\psi^{\prime} zíkáme ekvivalentní teorii, nebot pro každou strukturu A\mathcal{A} (daného jazyka LL ),

    AψAψ.\mathcal{A} \models \psi \Leftrightarrow \mathcal{A} \models \psi^{\prime} .
  3. Jazyk LL je spočetný. Pak každá teorie nad LL je spočetná. Označme LCL_{C} rozšíření jazyka LL o nové konstantní symboly c0,c1,c_{0}, c_{1}, \ldots (početně nekonečně mnoho). Platí, že konstantních termů jazyka LCL_{C} je spočetně. Nechť’ tit_{i} označuje ii-tý konstantní term (v pevně zvoleném očíslování).

Nová atomická tabla, kde φ\varphi je libovolná formule jazyka LCL_{C} ve volné proměnné x,tx, t je libovolný konstantní term jazyka LCL_{C} a cc je nový konstantní symbol z LC\LL_{C} \backslash L.

(#) Pokud mám formuli T(x)φ(x)T(\forall x) \varphi(x) nebo F(x)φ(x)F(\exists x) \varphi(x), za xx zvolím libovolný konstantní term tt a “zruším” kvantifikátor. Pravdivostní hodnota zůstává zachována.

(*) Pokud mám formuli F(x)φ(x)F(\forall x) \varphi(x) nebo T(x)φ(x)T(\exists x) \varphi(x), za xx dosadím novou konstantu cc a “zruším” kvantifikátor. Pravdivostní hodnota zůstává zachována. Konstantní symbol cc reprezentuje svědky položek, do kterých je dosazuji.

Tablo z teorie

Konečné tablo z teorie TT je binární, položkami značkovaný strom daný předpisem

Tablo z teorie TT je posloupnost konečných tabel z TT takových, že další tablo vznikne z předchozího pomocí pravidla číslo 2 nebo 3.

Položku, dle které tablo prodlužujeme, nebudeme na větev znovu zapisovat kromě případů (#)(\#)

Tablo důkaz

Vlastnosti tabla a tablo důkazu

Dokončené tablo

Chceme, aby dokončená bezesporná větev poskytovala protipříklad.

Výskyt položky PP ve vrcholu vv tabla τ\tau je ii-tý, pokud vvvτ\mathrm{v} \tau právě i1i-1 předků označených PP a je redukovaný na větvi VV skrze vv, pokud

Nechť VV je větev tabla τ\tau z teorie TT. Řekneme, že větev VV je dokončená, je-li sporná, nebo každý výskyt položky na VV je redukovaný na VV a navíc obsahuje TφT \varphi pro každé φT\varphi \in T. Rekneme, že tablo τ\tau je dokončené, pokud je každá jeho větev dokončená.

Konstrukce systematického tabla

Nechť RR je položka τ\tau a T={φ0,φ1,}T=\left\{\varphi_{0}, \varphi_{1}, \ldots\right\} je (konečná i nekonečná) teorie.

  1. Za τ0\tau_{0} vezmi atomické tablo pro RR. VV případě ()(*) vezmi lib. cLC\Lc \in L_{C} \backslash L, v případě () za tt vezmi term t1t_{1}. Dokud to lze, aplikuj následující kroky.
  2. Nechť vv je nejlevější vrchol v co nejmenší úrovni již daného tabla τn\tau_{n} obsahující výskyt položky PP, který není redukovaný na nějaké bezesporné větvi skrze vv. (Neexistuje-li vv, vezmi τn=τn\tau_{n}^{\prime}=\tau_{n} a jdi na (4).)

  3. a. Není-li PP tvaru (#), za τn\tau_{n}^{\prime} vezmi tablo vzniklé zτn\mathrm{z} \tau_{n} přidáním atomického tabla pro PP na každou bezespornou větev skrze vv. V případě ()\left({ }^{*}\right) za cc vezmi cic_{i} pro co nejmenší možné ii.
    b. Je-li PP tvaru (#) a ve vvii-tý výskyt, ta τn\tau_{n}^{\prime} vezmi tablo vzniklé z τn\tau_{n} připojením atomického tabla pro PP na každou bezespornou větev skrze vv, přičemž za tt vezmi term tit_{i}.
  4. Za τn+1\tau_{n+1} vezmi tablo vzniklé z τn\tau_{n}^{\prime} přidáním TφnT \varphi_{n} na každou bezespornou větev neobsahující TφnT \varphi_{n}. (Neexistuje-li φn\varphi_{n}, vezmi τn+1=τn\tau_{n+1}=\tau_{n}^{\prime}.)

Systematické tablo z TT pro RR je výsledkem uvedené konstrukce.

Axiomy rovnosti

Axiomy rovnosti pro jazyk LL s rovností jsou

Tablo důkaz z teorie TT jazyka LL s rovností je tablo důkaz z teorie TT^{*}, kde TT^{*} je rozšír̃ení teorie TT o axiomy rovnosti pro LL (resp. jejich generální uzávěry).

Kongruence a faktostruktura

Nechť \sim je ekvivalence na A,f:AnAA, f: A^{n} \rightarrow A a RAnR \subseteq A^{n}, kde nNn \in \N. Pak \sim je

x1y1xnynf(x1,,xn)f(y1,,yn),x_{1} \sim y_{1} \wedge \cdots \wedge x_{n} \sim y_{n} \Rightarrow f\left(x_{1}, \ldots, x_{n}\right) \sim f\left(y_{1}, \ldots, y_{n}\right), x1y1xnyn(R(x1,,xn)R(y1,,yn)).x_{1} \sim y_{1} \wedge \cdots \wedge x_{n} \sim y_{n} \Rightarrow\left(R\left(x_{1}, \ldots, x_{n}\right) \Leftrightarrow R\left(y_{1}, \ldots, y_{n}\right)\right) .

Nechť ekvivalence \sim ma AA je kongruence pro každou funkci i relaci struktury A=A,FA,RA\mathcal{A}=\left\langle A, \mathcal{F}^{A}, \mathcal{R}^{A}\right\rangle. Faktostruktura (podilová struktura) struktury A\mathcal{A} dle \sim je struktura A/=A/,FA/,RA/\mathcal{A} / \sim=\left\langle A / \sim, \mathcal{F}^{A / \sim}, \mathcal{R}^{A / \sim}\right\rangle, kde fA/([x1],,[xn])=[fA(x1,,xn)]f^{A / \sim}\left(\left[x_{1}\right]_{\sim}, \ldots,\left[x_{n}\right]_{\sim}\right)=\left[f^{A}\left(x_{1}, \ldots, x_{n}\right)\right]_{\sim} a RA/([x1],,[xn])RA(x1,,xn)R^{A / \sim}\left(\left[x_{1}\right]_{\sim}, \ldots,\left[x_{n}\right]_{\sim}\right) \Leftrightarrow R^{A}\left(x_{1}, \ldots, x_{n}\right) pro každé fF,RRf \in \mathcal{F}, R \in \mathcal{R} a x1,,xnAx_{1}, \ldots, x_{n} \in A, tj. funkce a relace jsou definované z A\mathcal{A} pomocí reprezentantů.

Kanonický model

Z\mathrm{Z} bezesporné větve VV dokončeného tabla vyrobíme model, který se shoduje s VV. Vyjdeme z dostupných syntaktických objektů - konstantních termů.

Nechť VV je bezesporná větev dokončeného tabla teorie TT jazyka L=F,RL=\langle\mathcal{F}, \mathcal{R}\rangle. Kanonický model z větve VV je LCL_{C}-struktura A=A,FA,RA\mathcal{A}=\left\langle A, \mathcal{F}^{A}, \mathcal{R}^{A}\right\rangle, kde

Poznámka: Výraz f(s1,,sn)f\left(s_{1}, \ldots, s_{n}\right) ve druhém bodě je konstantní term jazyka LCL_{C}, tedy prvek z AA.

Kanonický model s rovností

Je-li jazyk LL s rovností, TT^{*} označuje rozšíření TT o axiomy rovnosti pro LL.

Požadujeme-li, aby rovnost byla interpretována jako identita, kanonický model A\mathcal{A} z bezesporné větve VV dokončeného tabla TT^{*} musíme faktorizovat dle =A=^{A}.

Dle třetí definice, v modelu A\mathcal{A} z VV pro relaci =A=^{A} platí, že pro každé s1,s2As_{1}, s_{2} \in A,

s1=As2T(s1=s2) je polozˇka na V.s_{1}={ }^{A} s_{2} \Leftrightarrow T\left(s_{1}=s_{2}\right) \text { je položka na } V .

Jelikož je VV dokončená a obsahuje axiomy rovnosti, relace =A=^{A} je ekvivalence na AA a navíc kongruence pro všechny funkce a relace vA\mathrm{v} \mathcal{A}.

Kanonický model s rovností z větve VV je faktostruktura A/=A\mathcal{A} /=^{A}.

Extenze o definovaný relační symbol

Nechť TT je teorie jazyka L,ψ(x1,,xn)L, \psi\left(x_{1}, \ldots, x_{n}\right) je formule jazyka LL ve volných proměnných x1,,xnx_{1}, \ldots, x_{n} a LL^{\prime} je rozšíření LL o nový nn-ární relační symbol RR.

Extenze teorie TT o definici RR formulí ψ\psi je teorie TT^{\prime} vzniklá přidáním axiomu

R(x1,,xn)ψ(x1,,xn).R\left(x_{1}, \ldots, x_{n}\right) \leftrightarrow \psi\left(x_{1}, \ldots, x_{n}\right) .

Každý model teorie TT lze jednoznačně expandovat na model T,TT^{\prime}, T^{\prime} je potom konzervativní extenze TT.

Extenze o definovaný funkční symbol

Nechť TT je teorie jazyka LL a pro formuli ψ(x1,,xn,y)\psi\left(x_{1}, \ldots, x_{n}, y\right) jazyka LL ve volných proměnných x1,,xn,yx_{1}, \ldots, x_{n}, y platí

T(y)ψ(x1,,xn,y) (existence) Tψ(x1,,xn,y)ψ(x1,,xn,z)y=z (jednoznacˇnost) \begin{aligned} &T \models(\exists y) \psi\left(x_{1}, \ldots, x_{n}, y\right) \text { (existence) } \\ &T \models \psi\left(x_{1}, \ldots, x_{n}, y\right) \wedge \psi\left(x_{1}, \ldots, x_{n}, z\right) \rightarrow y=z \text { (jednoznačnost) } \end{aligned}

Označíme LL^{\prime} rozšírení LL o nový nn-ární funkční symbol ff.

Extenze teorie TT o definici ff formulí ψ\psi je teorie TT^{\prime} vzniklá přidáním axiomu

f(x1,,xn)=yψ(x1,,xn).f\left(x_{1}, \ldots, x_{n}\right)=y \leftrightarrow \psi\left(x_{1}, \ldots, x_{n}\right) .

Každý model teorie TT lze jednoznačně expandovat na model T,TT^{\prime}, T^{\prime} je potom konzervativní extenze TT.

Extenze o definice

Teorie TT^{\prime} jazyka LL^{\prime} je extenze teorie TT jazyka LL o definice, pokud vznikla z TT postupnou extenzí o definici relačního či funkčního symbolu.

Ekvisplnitelnost

Problém splnitelnosti lze redukovat na otevřené teorie.

K teorii TT nalezneme ekvisplnitelnou teorii následovně:

  1. Axiomy TT nahradíme za ekvivalentní formule v prenexním tvaru.
  2. Pomocí nových funkčních symbolů je převedeme na univerzální formule, tzv. Skolemovy varianty, čímž dostaneme ekvisplnitelnou teorii.
  3. Jejich otevřená jádra tvoří hledanou teorii.

Vytýkání kvantifikátorů

Pro každé formule φ,ψ\varphi, \psi takové, že xx není volná ve formuli ψ\psi,

¬(Qx)φ(Qˉx)¬φ((Qx)φψ)(Qx)(φψ)((Qx)φψ)(Qx)(φψ)((Qx)φψ)(Qˉx)(φψ)(ψ(Qx)φ)(Qx)(ψφ)\begin{aligned} &\models \neg(Q x) \varphi \leftrightarrow(\bar{Q} x) \neg \varphi \\ &\models((Q x) \varphi \wedge \psi) \leftrightarrow(Q x)(\varphi \wedge \psi) \\ &\models((Q x) \varphi \vee \psi) \leftrightarrow(Q x)(\varphi \vee \psi) \\ &\models((Q x) \varphi \rightarrow \psi) \leftrightarrow(\bar{Q} x)(\varphi \rightarrow \psi) \\ &\models(\psi \rightarrow(Q x) \varphi) \leftrightarrow(Q x)(\psi \rightarrow \varphi) \end{aligned}

Skolemova varianta

Nechť φ\varphi je sentence jazyka LL v prenexním normálním tvaru, y1,,yny_{1}, \ldots, y_{n} jsou existenčně kvantifikované proměnné ve φ\varphi (v tomto pořadí) a pro každé ini \leq n nechť x1,,xnix_{1}, \ldots, x_{n_{i}} jsou univerzálně kvantifikované proměnné před yiy_{i}. Označme LL^{\prime} rozšírení LL o nové nin_{i}-ární symboly fif_{i} pro každé in.i \leq n .

Nechť φS\varphi_{S} je formule jazyka LL^{\prime}, jež vznikne z formule φ\varphi odstraněním (yi)\left(\exists y_{i}\right) z jejího prefixu a nahrazením každého výskytu proměnné yiy_{i} za term fi(s1,,xni)f_{i}\left(s_{1}, \ldots, x_{n_{i}}\right). Pak formule φS\varphi_{S} se nazývá Skolemova varianta formule φ\varphi.

Redukce nesplnitelnosti na úroveň VL

Je-li otevřená teorie nesplnitelná, lze to “doložit na konkrétních prvcích”. Doložení má podobu nesplnitelných konjunkcí konečně mnoha instancí (některých) axiomů teorie TT v konstantních termech.

Herbrandův model

Nechť’ L=R,FL=\langle\mathcal{R}, \mathcal{F}\rangle je jazyk s alespoň jedním konstantním symbolem. (Pokud je třeba, co LL přidáme nový.)

Rezoluční metoda vv predikátové logice

Stručný popis RM v PL:

Substituce

Vlastnosti substitucí: