04. Rachunek zdań - dedukcja

 

1. Naturalna dedukcja

Wprowadzimy system naturalnej dedukcji i związane z nim reguły dedukcyjne, dzieki czemu nadamy formalne ramy dowodom w rachunku zdań. Zrobimy to w taki sposób, żeby nasze dowody istotnie można było zaprezentować w sposób zrozumiały dla komputera (będzie to też Państwa zadanie w ramach punktowanych zadań dodatkowych). Poniżej podejmiemy pewne decyzje odnośnie wyglądu dowodów, jednak inne postacie też są dopuszczalne i wykorzystywane w konstrukcji dowodów. Należy zatem potraktować poniższe zasady jako umowę ważną na czas wykładu ze Wstępu do Matematyki. W przyszłości mogą się Państwo stykać z innymi zestawami reguł dowodzenia, w szczególności w konstruktywnym podejściu do matematyki niektóre z poniższych reguł muszą być usuniętę.

Podobny system dedukcyjny można zbudować dla innych, bardziej złożonych logik, na przykład dla arytmetyki Peano, teorii zbiorów, albo dla geometrii Euklidesowej sformalizowanej w duchu Hilberta lub Tarskiego. Koncentrujemy się jednak na przypadku rachunku zdań, gdyż jest to bardzo prosta i użyteczna logika. W ramach tego wykładu sformalizowane dowody w innych logikach pojawiają się wyłącznie w materiale dodatkowym.

2. Sekwenty i reguły dedukcyjne

2.1. Sekwenty

(1)
\[\phi_1,\ldots,\phi_n\vdash \psi 
\]

Ten napis oznacza, że z przesłanek $\phi_1,\ldots,\phi_n$ chcemy wyprowadzić wniosek $\psi$. Powyższy napis nazyway sekwentem i mówimy, że jest poprawny, jeśli istotnie można znaleźć dowód $\psi$.

Zasady dowodzenia to będą pewne mechaniczne kroki, które może legalnie stosować. Większość reguł ma charakter oczywisty, jednak dobranie ich we właściwej kolejności może stanowić dość poważne wyzywanie intelektualne i z całą pewnościa stanowi wyzywanie obliczeniowe. Z drugiej strony reguły są na tyle proste, że jeżeli stosuje się je bez przeskoków, to weryfikacja jest kompletnie banalna. Można to porównać do skomplikowanego zadania szachowego, gdzie wykonanie krytycznego ruchu może wymagać mistrzowskiej intuicji, natomiast nawet początkujący gracz z łatwościa może stwierdzić, czy ruch był poprawny.

2.2. Wprowadzenie i eliminacje koniukcji

Przy pomocy reguły wprowadzającej implikację

(2)
\[\infer[\mathrm{\wedge i}]{\phi\wedge \psi}{\phi & \psi}
\]

oraz dwóch reguł eliminujących implikację

(3)
\[\infer[\mathrm{\wedge e_1}]{\phi}{\phi \wedge \psi},\  
\infer[\mathrm{\wedge e_2}]{\psi}{\phi \wedge \psi}
\]

wykażemy, że sekwent

(4)
\[p \wedge q, r\vdash q\wedge r
\]

jest poprawny. W pierwszym momencie może się wydawać, że jest to zupełnie oczywiste i faktycznie dowód jest bardzo prosty, ale w świecie formalnych rozumowań konieczne jest przedstawienie precyzyjnej argumentacji uzasadniającej poprawność sekwentu.

  1. $p \wedge q$— założenie
  2. $r$— założenie
  3. $q$ — uzyskujemy z zastosowania reguły $\wedge e_2$ do wiersza 1.
  4. $q\wedge r$ — uzyskujemy z zastosowania $\wedge i$ do wierszy 3 i 2.

Innym sposobem przedstawienia dowodu formalnego jest zapisanie go jako drzewa

\begin{prooftree}
\AxiomC{$p\wedge q$}
\RightLabel{$\wedge e_2$}
\UnaryInfC{$q$}
\AxiomC{$r$}
\RightLabel{$\wedge i$}
\BinaryInfC{$q\wedge r$}
\end{prooftree}

