Výroková logika - dedukčné kalkuly

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

Veta o dedukcii hovorí $$Γ \vdash φ ⇒ ψ \quad \text{vtt.}\quad Γ ∪ φ \vdash ψ.$$

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 uzavreté t. j. obsahujú iba hypotézy alebo axiómy (podľa použitej notácie), dôkaz formuly je skonštruovaný.

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.

Pri prezentácii pravidiel prirodzenej dedukcie je možné použiť dva ekvivalentné zápisy:

1. Notácia s implicitným kontextom – tradičná, používaná v základných učebniciach.
2. Notácia s explicitným kontextom – formálna, používaná v logických systémoch, kde sa sledujú všetky hypotézy (napr. v sekventovom kalkule alebo formálnych dokazovacích systémoch ako Rocq, Lean či Isabelle).

Obidve notácie opisujú ten istý dedukčný systém, líšia sa len v tom, ako zobrazujú množinu aktuálnych hypotéz (predpokladov).

Implicitný kontext

V notácii s implicitným kontextom sa množina hypotéz (predpokladov) nezapisuje pri každom kroku dôkazu.
Predpokladá sa, že každý krok využíva iba hypotézy, ktoré sa nachádzajú v aktuálnom dôkazovom strome.
Zápisy sú kompaktnejšie a vhodné pre výučbu alebo ilustráciu princípu dokazovania.

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 aplikácii 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.

V procese konštrukcie dôkazového stromu je potrebné sledovať, ktoré hypotézy sú aktuálne v danom kroku dôkazu. Dôkaz je korektný, ak každá vetva stromu obsahuje iba hypotézy, ktoré vznikli v danej vetve alebo v jej podvetvách.

Je potrebné si uvedomiť, že dedukčné pravidlá je možné intuitívne chápať nasledovne:

• Predpoklady (nad čiarou) sú formuly ktoré sú v konjunkcii. To znamená, že všetky predpoklady musia platiť, aby platil záver.
• Záver (pod čiarou) je dôsledok, výsledok, ktorý vyplýva z predpokladov.

Napríklad pravidlo: $$ \begin{prooftree} \AxiomC{φ} \AxiomC{φ ⇒ ψ} \RightLabel{(Modus ponens)} \BinaryInfC{ψ} \end{prooftree} $$ je ekvivalentné s formulou: $$ \varphi \wedge (\varphi \Rightarrow \psi) \Rightarrow \psi. $$

Pravidlá s implicitným kontextom

Konštanty

Negácia

Konjunkcia

Disjunkcia

Implikácia

Zhrnutie všetkých pravidiel s implicitným kontextom:

Príklad

Explicitný kontext

V notácii s explicitným kontextom sa v každom kroku dôkazu zapisuje aj množina hypotéz (kontext), t. j. množina všetkých formúl, z ktorých daná formula vyplýva.
Táto forma je bližšia sekventovému kalkulu (ďalšia kapitola), pretože používa zápis $ Γ ⊢ φ $, kde $ Γ $ je množina hypotéz (predpokladov).

Pravidlá s explicitným kontextom

Axióma $$ \begin{prooftree} \AxiomC{φ ∈ Γ} \RightLabel{(Ax)} \UnaryInfC{Γ ⊢ φ} \end{prooftree} $$

Konštanty $$ \begin{prooftree} \AxiomC{Γ ⊢ ⊥} \RightLabel{(⊥E₁)} \UnaryInfC{Γ ⊢ φ} \end{prooftree} \quad\quad \begin{prooftree} \AxiomC{Γ,¬φ ⊢ ⊥} \RightLabel{(⊥E₂)} \UnaryInfC{Γ ⊢ φ} \end{prooftree} \quad\quad \begin{prooftree} \AxiomC{ } \RightLabel{(⊤I)} \UnaryInfC{Γ ⊢ ⊤} \end{prooftree} \quad\quad $$

Negácia $$ \begin{prooftree} \AxiomC{Γ, φ ⊢ ⊥} \RightLabel{(¬I)} \UnaryInfC{Γ ⊢ ¬φ} \end{prooftree} \quad\quad \begin{prooftree} \AxiomC{Γ ⊢ φ} \AxiomC{Γ ⊢ ¬φ} \RightLabel{(¬E)} \BinaryInfC{Γ ⊢ ⊥} \end{prooftree} $$

