Predikátová logika - dedukčné kalkuly

Terminológia

Substitúcia (definovaná na predchádzajúcom cvičení) je funkcia na termoch a na formulách, budeme je označovať $σ$.

Variant formuly $(Q x)φ$, (kde $Q$ je ľubovoľný kvantifikátor), je formula $(Q y)φ[y/x]$ pričom $y$ nemá voľný výskyt v $φ$. To znamená, ako už bolo načrtnuté v predchádzajúcom cvičení, viazanú premennú je možné premenovať t.j. substituovať za inú premennú, ktorá nemá voľný výskyt v danej formule pričom platí, že pôvodná formula je sémanticky ekvivalentná s novou formulou $(Q x)φ ≡ (Q y)φ[y/x]$.

Gödelova veta o úplnosti (predikátovej logiky) (Gödel's completeness theorem) hovorí, že ak formula $φ$ platí (pravdivá v nezávisle na modely a interpretácii), potom je $φ$ dokázateľná. To znamená:
$$\text{ak}~ \quad Γ \models φ \quad \text{potom}~ \quad Γ \vdash φ.$$

Gödelova veta o neúplnosti (Gödel's incompleteness theorems) hovorí, že akýkoľvek formálny systém, ktorý dokáže vyjadriť základnú aritmetiku bude obsahovať tvrdenia (formuly), ktoré sú pravdivé ale nie je možné ich dokázať a zároveň nie je možné dokázať ani ich negácie.

Prirodzená dedukcia v predikátovej logike

Prirodzená dedukcia v predikátovej logike (systém NK) pozostáva z dedukčných pravidiel výrokovej logiky a je rozšírená o štyri pravidlá pre kvantifikátory.

Prirodzená dedukcia v predikátovej logike je konzistentná a úplná, platí: $$Γ \models φ \quad \text{vtt.}~ \quad Γ \vdash φ.$$

Eliminácia všeobecného kvantifikátora

Dedukčné pravidlo pre elimináciu všeobecného kvantifikátora:

Vychádza z jednoduchého princípu, ak $(∀x)φ$ je pravda, potom viazanú premennú $x$ je možné substituovať ľubovoľným termom $t$ a $φ[t/x]$ musí byť pravda. Vychádza zo zákona $(∀x)P(x) ⇒ P(t)$.

Zavedenie všeobecného kvantifikátora

Dedukčné pravidlo pre zavedenie všeobecného kvantifikátora:

Aby bolo možné dokázať $(∀x)φ$ je potrebné najskôr dokázať $φ[t/x]$ je pravda, pre každý prvok domény. Samozrejme, že nechceme dokázať $φ[t/x]$ pre všetky možnosti, pričom doména môže byť nekonečná. Namiesto toho postačuje ukázať, že $φ[t/x]$ je pravda pre ľubovoľný prvok $t$. To znamená, term $t$ musí byť nový (fresh), t.j. $t$ nesmie mať voľný výskyt v hypotézach, z ktorých je možné dokázať $φ[t/x]$.

Eliminácia existenčného kvantifikátora

Dedukčné pravidlo pre elimináciu existenčného kvantifikátora:

Pravidlo pre elimináciu existenčného kvantifikátora je komplexnejšie. Ak vieme, že platí $(∃x)φ[t/x]$, pre elimináciu existenčného kvantifikátora je potrebné nájsť také $t$, že $φ[t/x]$ je pravdivé. To je zabezpečené jednoduchým trikom a to tak, že vo vedľajšej vetve zavedieme novú hypotézu, kde vo $φ$ substituujeme $x$ za konkrétny prvok $t$ z ktorej dokážeme $ψ$. Term $t$ musí byť nový (fresh), t.j. $t$ nesmie mať voľný výskyt v hypotézach, z ktorých je možné dokázať $φ[t/x]$ ani $ψ$.

Zavedenie existenčného kvantifikátora

Dedukčné pravidlo pre zavedenie existenčného kvantifikátora:

Pravidlo opisuje zákon $P(a) ⇒ (∃x)P(x)$. To znamená, ak je možné dokázať, že $φ[t/x]$ je pravda, tak musí platiť tvrdenie $(∃x)φ$.

Dedukčné pravidlá prirodzenej dedukcie pre predikátovú logiku

Sekventový kalkul v predikátovej logike

Analogicky ako v prirodzenej dedukcii, pri sekventovom kalkule (systém LK) je taktiež potrebné pridať štyri nové dedukčné pravidlá pre kvantifikátory (pre každý kvantifikátor jedno pravidlo pre obe strany sekventu).

Sekventový kalkul v predikátovej logike je konzistentný a úplný, platí: $$Γ \models φ \quad \text{vtt.}~ \quad Γ \vdash φ.$$

Dedukčné pravidlá pre všeobecný kvantifikátor

• Pravidlo $(∀l)$ sa nazýva pravidlo konkretizácie. Term $t$ musí byť substituovateľný za premennú $x$ vo formule $\varphi$.
• Pravidlo $(∀r)$ sa nazýva pravidlo generalizácie. Premenná $y$ musí byť substituovateľná za premennú $x$ vo formule $\varphi$ a nemať žiadny voľný výskyt v množine predpokladov $Γ$, množine záverov $Δ$ a v $(∀x)φ$.

Dedukčné pravidlá pre existenčný kvantifikátor

• Pravidlo $(∃r)$ sa nazýva pravidlo konkretizácie. Term $t$ musí byť substituovateľný za premennú $x$ vo formule $\varphi$.
• Pravidlo $(∃l)$ sa nazýva pravidlo generalizácie. Premenná $y$ musí byť substituovateľná za premennú $x$ vo formule $\varphi$ a nemať žiadny voľný výskyt v množine predpokladov $Γ$, množine záverov $Δ$ a v $(∀x)φ$.

Dedukčné pravidlá sekventového kalkulu pre predikátovú logiku

Pravidlo identity a rezu:

Logické pravidlá:

Negácia

Konjunkcia

Disjunkcia

Implikácia

Konštanty

Kvantifikátory

Štrukturálne pravidlá:

Pravidlá zoslabenia

Pravidlá kontrakcie

Pravidlá výmeny

Rezolučná metóda a automatické dokazovanie v predikátovej logike

Na štvrtom cvičení bola prezentovaná rezolučná metóda ako spôsob automatického dokazovania vo výrokovej logike. Zovšeobecnenie rezolučnej metódy pre predikátovú logiku žiaľ nie je také triviálne ako v prípade Gentzenových dedukčných kalkulov.

Rezolučná metóda v predikátovej logike je konzistentná a úplná sporom (refutation completeness) avšak je semi-rozhodnuteľná. To znamená, ak formula je kontradikcia, tak rezolučná metóda v konečnom počte krokov túto skutočnosť zistí a zastaví svoje vykonávanie. Avšak ak je formula splniteľná (nie tautológia), algoritmus nemusí skončiť svoje vykonávanie.

Pred tým ako zovšeobecníme rezolučnú metódu pre predikátovú logiku, je potrebné zaviesť niekoľko nových pojmov. Pre aplikovanie rezolučnej metódy musí byť formula predikátovej logiky v požadovanom klauzulárnom tvare.

Zjednodušený postup ako dostať formulu predikátovej logiky do klauzulárneho tvaru je nasledovný:

1. Negácia formuly.
2. Prevod formuly na prenexný normálny tvar, v ktorom všetky kvantifikátory sa nachádzajú na začiatku formuly.
3. Úprava formuly na Skolemovský normálny tvar, kde sa procesom nazývaním skolemizácia odstránia existenčné kvantifikátory.
4. Vynechanie všeobecných kvantifikátorov (formula je uzavretá, každá premenná je implicitne všeobecne kvantifikovaná).
5. Prevod formuly na konjunktívny normálny tvar.
6. Úprava formuly v KNF na množinovú notáciu KNF.

Prenexný normálny tvar

Formula $φ$ je v prenexnom normálnom tvare ak: $$φ=(Q_1x_1)(Q_2x_2)...(Q_nx_n)φ',$$ kde:

• $Q_i ∈ \{∀,∃\}$ pre akékoľvek $(1≤i≤n)$,
• $φ'$ neobsahuje kvantifikátory.

Zjednodušene povedané, všetky kvantifikátory $Q_ix_i$ musia byť na začiatku formuly, všetky premenné $x_i$ musia byť navzájom rôzne a $φ'$ je otvorená formula (jadro formuly).

Pre každú formulu $φ$ predikátovej logiky existuje sémanticky ekvivalentná formula $φ'$, ktorá je v prenexnom normálnom tvare.

Prevod formuly na prenexný normálny tvar:

1. Eliminácia ekvivalencií a implikácii.
2. Vloženie (potlačenie) negácií do vnútra, tak že negácie sa budú nachádzať len pred atomickými formulami.
3. Premenovanie viazaných premenných, v prípade výskytu rovnakej premennej vo viacerých kvantifikátoroch (variant formuly).
4. Presun kvantifikátorov na začiatok formuly.

Skolemovský normálny tvar

Ďalším krokom potrebným na úpravu formuly predikátovej logiky do tvaru vhodného pre rezolučnú metódu je skolemizácia (proces transformácie formuly na Skolemovský normálny tvar). Skolemizáciou sa odstránia existenčné kvantifikátory tak, že každá viazaná premenná existenčným kvantifikátorom je nahradená skolemovskou konštantou alebo skolemovskou funkciou. Takáto transformácia nezachováva sémantickú ekvivalenciu formúl ale výsledná formula je ekvisplniteľná. To znamená, ak pôvodná formula je nesplniteľná, tak aj formula v skolemovskom normálnom tvare je nesplniteľná. Pričom pravé nesplniteľnosť je kľúčová vlastnosť, ktorú skúma rezolučná metóda.

Skolemizácia

Majme nasledujúcu formulu v prenexnom tvare $$φ=(∀x_1)(∀x_2)...(∀x_k)(∃x)φ',$$ kde $k≥0$, pričom $φ'$ môže obsahovať ďalšie kvantifikátory. Inými slovami, máme $k$ všeobecných kvantifikátorov pred prvým existenčným kvantifikátorom.

Nech $f$ je funkčný symbol s aritou $k$, ktorý sa nenachádza vo $φ$ (nový funkčný symbol (fresh)). Potom existuje formula $ψ$, ktorá je ekvisplniteľná s $φ$: $$ψ=(∀x_1)(∀x_2)...(∀x_k)σ(φ'),$$ kde: $$σ=[f(x_1,x_2,...,x_k)/x]$$ a platí $$φ ≡_e ψ$$

Či sa jedná o substitúciu skolemovskou funkciou alebo konštantou závisí od toho, či sa pred existenčným kvantifikátorom (vľavo) nachádza jeden (prípadne viacero) všeobecných kvantifikátorov alebo žiaden.

Majme formulu $φ=(Q_1x_1)...(Q_nx_n)φ'$ v prenexnom normálnom tvare, kde $Q_i ∈ \{∀,∃\}$. Potom pre každý výskyt existenčného kvantifikátora $Q_i$ v $φ$:

• Ak sa pred $Q_ix_i$ (vľavo od $Q_ix_i$) nenachádzajú žiadne všeobecné kvantifikátory, zavedieme do modelu novú konštantu $c_i$, vynecháme existenčný kvantifikátor a aplikujeme substitúciu $σ_i=[c_i/x_i]$ na jadro formuly $φ'$.
• Ak sa pred $Q_ix_i$ (vľavo od $Q_ix_i$) nachádza $k$ všeobecných kvantifikátorov, zavedieme do modelu nový funkčný symbol $f_i$ s aritou $k$, vynecháme existenčný kvantifikátor a aplikujeme substitúciu $σ_i=[f_k(x_1,...,x_k)/x_i]$ na jadro formuly $φ'$. Argumenty nového funkčného symbolu sú závislé na všeobecných kvantifikátoroch.
• Ak formula obsahuje viacero existenčných kvantifikátorov, odstraňujeme ich postupne zľava. Je potrebné mať na pamäti, že postupnosť kvantifikátorov v skutočnosti vyjadruje vnorenie kvantifikátorov.