2.3. Wprowadzenie i eliminacja alternatywy

Reguły wprowadzające alternatywę wyglądają następująco:

(5)
\[\infer[\mathrm{\vee i_1}]{\phi \vee \psi}{\phi},\  
\infer[\mathrm{\vee i_2}]{\phi \vee \psi}{\psi}
\]

Reguła eliminująca alternatywę przedstawia się w sposób nieco bardziej skomplikowany:

(6)
\[\infer[\mathrm{\vee e}]{\chi}{\phi \vee \psi\ \infer*{\chi}{\phi}\ \infer*{\chi}{\psi}}
\]

Zasadę tą trzeba rozumieć następująco. Jeśli uda nam się zarówno z $\phi$ jak i z $\psi$ wyprowadzić wspólny wniosek $\chi$, to alternatywę $\phi\vee \psi$ możemy wyelimonować, zastępując ją $\chi$.

2.4. Wprowadzenie i eliminacja podwójnej negacji

Reguła wprowadzające podwójną negację wyglądają następująco:

(7)
\[\infer[\mathrm{\neg\neg i}]{\neg\neg\phi}{\phi}
\]

Reguła eliminująca podwójną negację wyglądają następująco:

(8)
\[\infer[\mathrm{\neg\neg e}]{\phi}{\neg\neg \phi}
\]

2.5. Wprowadzenie i eliminacja implikacji

2.5.1. Eliminacja implikacji

(9)
\[\infer[\mathrm{\to e}]{\psi}{\phi & \phi \to \psi}
\]

2.5.2. Wprowadzanie implikacji

Do tej pory rozważane zasady, które nie zwiększaja liczby implikacji. Podobnie żadna z powyższych reguł nie pozwala na modyfikowanie istniejącej implikacji.

(10)
\[\infer[\mathrm{\to i}]{\psi\to \phi}{\infer*{\phi}{\psi}}
\]

Powyższa reguła oznacza, że dowód $\phi$ z $\psi$ możemy zastąpić implikacją $\psi\to\phi$.

2.6. Pojęcie sprzeczności- reguła eliminująca sprzeczność

W rachunku symbol $\bot$ rezerwujemy na zdania sprzeczne. Jednynym źródłem zdań sprzecznych będzie reguła eliminująca negację, która wprowadzimy w następnym punkcie. Tymczasem dodajemy regułe, że ze sprzeczności można wyprowadzić dowolne inne zdanie

(11)
\[\infer[\mathrm{\bot e}]{\phi}{\bot}
\]

2.7. Wprowadzenie i eliminacja negacji

2.7.1. Eliminacja negacji

(12)
\[\infer[\mathrm{\neg e}]{\bot}{\phi & \neg \phi}
\]

2.7.2. Wprowadzanie negacji

Do tej pory rozważane zasady, które nie wprowadzały negacji. Dodamy zasadę, że przed formułą $\phi$ można postawić $\neg$, jeśli z $\phi$ można wyprowadzić sprzeczność.

(13)
\[\infer[\mathrm{\neg i}]{\neg\phi}{\infer*{\phi}{\bot}}
\]

2.8. Podsumowanie reguł dedukcyjnych

rach_rules


Figure 1. Podsumowanie reguł dedukcyjnych.

2.9. Przykłady rozumowań w rachunku zdań

Posługując się do tej pory zgromadzonymi zasadami udowodnimy wzmiankowane na powyższym obrazku reguły pochodne.

2.9.1. Modus tolens

(14)
\[\infer[MT]{\neg\phi}{\phi\to\psi & \neg\psi}
\]
  1. $\phi \to \psi$— założenie
  2. $\neg \psi$—założenie
    • $\phi$ — założenie, dążymy do skorzystania z $\neg i$, tak więc wystarczy wykazać, że z $\phi$ można wyprowadzić $\bot$.
    • $\psi$ — uzyskujemy z zastosowania założenia $\phi$, założenia $\phi\to\psi$ i reguły $\to e$.
    • $\bot$ — uzyskujemy z zastosownia $\neg e$ do $\psi$ i $\neg \psi$.