Konjunkcia $$ \begin{prooftree} \AxiomC{Γ ⊢ φ} \AxiomC{Γ ⊢ ψ} \RightLabel{(∧I)} \BinaryInfC{Γ ⊢ φ ∧ ψ} \end{prooftree} \quad\quad \begin{prooftree} \AxiomC{Γ ⊢ φ ∧ ψ} \RightLabel{(∧E₁)} \UnaryInfC{Γ ⊢ φ} \end{prooftree} \quad \begin{prooftree} \AxiomC{Γ ⊢ φ ∧ ψ} \RightLabel{(∧E₂)} \UnaryInfC{Γ ⊢ ψ} \end{prooftree} $$

Disjunkcia $$ \begin{prooftree} \AxiomC{Γ ⊢ φ} \RightLabel{(∨I₁)} \UnaryInfC{Γ ⊢ φ ∨ ψ} \end{prooftree} \quad \begin{prooftree} \AxiomC{Γ ⊢ ψ} \RightLabel{(∨I₂)} \UnaryInfC{Γ ⊢ φ ∨ ψ} \end{prooftree} \quad \begin{prooftree} \AxiomC{Γ ⊢ φ ∨ ψ} \AxiomC{Γ, φ ⊢ θ} \AxiomC{Γ, ψ ⊢ θ} \RightLabel{(∨E)} \TrinaryInfC{Γ ⊢ θ} \end{prooftree} $$

Implikácia $$ \begin{prooftree} \AxiomC{Γ, φ ⊢ ψ} \RightLabel{(⇒I)} \UnaryInfC{Γ ⊢ φ ⇒ ψ} \end{prooftree} \quad\quad \begin{prooftree} \AxiomC{Γ ⊢ φ ⇒ ψ} \AxiomC{Γ ⊢ φ} \RightLabel{(⇒E)} \BinaryInfC{Γ ⊢ ψ} \end{prooftree} $$

Porovnanie

Príklad

Majme danú nasledujúcu formulu $$(a \Rightarrow b) \wedge (b \Rightarrow c) \Rightarrow a \Rightarrow c$$ Dokážte túto formulu prostredníctvom prirodzenej dedukcie s notáciou s explicitným kontextom. Riešenie:

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

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:

Logické pravidlá:

Negácia

Konjunkcia

Disjunkcia

Implikácia

Konštanty

Štrukturálne pravidlá:

Pravidlá zoslabenia

Pravidlá kontrakcie

Pravidlá výmeny

Príklad

Záver – Prečo dva dôkazové systémy?

V tejto prednáške boli zavedené dva formálne dokazovacie systémy:

• Prirodzená dedukcia (ND)
• Sekventový kalkul (SK)

Oba systémy dokazujú tie isté formuly, ale používajú odlišný pohľad na dôkaz.

Prirodzená dedukcia

• Modeluje spôsob, akým uvažuje človek.
• Pracuje s hypotézami a ich postupným „uzatváraním“.
• Je vhodná pre manuálne konštruovanie dôkazov.

Prirodzená dedukcia odpovedá na otázku:
Ako by sme tento dôkaz napísali ako matematickú argumentáciu?

Sekventový kalkul

• Modeluje dôkaz ako formálnu štruktúru.
• Pracuje explicitne s kontextom na oboch stranách sekventu.
• Je vhodný pre algoritmické a automatické dokazovanie.

Sekventový kalkul odpovedá na otázku:
Ako môže dôkaz konštruovať alebo analyzovať stroj?

Metateoretický pohľad

Platí zásadný výsledok:

$$ \Gamma \vdash_{ND} \varphi \quad \text{vtedy a len vtedy, keď} \quad \Gamma \vdash_{SK} \varphi. $$

Oba systémy sú teda ekvivalentné vzhľadom na dokázateľnosť.

V sekventovom kalkule navyše platí veta o eliminácii rezu (cut-elimination), ktorá zaručuje, že dôkazy je možné normalizovať a systém je konzistentný.

Zhrnutie

Je potrebné si uvedomiť, že:

• Sémantika určuje, čo je pravdivé.
• Dedukčné systémy určujú, čo je dokázateľné.
• Prirodzená dedukcia je bližšia ľudskému uvažovaniu.
• Sekventový kalkul je bližší algoritmickému spracovaniu.
• Obe formy sú formálne ekvivalentné.