Ciele
- Naštudovať potrebné pojmy.
- Preštudovať vzorové príklady prezentované v rámci teoretickej časti.
- Vypracovať zadané úlohy.
Základne pojmy
Predchádzajúce cvičenia sa zaoberali syntaxou a sémantikou výrokovej logiky. Skúmali sa otázky pravdivosti, splniteľnosti a logického vyplývania. Toto cvičenie bude venované ďalšej dôležitej oblasti každého logického systémy - dedukčným kalkulom.
Predchádzajúce cvičenia boli venované aj pravdivostným tabuľkám ako metóde pre vyhodnotenie formúl. Ich konštrukcia je systematická a jednoducho mechanizovateľná, avšak počet riadkov tabuľky rastie exponenciálne s počtom premenných vo formule, čo z hľadiska algoritmickej zložitosti je jeden z najhorších prípadov a práve tento problém riešia dedukčné kalkuly.
Dôkaz dedukciou je to spôsob dôkazu pri ktorom tvrdenie vyplýva z iných tvrdení. Napríklad logické vyplývanie (LV):
Ak prší, je zlé počasie.
Prší.
----------------------------------------------
Je zlé počasie.
je vo forme dedukcie.
Dedukčný kalkul logiky je konečná množina axióm a dedukčných pravidiel. V niektorej literatúre je označovaný ako dokazovací systém, alebo odvodzovací systém. Pomocou dedukčného kalkulu je možné dokázať formuly daného logického systému. Dokazovanie formuly v dedukčnom kalkule je proces, ktorý sa nazýva formálny dôkaz.
Axióma je tvrdenie, ktoré sa považuje za pravdivé a slúži ako predpoklad alebo východiskový bod pre ďalšie uvažovanie (odvodzovanie) a argumentáciu. Slovo pochádza zo starogréckeho slova ἀξίωμα (axíōma), čo znamená „to, čo sa považuje za evidentné“.
Dedukčné pravidlo (odvodzovacie pravidlo) je to logická forma pozostávajúca z funkcie, ktorá berie premisy, analyzuje ich syntax a vracia záver (alebo závery). Vo všeobecnosti má tvar: \begin{prooftree} \AxiomC{Predpoklad 1,} \AxiomC{...,} \AxiomC{Predpoklad n} \RightLabel{ (Názov Pravidlá)} \TrinaryInfC{Záver} \end{prooftree}
- Zápis vyššie je možné prečítať nasledovane: "ak platia všetky tvrdenia nad čiarou (predpoklad 1, ..., predpoklad n), potom platí záver".
- Dedukčné pravidlo môže mať jeden alebo viac predpokladov, ale aj žiaden.
- Pravidlo bez predpokladov je axióma.
- Dedukčné pravidlá sú schémy, v ktorých je možné za $φ, ψ, θ$ dosadiť ľubovoľné formuly.
Formálny dôkaz je konečná postupnosť viet (v prípade logiky sú to formuly), z ktorých každá je axiómou, predpokladom alebo je odvodená z predchádzajúcich viet pomocou dedukčného pravidla. Od idiomatického dôkazu pomocou prirodzeného jazyka sa formálny dôkaz líši tým, že je rigorózny, jednoznačný a mechanicky overiteľný.
Dokázateľnosť formuly $φ$ v dedukčnom systéme sa označuje $$\vdash φ.$$
Dokázateľnosť formuly $φ$ z množiny predpokladov $Γ$ v dedukčnom systéme sa označuje $$Γ \vdash φ,$$ kde $Γ$ je množina predpokladov (premisy) v tvare: $φ_1, ..., φ_n$.
Axiómy sú tautológie. Z tautológií je konštruovaný axiomatický systém tak, aby bol:
- konzistentný (bezosporný), axiómy si nesmú odporovať,
- úplný, musí obsahovať všetky axiómy potrebné pre dôkazy tvrdení v danom logickom systéme,
- nezávislý, nesmie obsahovať axiómy, ktoré sa dajú dokázať z iných axióm.
Konzistentnosť a úplnosť dedukčného kalkulu (Soundness and Completeness)
- Konzistentnosť voči sémantike logického systému. Ak v dedukčnom kalkule je formula $\varphi$ dokázateľná z množiny predpokladov $Γ$, potom formula $φ$ vyplýva z množiny predpokladov $Γ$ vzhľadom na definovanú sémantiku daného logického systému: $$\text{ak} \quad Γ \vdash φ, \quad \text{potom}~ \quad Γ \models φ.$$
- Úplnosť voči dedukčnému kalkulu logického systému. Ak formula $φ$ vyplýva z množiny predpokladov $Γ$ vzhľadom na definovanú sémantiku daného logického systému, potom v dedukčnom kalkule je formula $\varphi$ dokázateľná z množiny predpokladov $Γ$. $$\text{ak} \quad Γ \models φ, \quad \text{potom}~ \quad Γ \vdash φ.$$
- Dedukčný kalkul je konzistentný a úplný (silná forma vety) ak platí: $$Γ \models φ \quad \text{vtt.}~ \quad Γ \vdash φ.$$
Inými slovami a zjednodušene, ak je formula tautológia vzhľadom na definíciu sémantiky v danom logickom systéme, potom musí byť aj dokázateľná v jeho dedukčnom kalkule a vice versa. To hovorí slabá veta forma vety konzistentnosti a úplnosti dedukčného kalkulu: $$\models φ \quad \text{vtt.}~ \quad \vdash φ.$$
Poznámka
$~$
- Konzistentnosť - každá dokázateľná formula musí byť tautológia.
- Úplnosť - každá tautológia musí byť dokázateľná.
Veta o dedukcii hovorí $$Γ \vdash φ ⇒ ψ \quad \text{vtt.}\quad Γ ∪ φ \vdash ψ.$$
Príklad
Logické vyplývanie (LV) z príkladu vyššie je možné preložiť do formuly VL nasledovne:
- Prší označíme $p$.
- Zlé počasie označíme $z$.
Potom (LV) je možné vyjadriť ako $$p ⇒ z, p \vdash z.$$ Zároveň môžeme zaviesť množinu predpokladov $Γ = \{p ⇒ z, p\}$ a zápis zjednodušiť na: $$Γ \vdash z.$$
Poznámka
Dedukčné kalkuly sú vytvorené na dokazovanie formúl. Možno ich považovať za "dokazovací stroj", ktorého výsledkom sú dokázateľné formuly. Takýto stroj je definovaný konečnou množinou dedukčných pravidiel. Dedukčné pravidlá opisujú spôsob ako je možné transformovať formuly v rámci systému, pričom axiómy slúžia ako počiatočné body. Proces takejto transformácie je formálny dôkaz, ktorý je možné načrtnúť nasledovne:
Axiómy
↓↓↓
Dedukčné pravidlá aplikované na axiómy
↓↓↓
Dokázateľné formuly
↓↓↓
Dedukčné pravidlá aplikované na dokázateľné formuly
↓↓↓
Nové dokázateľné formuly
↓↓↓
... a pod. ...
Prirodzená dedukcia
V tridsiatych rokoch minulého storočia vyvinul Gerhard Gentzen dedukčný kalkul, ktorého cieľom bolo napodobniť prirodzený spôsob ľudského uvažovania. Pojem „natürliches Schließen“, ktorý v preklade znamená „prirodzená dedukcia“ (v niektorej literatúre označovaná aj ako naturálna dedukcia), zaviedol vo svojej dizertačnej práci. Tento dôkazový kalkul sa často označuje ako NK (z nemeckého “Natürliche Kalkül”).
Prirodzená dedukcia je:
- konzistentná a úplná,
- má menej axióm a viac dedukčných pravidiel,
- dôkaz formuly sa konštruuje odzadu, od dokazovanej formuly.
Dôkaz v prirodzenej dedukcii:
- Je dôkazový strom.
- V koreni stromu sa nachádza dokazovaná formula.
- Konštruuje sa od koreňa k listom.
- Každý krok dôkazu vznikol aplikovaním vhodného dedukčného pravidla.
- Každý krok dôkazu je oddelený horizontálnou čiarou.
- Ak sú všetky listy stromu hypotézy, dôkaz formuly je skonštruovaný.
Hypotéza (predpoklad):
- V dôkaze sa zavádzajú hypotézy aplikovaní určitých pravidiel.
- Zavedenie hypotézy v pravidle symbolizujú vertikálne bodky ⋮ a vytvorená hypotéza sa nachádza nad bodkami v hranatých zátvorkách $[φ]$.
- Vzniknuté hypotézy sa zapisujú mimo dôkazového stromu a označujú sa malými písmenami latinskej abecedy v tvare $a=[φ]$.
- Ak pri konštrukcii dôkazového stromu po aplikovaní príslušného pravidla vzniká hypotéza, potom pri názve pravidla sa uvádza ako horný index názov hypotézy.
- V prípade, že je potrebné dokázať tvrdenie v tvare $Γ \vdash φ$, dokazuje sa len formula $φ$ a všetky formuly z množiny predpokladov sú hypotézy.
Dedukčné pravidlá
Dedukčné pravidlá naturálnej dedukcie delíme do dvoch skupín:
- uvádzacie (I - introducing) - zavedú v svojom závere určitú logickú spojku, poskytujú dôvod, príčinu formuly,
- eliminujúce (E - eliminating) - odstránia v svojom závere určitú logickú spojku, dedukujú záver, dôsledok.
Konštanty
Negácia
Konjunkcia
Disjunkcia
Implikácia
Príklad
Príklad
Prostredníctvom prirodzenej dedukcie dokážte tranzitivitu implikácie: $$(\varphi \Rightarrow \psi) \wedge (\psi \Rightarrow \theta) \Rightarrow (\varphi \Rightarrow \theta).$$
Riešenie
Dôkaz v prirodzenej dedukcii je dôkazový strom, kde v koreni sa nachádza dokazovaná formula. Postup je nasledovný:
- Prepísanie formuly do koreňa stromu a na základe štruktúry formuly aplikácia vhodného dedukčného pravidla (pozor na prioritu a asociativitu operátorov).
- Aplikácia pravidla pre zavedenie implikácie, na základe toho vznikla hypotéza $a$.
Aktuálne hypotézy: $a=[(φ⇒ψ)∧(ψ⇒θ)]$.
- Opätovná aplikácia pravidla pre zavedenie implikácie, na základe toho vznikla hypotéza $b$.
Aktuálne hypotézy: $a=[(φ⇒ψ)∧(ψ⇒θ)]$, $\quad b=[φ]$.
- V tomto stave formula neobsahuje logické spojky, to znamená je potrebné použiť niektoré pravidlo pre elimináciu. V tomto prípade je vhodné aplikovať pravidlo pre elimináciu implikácie, ktoré rozvetví strom na dve vetvy:
Aktuálne hypotézy: $a=[(φ⇒ψ)∧(ψ⇒θ)]$, $\quad b=[φ]$.
- V tomto prípade je potrebné zvoliť konkrétnu vetvu, napr. ľavú. V ľavej vetve formula neobsahuje logické spojky. Opäť je potrebné aplikovať pravidlo pre elimináciu spojky. Aplikácia pravidla pre elimináciu implikácie, ktoré danú vetvu rozvetví na dve vetvy.
Poznámka: nezáleží na tom, ktorou vetvou sa rozhodneme pokračovať, je potrebné uzavrieť všetky.
Aktuálne hypotézy: $a=[(φ⇒ψ)∧(ψ⇒θ)]$, $\quad b=[φ]$.
- Ľavá vetva. Formula $φ$ je hypotéza $b$. Táto vetva je korektne uzavretá.
Aktuálne hypotézy: $a=[(φ⇒ψ)∧(ψ⇒θ)]$, $\quad b=[φ]$.
- Pravá vetva. Aplikácia pravidla pre elimináciu konjunkcie, tak aby vznikla hypotéza. Formula $(φ⇒ψ)⇒(ψ⇒θ)$ je hypotéza $a$. Táto vetva je korektne uzavretá.
Aktuálne hypotézy: $a=[(φ⇒ψ)∧(ψ⇒θ)]$, $\quad b=[φ]$.
- Návrat v strome o úroveň nižšie a pokračovanie otvorenou pravou vetvou. Aplikácia pravidla pre elimináciu konjunkcie, tak aby vznikla hypotéza. Formula $(φ⇒ψ)⇒(ψ⇒θ)$ je hypotéza $a$. Táto vetva je korektne uzavretá.
Aktuálne hypotézy: $a=[(φ⇒ψ)∧(ψ⇒θ)]$, $\quad b=[φ]$.
- Záver: všetky vetvy stromu sú hypotézy, formula v koreni je dokázaná.
Sekventový kalkul
V roku 1935 Gerhard Gentzen formuloval ďalší dedukčný systém s názvom sekventový kalkul, niekedy nazývaný aj systém LK (“Logistiche Kalkül”). Základom tohto kalkulu je štruktúra s názvom sekvent.
Sekvent je dvojica konečných množín formúl $Γ, Δ$ v tvare: $$Γ ⊢ Δ,$$ ktorú je možné prečítať nasledovne: "ak platia všetky formuly z $Γ$, potom platí aspoň jedna formúl z $Δ$", kde:
- $⊢$ sa nazýva turniket, nie je to logický symbol ale metasymbol jazyka, oddeľuje pravú a ľavú stranu sekventu,
- $Γ$ sa nazýva antecedent (predpoklady),
- $Δ$ sa nazýva sukcedent (záver).
Taktiež platí:
- $Γ, Δ$ môžu byť prázdne množiny,
- Ak $Γ= φ_1 ∧ ... ∧ φ_n$, potom $$Γ,ψ$$ znamená, že množina predpokladov $Γ$ je rozšírená o formulu $ψ$.
- Zápis $$Γ⊢$$ znamená, že množina predpokladov je sporná.
Zápis $Γ ⊢ Δ$ je možné prepísať do formy: $$φ_1,...,φ_n ⊢ ψ_1,...,ψ_m,$$ pričom pre získanie ekvivalentného zápisu je možné na ľavej strane za čiarku substituovať konjunkciu a na strane pravej disjunkciu: $$φ_1 ∧ ... ∧ φ_n ⊢ ψ_1 ∨ ... ∨ ψ_m.$$
Poznámka
$\\$
Na základe vety o dedukcii je možné si symbol $⊢$ predstaviť ako implikáciu, avšak zápisy $φ⊢ψ$ a $φ⇒ψ$ nie sú ekvivalentné!
Existujú dva typy sekventového kalkulu:
- obojstranný sekventový kalkul (vyššie definovaný, budeme využívať v rámci cvičení),
- pravostranný sekventový kalkul, ktorý má všetky formuly na pravej strane sekventu (formuly je možné presúvať z jednej strany na druhú pomocou negácie).
Dôkaz v sekventovom kalkule je dôkazový strom, pričom:
- Uzly stromu sú sekventy.
- Koreň stromu je dokazovaný sekvent.
- Dôkaz začína od koreňa stromu.
- Každý krok dôkazu je aplikovanie vhodného dedukčného pravidla.
- Sekvent je dokázaný (skonštruovali sme dôkaz sekventu), ak listy stromu sú axiómy.
Dedukčné pravidlá majú štandardný tvar (definovaný vyššie), avšak na rozdiel od naturálnej dedukcie, tvrdenia nie sú formuly ale jednotlivé sekventy. Je možné ich rozdeliť na 3 kategórie:
- Pravidlo identity a rezu.
- Logické pravidlá - zavádzajú novú logickú spojku v závere.
- Štrukturálne pravidlá - manipulujú so štruktúrou sekventu.
Pravidlo identity a rezu:
| \begin{prooftree} \AxiomC{ } \RightLabel{ (id)} \UnaryInfC{Γ, φ ⊢ Δ, φ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Λ, φ} \AxiomC{φ, Δ ⊢ Σ} \RightLabel{ (cut)} \BinaryInfC{Γ, Δ ⊢ Λ, Σ} \end{prooftree} |
|---|
Logické pravidlá:
Negácia
| \begin{prooftree} \AxiomC{Γ ⊢ Δ, φ} \RightLabel{ (¬l)} \UnaryInfC{Γ, ¬φ ⊢ Δ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ, φ ⊢ Δ} \RightLabel{ (¬r)} \UnaryInfC{Γ ⊢ Δ, ¬φ} \end{prooftree} |
|---|
Konjunkcia
| \begin{prooftree} \AxiomC{Γ, φ ⊢ Δ} \RightLabel{ (∧l1)} \UnaryInfC{Γ, φ ∧ ψ ⊢ Δ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ, ψ ⊢ Δ} \RightLabel{ (∧l2)} \UnaryInfC{Γ, φ ∧ ψ ⊢ Δ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Δ, φ} \AxiomC{Γ ⊢ Δ, ψ} \RightLabel{ (∧r)} \BinaryInfC{Γ ⊢ Δ, φ ∧ ψ} \end{prooftree} |
|---|
Disjunkcia
| \begin{prooftree} \AxiomC{Γ ⊢ Δ, φ} \RightLabel{ (∨r1)} \UnaryInfC{Γ ⊢ Δ, φ ∨ ψ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Δ, ψ} \RightLabel{ (∨r2)} \UnaryInfC{Γ ⊢ Δ, φ ∨ ψ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ, φ ⊢ Δ} \AxiomC{Γ, ψ ⊢ Δ} \RightLabel{ (∨l)} \BinaryInfC{Γ, φ ∨ ψ ⊢ Δ} \end{prooftree} |
|---|
Implikácia
| \begin{prooftree} \AxiomC{Γ, φ ⊢ Δ, ψ} \RightLabel{ (⇒r)} \UnaryInfC{Γ ⊢ Δ, φ ⇒ ψ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Λ, φ} \AxiomC{Δ, ψ ⊢ Σ} \RightLabel{ (⇒l)} \BinaryInfC{Γ,Δ φ ⇒ ψ ⊢ Λ, Σ} \end{prooftree} |
|---|
Konštanty
| \begin{prooftree} \AxiomC{Γ ⊢ Δ} \RightLabel{ (⊥r)} \UnaryInfC{Γ ⊢ Δ, ⊥} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Δ} \RightLabel{ (⊤r)} \UnaryInfC{Γ ⊢ Δ, ⊤} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Δ} \RightLabel{ (⊤l)} \UnaryInfC{Γ, ⊤ ⊢ Δ} \end{prooftree} |
|---|
Štrukturálne pravidlá:
Pravidlá zoslabenia
| \begin{prooftree} \AxiomC{Γ ⊢ Δ} \RightLabel{ (wl)} \UnaryInfC{Γ, φ ⊢ Δ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Δ} \RightLabel{ (wr)} \UnaryInfC{Γ ⊢ Δ, φ} \end{prooftree} |
|---|
Pravidlá kontrakcie
| \begin{prooftree} \AxiomC{Γ, φ, φ ⊢ Δ} \RightLabel{ (cl)} \UnaryInfC{Γ, φ ⊢ Δ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Δ, φ, φ} \RightLabel{ (cr)} \UnaryInfC{Γ ⊢ Δ, φ} \end{prooftree} |
|---|
Pravidlá výmeny
| \begin{prooftree} \AxiomC{Γ, ψ, φ ⊢ Δ} \RightLabel{ (exl)} \UnaryInfC{Γ, φ, ψ ⊢ Δ} \end{prooftree} | \begin{prooftree} \AxiomC{Γ ⊢ Δ, ψ, φ} \RightLabel{ (exr)} \UnaryInfC{Γ ⊢ Δ, φ, ψ} \end{prooftree} |
|---|
Príklad
Príklad
Sekventovým kalkulom, dokážte formulu: $$φ ⇒ (ψ ⇒ (φ ∧ ψ))$$
Riešenie
Dôkaz v sekventovom kalkule je dôkazový strom, kde v koreni sa nachádza sekvent, ktorý obsahuje dokazovanú formulu. Postup je nasledovný.
- Prepísanie formuly do tvaru sekventu a jej vloženie do koreňa stromu. Na základe štruktúry formuly sa aplikuje vhodné dedukčné pravidlo (pozor na prioritu a asociativitu operátorov).
- Aplikácia pravidla pre implikáciu na pravej strane, ktoré presunie predpoklad implikácie na ľavú stranu sekventu.
- Opätovná aplikácia pravidla pre implikáciu na pravej strane.
- Aplikácia pravidla pre konjunkciu na pravej strane, ktoré spôsobí rozvetvenie stromu.
Poznámka: V tomto kroku v oboch vetvách je možné aplikovať pravidlo identity, tým uzavrieť obe vetvy a ukončiť dôkaz. Avšak z dôvodu demonštrácie použitia štrukturálnych pravidiel pokračujeme v dokazovaní.
- Ľavá vetva: aplikácia pravidla oslabenia na ľavej strane (odstránenie formulu $ψ$).
- Pravá vetva: aplikácia pravidla zámeny na ľavej strane (príprava sekventu do tvaru aby v ďalšom kroku bolo možné odstránenie formuly $φ$).
- Ľavá vetva: aplikácia pravidla identity, vetva je uzavretá.
- Pravá vetva: aplikácia pravidla oslabenia na ľavej strane (odstránenie formuly $φ$). Následnou aplikáciu pravidla identity je vetva uzavretá.
Záver: všetky vetvy stromu obsahujú identity, sú uzavreté, sekvent v koreni je dokázaný.
Postup
Krok 1: Pokúste sa dokázať nasledujúce formuly prostredníctvom prirodzenej dedukcie a v sekventovom kalkule
Úloha 1.1
$$ φ ⇒ φ $$
Úloha 1.2
$$ φ ⇒ ¬¬φ $$
Úloha 1.3
$$ φ ⇒ (φ ∧ ψ) $$
Úloha 1.4
$$ (φ ⇒ ψ) ⇒ (¬ φ ⇒ ¬ψ) $$
Úloha 1.5
$$ (φ ⇒ (ψ⇒θ)) ⇒ ((φ ∧ ψ) ⇒θ)) $$
Úloha 1.6
$$ φ~∨ ⊥ ⇒ φ~∧ ⊤ $$
Úloha 1.7
$$ (φ ∨ ψ) ⇒ (¬φ ⇒ ψ) $$
Krok 2: Prepíšte nasledujúce tvrdenia v prirodzenom jazyku do formúl výrokovej logiky a pokuste sa ich dokázať prirodzenou dedukciou a sekventovým kalkulom.
Úloha 2.1
Ak mám peniaze, tak si kúpim auto.
Peniaze mám.
----------------------------------------------
Kúpim si auto.
Úloha 2.2
Ak je Svätopluk učiteľ, tak je múdry.
Svätopluk je múdry.
----------------------------------------------
Svätopluk je učiteľ.
Úloha 2.3
Ak je zamračené a nezoberiem si dáždnik, zmoknem.
Nezoberiem si dáždnik.
----------------------------------------------
Zmoknem.
Úloha 2.4
Budem inžinier z informatiky ak urobím skúšku.
Urobím skúšku ak urobím zápočet
Urobím zápočet ak nebudem lenivý.
----------------------------------------------
Budem inžinier ak nebudem lenivý.
Úloha 2.5
Ak budem veľa cestovať, tak navštívim veľa krajín.
Ak navštívim veľa krajín, tak spoznám veľa ľudí.
Ak spoznám veľa ľudí, tak budem mať veľa priateľov.
----------------------------------------------
Ak budem veľa cestovať, budem mať veľa priateľov.
Úloha 2.6
Ak sa Argentína pripojí k aliancii, potom Brazília alebo Chile ju budú bojkotovať.
Ak sa Ekvádor pripojí k aliancii, potom Chile alebo Peru ju budú bojkotovať.
Chile nebojkotuje alianciu.
----------------------------------------------
Ak ani Brazília ani Peru nebojkotujú alianciu, tak sa ani Argentína ani Ekvádor nepripoja k aliancii.