Innym sposobem przedstawienia powyższego dowodu jest zapisanie go jako drzewa

\begin{prooftree}
\AxiomC{$\phi$}
\AxiomC{$\phi\to\psi$}
\RightLabel{$\to e$}
\BinaryInfC{$\psi$}
\AxiomC{$\neg \psi$}
\RightLabel{$\neg e$}
\BinaryInfC{$\bot$}
\RightLabel{$\neg i$}
\UnaryInfC{$\neg\phi$}
\end{prooftree}

2.10. Rozumowania sformalizowane na komputerze

Posługując się powyższymi zasadami podamy dwa cztery sformalizowne dowody w języku programowania Coq, a konkretnie w jego wersji Proofweb (dokumentacja Proofweb).

2.10.1. Modus Tolens

(* Sformalizowany dowód Modus Tolens *) Require Import ProofWeb. Variables p q : Prop. Theorem MT : ((p -> q) /\ ~q) -> ~p. Proof. imp_i H. neg_i H1. neg_e (q). con_e2 (p -> q). apply H. imp_e (p). con_e1 (~q). apply H. apply H1. Qed.

Komputer automatycznie generuje drzewo dowodu

drzewo_mt_coq


Figure 2. Drzewo dowodu wygenerowane przez Proofweb.

2.10.2. Prawo wyłączonego środka

Powyższa tabelka sugeruje, że prawo $p\vee \neg p$ jest twierdzeniem rachunku zdań wynikającym z uprzednio ustalonych zdań. Przyjrzyjmy się dowodowi na komputerze.

 (* Sformalizowany dowód Prawa Wyłączonego Środka aka Law of Excluded Middle = LEM aka Tertium non datur *) Require Import ProofWeb. Variable p : Prop. Theorem LEM : p \/ ~p. Proof. (* zamiast dowodzić p \/ ~p udowodnimy ~~ (p \/ ~p) *) negneg_e. (* w tym miejscu do naszych założen trafia ~(p \/ ~p) *) neg_i H. (* w tym miejscu rozumowanie rozbija sie nad dwa fragmenty widoczne w drzewie dowodowym *) neg_e (p \/ ~p). (* z pierwszym fragmentem radzimy sobie łatwo, bo dokładnie odpowiada naszemu założeniu H *) apply H. (* mając do wyboru wykazanie p \/ ~p decydujemy sie na ~p *) dis_i2. (* w tym miejscu trafia do naszych założen trafia H1 = p *) neg_i H1. (* musimy wykazać, że z H = ~(p \/ ~p) i H1 = p wynika sprzeczność *) (* w tym celu wykażemy, że zachodzi ~(p \/ ~p) i (p \/ ~p) *) neg_e (p \/ ~p). (* pierwszy krok jest łatwy - ~(p \/ ~p) jest równe założeniu H *) apply H. (* drugi krok polega uzyskaniu p \/ ~p z p poprzez wprowadzenie dyzjunkcji *) dis_i1. (* w tym miejscu wystarczy zastosować założenie H1 = p *) apply H1. Qed.

2.10.3. Inne przykłady

(* Cwiczenie 1 *) Require Import ProofWeb. Variables p q r : Prop. Theorem pred_001 : p /\ q -> p. Proof. imp_i H. con_e1 q. apply H. Qed.

Wczesniej uzyskany dowód $(p\wedge q), r\vdash q\wedge r$ możemy zapisać jako implikacje $(p\wedge q)\wedge r\to q\wedge r$ a następnie zaprogramować na komputerze w systemie Proofweb:

(* Cwiczenie 2 *) Require Import ProofWeb. Variables p q r : Prop. Theorem pred_002 : (p /\ q) /\ r -> q /\ r. Proof. imp_i H. con_i. con_e2 p. con_e1 r. apply H. con_e2 (p /\ q). apply H. Qed.
(* Cwiczenie 3 *) Require Import ProofWeb. Variables p q r : Prop. Theorem pred_003 : ((p /\ q) -> r) -> (p -> (q -> r)). Proof. imp_i H. imp_i H1. imp_i H2. apply H. con_i. apply H1. apply H2. Qed.
Created with Madoko.net.