Logika dla informatyków/Paradygmaty dowodzenia

Paradygmaty dowodzenia

Sprawdzenie, czy dana formuła rachunku zdań jest tautologią, polega zwykle na obliczeniu jej wartości dla $\displaystyle 2^{n}$ różnych wartościowań, gdzie $\displaystyle n$ jest liczbą zmiennych zdaniowych tej formuły. Jak dotąd nie są znane radykalnie szybsze metody. Dla rachunku predykatów nie istnieje w ogóle żaden algorytm sprawdzania czy dana formuła jest tautologią (Twierdzenie 3.8). W obu przypadkach istnieją jednak metody dowodzenia pozwalające na wyprowadzanie prawdziwych formuł za pomocą ustalonych procedur syntaktycznych.

Każdy system dowodzenia zawiera dwa składniki:

• początkowy zbiór formuł (lub wyrażeń zbudowanych z wielu formuł) zwanych aksjomatami;
• zbiór operacji przekształcających wyrażenia w wyrażenia - operacje te są nazywane regułami dowodzenia.

Reguły dowodzenia opisują warunki, przy pomocy których można otrzymać nowe wyrażenie (nazywane konkluzją) z otrzymanych już wyrażeń (nazywanych przesłankami). Dowody w systemach formalnych są ciągami wyrażeń, być może posiadającymi dodatkową strukturę pozwalającą na lepszą wizualizację.

W dalszej części opiszemy trzy systemy dowodzenia: system typu hilbertowskiego (od nazwiska Davida Hilberta), system naturalnej dedukcji oraz rachunek sekwentów. Ostatnie dwa systemy znajdują zastosowanie w pewnych działach sztucznej inteligencji oraz w systemach automatycznego dowodzenia twierdzeń.

System hilbertowski

Poniższy system dowodzenia dotyczy formuł zbudowanych przy użyciu jedynie spójnika $\displaystyle \to$, stałej $\displaystyle \bot$ oraz zmiennych zdaniowych. Przypomnijmy, że dla dowolnej formuły $\displaystyle \varphi$, napis $\displaystyle \neg \varphi$ jest skrótem zapisu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\bot} . Symbole $\displaystyle \varphi ,\psi ,\vartheta$ w poniższym systemie oznaczają dowolne formuły.

Aksjomaty

$(A1)\ \ \ \displaystyle \varphi \to (\psi \to \varphi )$
$(A2)\ \ \ \displaystyle (\varphi \to (\psi \to \vartheta ))\to ((\varphi \to \psi )\to (\varphi \to \vartheta ))$
$(A3)\ \ \ \displaystyle \neg \neg \varphi \to \varphi$

Reguła dowodzenia

Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle {\rm (MP)}\hspace{1cm} \frac{\varphi\ \ \ \varphi\to\psi}{\psi}}

Reguła (MP) jest nazywana regułą odrywania lub też regułą modus ponens.

Dowodem w powyższym systemie nazywamy taki ciąg formuł, w którym każda formuła albo jest aksjomatem, albo też została otrzymana z wcześniej występujących formuł w wyniku zastosowania reguły odrywania. Powiemy, że formuła $\displaystyle \varphi$ ma dowód lub jest twierdzeniem systemu hilbertowskiego, co zapiszemy $\displaystyle \vdash _{H}\varphi$, gdy istnieje dowód zawierający $\displaystyle \varphi$. Powyższą definicję możemy nieco uogólnić. Niech $\displaystyle \Delta$ będzie dowolnym zbiorem formuł. Powiemy, że formuła $\displaystyle \varphi$ ma dowód ze zbioru hipotez $\displaystyle \Delta$ (notacja $\displaystyle \Delta \vdash _{H}\varphi$), gdy $\displaystyle \varphi$ jest twierdzeniem systemu, w którym zbiór aksjomatów został poszerzony o formuły ze zbioru $\displaystyle \Delta$.

Przykład 5.1

Niech $\displaystyle p$ będzie zmienną zdaniową. Pokażemy, że formuła $\displaystyle p\to p$ jest twierdzeniem systemu hilbertowskiego. Poniżej podajemy dowód dla tej formuły. W nawiasach podajemy nazwę aksjomatu, jeśli dana formuła jest instancją tego aksjomatu, lub też numery formuł z wcześniejszych kroków dowodu, do których jest stosowana reguła odrywania.

1. $\displaystyle (p\to ((p\to p)\to p))\to ((p\to (p\to p))\to (p\to p))\ \ \ \ (A2)$
2. $\displaystyle p\to ((p\to p)\to p)\ \ \ \ (A1)$
3. $\displaystyle (p\to (p\to p))\to (p\to p)\ \ \ \ (1,2)$
4. $\displaystyle p\to (p\to p)\ \ \ \ (A1)$
5. $\displaystyle p\to p\ \ \ \ (3,4)$

Zauważmy, że w powyższym przykładzie możemy wszędzie zastąpić zmienną $\displaystyle p$ przez dowolną formułę $\displaystyle \varphi$ dostając dowód formuły $\displaystyle \varphi \to \varphi$.

Następujące twierdzenie jest bardzo użyteczne, gdy trzeba uzasadnić, że jakaś formuła jest twierdzeniem.

Twierdzenie 5.2 (o dedukcji)

Dla dowolnego zbioru formuł $\displaystyle \Delta$ oraz dowolnych formuł $\displaystyle \varphi ,\psi$, jeśli $\displaystyle \Delta \cup \{\varphi \}\vdash _{H}\psi$, to $\displaystyle \Delta \vdash _{H}\varphi \to \psi$.

Dowód

Dowód jest indukcyjny ze względu na liczbę kroków w dowodzie formuły $\displaystyle \psi$ ze zbioru hipotez $\displaystyle \Delta \cup \{\varphi \}$. Przypuśćmy najpierw, że dowód ten składa się tylko z jednego kroku. Jeśli $\displaystyle \psi =\varphi$, to stosując wyprowadzenie z Przykładu 5.1 dostajemy dowód formuły $\displaystyle \varphi \to \varphi$. Możemy oczywiście przyjąć, że formuła ta jest wyprowadzona ze zbioru hipotez $\displaystyle \Delta$. Druga możliwość jest taka, że $\displaystyle \psi \in \Delta$ lub też, że $\displaystyle \psi$ jest aksjomatem. W każdym z tych przypadków mamy $\displaystyle \Delta \vdash _{H}\psi$. Wówczas stosując regułę odrywania do $\displaystyle \psi$ oraz aksjomatu $\displaystyle \psi \to (\varphi \to \psi )$, dostajemy formułę $\displaystyle \varphi \to \psi$.

Założmy teraz, że ostatnim krokiem w wyprowadzeniu formuły $\displaystyle \psi$ jest zastosowanie reguły (MP) do formuł $\displaystyle \vartheta \to \psi$ oraz $\displaystyle \vartheta$, dla pewnej formuły $\displaystyle \vartheta$. Z założenia indukcyjnego mamy $\displaystyle \Delta \vdash _{H}\varphi \to (\vartheta \to \psi )$ oraz $\displaystyle \Delta \vdash _{H}\varphi \to \vartheta$. Stosując regułę odrywania do $\displaystyle \varphi \to (\vartheta \to \psi )$ oraz do aksjomatu (A2): $\displaystyle (\varphi \to (\vartheta \to \psi ))\to ((\varphi \to \vartheta )\to (\varphi \to \psi ))$ dostajemy formułę $\displaystyle (\varphi \to \vartheta )\to (\varphi \to \psi )$. Ponownie stosując regułę odrywania do tej formuły oraz do $\displaystyle \varphi \to \vartheta$ dostajemy żądaną formułę $\displaystyle \varphi \to \psi$. To kończy dowód twierdzenia o dedukcji.

Twierdzenie 5.3 (o poprawności)

Jeśli $\displaystyle \Delta \vdash _{H}\varphi$, to $\displaystyle \Delta \models \varphi$. W szczególności, jeśli $\displaystyle \vdash _{H}\varphi$, to $\displaystyle \varphi$ jest tautologią.

Dowód

Dowód jest indukcyjny ze względu na liczbę kroków w wyprowadzeniu formuły $\displaystyle \varphi$ w systemie hilbertowskim ze zbioru hipotez $\displaystyle \Delta$. Jeśli dowód ten składa się tylko z jednego kroku, to albo $\displaystyle \varphi \in \Delta$, albo $\displaystyle \varphi$ jest aksjomatem. W obu przypadkach oczywiście zachodzi $\displaystyle \Delta \models \varphi$.

Załóżmy teraz, że $\displaystyle \varphi$ jest otrzymana przez zastosowanie reguły odrywania do formuł $\displaystyle \psi \to \varphi$ oraz $\displaystyle \psi$. Z założenia indukcyjnego mamy

$\displaystyle \Delta \models \psi \to \varphi$ oraz Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \Delta\models\psi. \hspace{3cm}(1) }

Niech $\displaystyle \varrho$ będzie dowolnym wartościowaniem spełniającym wszystkie formuły z $\displaystyle \Delta$. Na mocy  (1), wartościowanie $\displaystyle \varrho$ spełnia $\displaystyle \psi \to \varphi$ oraz spełnia $\displaystyle \psi$. Wynika stąd, że $\displaystyle \varrho$ spełnia $\displaystyle \varphi$. Tym samym udowodniliśmy, że $\displaystyle \Delta \models \varphi$. To kończy dowód.

Lemat 5.4

Dla dowolnych formuł $\displaystyle \varphi ,\psi$ zbudowanych przy użyciu $\displaystyle \to$ oraz $\displaystyle \bot$, następujące formuły są twierdzeniami systemu hilbertowskiego.

1. $\displaystyle \varphi \to (\neg \psi \to \neg (\varphi \to \psi ))$;
2. $\displaystyle \bot \to \varphi$;
3. $\displaystyle (\varphi \to \psi )\to ((\neg \varphi \to \psi )\to \psi )$;

Dowód

(1)  Niech $\displaystyle \Delta =\{\varphi ,\psi \to \bot ,\varphi \to \psi \}$. Stosując regułę odrywania do formuł $\displaystyle \varphi$ oraz $\displaystyle \varphi \to \psi$ dostajemy $\displaystyle \psi$. Przez ponowne zastosowanie (MP) do tej formuły oraz do $\displaystyle \psi \to \bot$ otrzymujemy wyprowadzenie $\displaystyle \bot$. Tym samym pokazaliśmy, że $\displaystyle \Delta \vdash _{H}\bot$. Stosując teraz trzy razy twierdzenie o dedukcji dostajemy

$\displaystyle \vdash _{H}\varphi \to ((\psi \to \bot )\to ((\varphi \to \psi )\to \bot )),$

czyli

$\displaystyle \vdash _{H}\varphi \to (\neg \psi \to \neg (\varphi \to \psi )).$

(2)  Ponieważ $\displaystyle \{\bot ,\neg \varphi \}\vdash _{H}\bot$, więc z twierdzenia o dedukcji wynika $\displaystyle \bot \vdash _{H}\neg \neg \varphi$. Stosując teraz (MP) do tej formuły oraz do aksjomatu (A3) w postaci $\displaystyle \neg \neg \varphi \to \varphi$ otrzymujemy $\displaystyle \bot \vdash _{H}\varphi$. Ponowne zastosowanie twierdzenia o dedukcji daje nam $\displaystyle \vdash _{H}\bot \to \varphi$.

(3)  Niech $\displaystyle \Delta =\{\varphi \to \psi ,\neg \varphi \to \psi \}$. Zaczynamy od zbioru hipotez $\displaystyle \Delta \cup \{\varphi ,\neg \psi \}$. Stosując (MP) do formuł $\displaystyle \varphi$ oraz $\displaystyle \varphi \to \psi$ dostajemy $\displaystyle \psi$. Ponowne zastosowanie (MP) do tej formuły oraz do $\displaystyle \neg \psi$ daje nam $\displaystyle \bot$. Używając teraz twierdzenia o dedukcji do formuły $\displaystyle \bot$ otrzymujemy

$\displaystyle \Delta \cup \{\neg \psi \}\vdash _{H}\neg \varphi .$

Ponieważ mamy $\displaystyle \Delta \cup \{\neg \psi \}\vdash _{H}\neg \varphi \to \psi$, to stosując (MP) otrzymujemy $\displaystyle \Delta \cup \{\neg \psi \}\vdash _{H}\psi$. Jeszcze raz używamy (MP) aby z $\displaystyle \neg \psi$ i $\displaystyle \psi$ otrzymać $\displaystyle \bot$ i mamy

$\displaystyle \Delta \cup \{\neg \psi \}\vdash _{H}\bot .$

Na mocy twierdzenia o dedukcji $\displaystyle \Delta \vdash _{H}\neg \neg \psi$. Stosując (MP) do formuły $\displaystyle \neg \neg \psi$ oraz do aksjomatu $\displaystyle \neg \neg \psi \to \psi$ otrzymujemy $\displaystyle \Delta \vdash _{H}\psi$. Dwukrotne zastosowanie twierdzenia o dedukcji daje nam $\displaystyle \vdash _{H}(\varphi \to \psi )\to ((\neg \varphi \to \psi )\to \psi )$. To kończy dowód lematu.

Powyższy system można łatwo rozszerzyć do systemu dla formuł opartych o pozostałe spójniki logiczne. Wystarczy w tym celu dodać aksjomaty wyrażające równoważności definiujące te spójniki.

$(B1)\ \ \ \displaystyle \varphi \wedge \psi \to \neg (\varphi \to \neg \psi )$
$(B2)\ \ \ \displaystyle \neg (\varphi \to \neg \psi )\to \varphi \wedge \psi$
$(B3)\ \ \ \displaystyle \varphi \vee \psi \to (\neg \varphi \to \psi )$
$(B4)\ \ \ \displaystyle (\neg \varphi \to \psi )\to \varphi \vee \psi$

Tak otrzymany system oznaczymy przez $\displaystyle \vdash _{H^{+}}$.

Twierdzenie 5.5 (o poprawności dla $\displaystyle \vdash _{H^{+}}$)

Dla dowolnego zbioru formuł $\displaystyle \Delta$ i dla dowolnej formuły $\displaystyle \varphi$ w języku z Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vee,\wedge,\arr,\bot} , jeśli Parser nie mógł rozpoznać (nieznana funkcja „\se”): {\displaystyle \displaystyle \se_{H^+}\varphi} to $\displaystyle \Delta \models \varphi$.

Dowód

Wystarczy sprawdzić, że aksjomaty (B1)-(B4) są tautologiami. Konkluzja wynika z  Twierdzenia 5.3 o poprawności dla $\displaystyle \vdash _{H}$.

Lemat 5.6

Dla dowolnej formuły $\displaystyle \varphi$ istnieje formuła $\displaystyle {\tilde {\varphi }}$ zbudowana przy użyciu jedynie $\displaystyle \to$ oraz $\displaystyle \bot$, taka że $\displaystyle \vdash _{H^{+}}\varphi \to {\tilde {\varphi }}$ oraz $\displaystyle \vdash _{H^{+}}{\tilde {\varphi }}\to \varphi$.

Dowód

W danej formule $\displaystyle \varphi$, zastąpmy każdą podformułę postaci $\displaystyle \psi \wedge \vartheta$ formułą $\displaystyle \neg (\psi \to \neg \vartheta )$ oraz każdą podformułę postaci $\displaystyle \psi \vee \vartheta$ formułą $\displaystyle \neg \psi \to \vartheta$. Aksjomaty (B1)-(B4) mówią, że zastąpione formuły są równoważne. Tak więc łatwo dostajemy $\displaystyle \vdash _{H^{+}}\varphi \to {\tilde {\varphi }}$ oraz $\displaystyle \vdash _{H^{+}}{\tilde {\varphi }}\to \varphi$. Szczegóły dowodu pozostawimy Czytelnikowi.

System naturalnej dedukcji

System naturalnej dedukcji (wprowadzony przez S. Jaśkowskiego i G. Gentzena) operuje wyrażeniami zwanymi sekwentami. Są to wyrażenia postaci $\displaystyle \Delta \vdash \varphi$, gdzie $\displaystyle \Delta$ jest pewnym skończonym zbiorem formuł, a $\displaystyle \varphi$ jest formułą. W odróżnieniu od systemu hilbertowskiego, w naturalnej dedukcji istotne są reguły dowodzenia, a aksjomat jest bardzo prosty. Charakterystyczną cechą naturalnej dedukcji jest to, że reguły dowodzenia (za wyjątkiem reguły (PS) "przez sprzeczność") są podzielone na grupy, po jednej dla każdego spójnika. W ramach jednej takiej grupy mamy dwa rodzaje reguł. Reguły wprowadzania mówią o tym w jakiej sytuacji można wprowadzić dany spójnik na prawo od znaku $\displaystyle \vdash$ (tj. wywnioskować formułę danego kształtu). Reguły eliminacji mówią o tym, w jakiej sytuacji można ten spójnik wyeliminować, tzn. jak można użyć formuły zbudowanej z jego pomocą do wyprowadzenia innej formuły. Regułę dowodzenia "przez sprzeczność" można traktować jako "silną" regułę eliminacji $\displaystyle \bot$. Pamiętajmy, że $\displaystyle \neg \varphi$ oznacza formułę $\displaystyle \varphi \to \bot$.

Poniżej będziemy stosować następującą konwencję: Napis $\displaystyle \Delta ,\varphi _{1},\ldots ,\varphi _{n}$ oznacza zbiór $\displaystyle \Delta \cup \{\varphi _{1},\ldots ,\varphi _{n}\}$, przy czym nie zakładamy tu, że $\displaystyle \varphi _{i}\not \in \Delta$.

Aksjomat

$(A0)\ \ \ \displaystyle \Delta ,\varphi \vdash \varphi$

Reguły dowodzenia

$\displaystyle (\to$ -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\to\psi} \hspace{1cm} (\to } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta\vdash\varphi\to\psi\qquad \Delta\vdash\varphi}{\Delta\vdash\psi}}

$\displaystyle (\wedge$ -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\qquad \Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}}

$\displaystyle (\vee$ -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm} (\vee } -intro Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi} }

$\displaystyle (\vee$ -elim Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\qquad \Delta,\varphi\vdash\vartheta\qquad \Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}}

$\displaystyle ($ PS Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\neg\varphi\vdash\bot}{\Delta\vdash\varphi}}

Zauważmy, że szczególnym przypadkiem reguły ($\displaystyle \to$ -intro) jest następująca reguła, można ją traktować jak regułę wprowadzenia negacji.

$\displaystyle {\frac {\Delta ,\varphi \vdash \bot }{\Delta \vdash \neg \varphi }}$

Zauważmy też, że szczególnym przypadkiem reguły ($\displaystyle \to$ -elim) jest następująca reguła, można ją traktować jak regułę eliminacji negacji.

$\displaystyle {\frac {\Delta \vdash \neg \varphi \quad \Delta \vdash \varphi }{\Delta \vdash \bot }}$

O ile dowody w systemie hilbertowskim są tradycyjnie definiowane jako ciągi, a więc struktury liniowe, to w systemie naturalnej dedukcji dowody są drzewami. Pozwala to znacznie lepiej wizualizować zależności pomiędzy przesłankami i konkluzją stosowanych reguł. Dowodem sekwentu $\displaystyle \Delta \vdash \varphi$ w systemie naturalnej dedukcji nazwiemy drzewo etykietowane sekwentami tak, że korzeń ma etykietę $\displaystyle \Delta \vdash \varphi$, liście są etykietowane wystąpieniami aksjomatu oraz każdy wewnętrzny wierzchołek jest etykietowany sekwentem otrzymanym z etykiet potomków tego wierzchołka przy zastosowaniu jednej z reguł. Piszemy $\displaystyle \Delta \vdash _{N}\varphi$, gdy sekwent $\displaystyle \Delta \vdash \varphi$ ma dowód w systemie naturalnej dedukcji. Gdy $\displaystyle \Delta =\emptyset$, to mówimy też, że $\displaystyle \varphi$ jest twierdzeniem systemu naturalnej dedukcji i zapisujemy to przez $\displaystyle \vdash _{N}\varphi$. Jeśli $\displaystyle \Delta$ jest zbiorem nieskończonym, to $\displaystyle \Delta \vdash _{N}\varphi$ oznacza, że istnieje dowód sekwentu $\displaystyle \Delta _{0}\vdash \varphi$, dla pewnego skończonego $\displaystyle \Delta _{0}\subseteq \Delta$.

Poniżej podajemy kilka przykładów dowodów w systemie naturalnej dedukcji.

Przykład 5.7

• Pokażemy $\displaystyle \vdash _{N}p\to p$.

$\displaystyle {\frac {p\vdash p}{\vdash p\to p}}(\to \ -intro)$

• Pokażemy $\displaystyle \vdash _{N}p\to (q\to p)$.

$\displaystyle {\frac {{\frac {p,q\vdash p}{p\vdash q\to p}}(\to -intro)}{\vdash p\to (q\to p)}}(\to -intro)$

• Pokażemy $\displaystyle \vdash _{N}\neg \neg p\to p$.

$\displaystyle {\frac {\neg \neg p,\neg p\vdash \neg \neg p\qquad \neg \neg p,\neg p\vdash \neg p}{{\frac {\neg \neg p,\neg p\vdash p}{{\frac {\neg \neg p\vdash p}{\vdash \neg \neg p\to p}}(\to -\ intro)}}(PS)}}(\to -\ elim)$

Twierdzenie 5.8

Dla dowolnego sekwentu $\displaystyle \Delta \vdash \varphi$ mamy następującą równoważność:

Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \Delta\vdash_{N}\varphi\hspace{.2cm} } , gdy Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \hspace{.2cm} \Delta\vdash_{H^+}\varphi.}

Aby pokazać, że każdy dowód w $\displaystyle \vdash _{N}$ daje się przerobić na dowód w $\displaystyle \vdash _{H^{+}}$ wystarczy sprawdzić, że każda z reguł systemu naturalnej dedukcji jest dopuszczalna w $\displaystyle H^{+}$. Tzn. wystarczy sprawdzić, że jeśli mamy dowody przesłanek w $\displaystyle \vdash _{H^{+}}$, to możemy udowodnić konkluzję. Zauważmy, że wyprowadzalność reguły($\displaystyle \to -$ intro) jest konsekwencją twierdzenia o dedukcji, natomiast reguła ($\displaystyle \to -$ elim) jest regułą (MP). Przykładowo pokażemy wyprowadzenie ($\displaystyle \vee -$ elim) oraz (PS) w $\displaystyle H^{+}$, pozostawiając Czytelnikowi wyprowadzenie pozostałych reguł.

Załóżmy, że mamy w $\displaystyle H^{+}$ dowody następujących sekwentów: $\displaystyle \Delta \vdash \varphi \vee \psi$, {.1cm} $\displaystyle \Delta ,\varphi \vdash \vartheta$ {.1cm}oraz {.1cm} $\displaystyle \Delta ,\psi \vdash \vartheta$. Wówczas, stosując aksjomat (B2) i regułę (MP) mamy $\displaystyle \Delta \vdash _{H^{+}}\neg \varphi \to \psi$. Zatem $\displaystyle \Delta ,\neg \varphi \vdash _{H^{+}}\psi$ i ponieważ $\displaystyle \Delta \vdash _{H^{+}}\psi \to \vartheta$ to również $\displaystyle \Delta ,\neg \varphi \vdash _{H^{+}}\psi \to \vartheta$. Stąd $\displaystyle \Delta ,\neg \varphi \vdash _{H^{+}}\vartheta$. Stosując twierdzenie o dedukcji dostajemy $\displaystyle \Delta \vdash _{H^{+}}\neg \varphi \to \vartheta$. Skoro mamy również $\displaystyle \delta \vdash _{H^{+}}\varphi \to \vartheta$, to na mocy  Lematu 5.4 (3) otrzymujemy $\displaystyle \Delta \vdash _{H^{+}}\vartheta$.

Dla wyprowadzenia (PS) załóżmy, że $\displaystyle \Delta ,\neg \varphi \vdash _{H^{+}}\bot$. Z twierdzenia o dedukcji dostajemy $\displaystyle \Delta \vdash _{H^{+}}\neg \neg \varphi$. Tak więc z (A3) i (MP) dostajemy $\displaystyle \Delta \vdash _{H^{+}}\varphi$.

Dla pokazania implikacji odwrotnej wystarczy pokazać, że wszystkie aksjomaty systemu $\displaystyle H^{+}$ są twierdzeniami systemu naturalnej dedukcji. Wyprowadzenia (A1) i (A3) w ND zostały podane w  Przykładzie 5.7. Przykładowo pokażemy wyprowadzenia (A2) i (B1). Zaczniemy od wyprowadzenia (A2). Niech $\displaystyle \Delta =\{\varphi \to (\psi \to \vartheta ),\ \varphi \to \psi ,\ \varphi \}$. Mamy następujący dowód:

$\displaystyle {\frac {{\frac {\Delta \vdash \varphi \to (\psi \to \vartheta )\qquad \Delta \vdash \varphi }{\Delta \vdash \psi \to \vartheta }}(\to -\ elim)\qquad {\frac {\Delta \vdash \varphi \to \psi \qquad \Delta \vdash \varphi }{\Delta \vdash \psi }}(\to -\ elim)}{\Delta \vdash \vartheta }}(\to -\ elim)$

Stosując trzy razy ($\displaystyle \to$ -intro ) do sekwentu $\displaystyle \Delta \vdash \vartheta$ dostajemy wyprowadzenie aksjomatu (A2).

Następnie pokażemy dowód (B1) w ND. Zaczniemy od wyprowadzenia $\displaystyle \neg (\varphi \to \neg \psi )\vdash \varphi$, gdzie $\displaystyle \Delta =\{\neg (\varphi \to \neg \psi ),\neg \varphi \}$:

$\displaystyle {\frac {{\frac {{\frac {{\frac {\Delta ,\varphi ,\psi \vdash \neg \varphi \qquad \Delta ,\varphi ,\psi \vdash \varphi }{\Delta ,\varphi ,\psi \vdash \bot }}(\to -\ elim)}{\Delta ,\varphi \vdash \neg \psi }}(\to -\ intro)}{\Delta \vdash \varphi \to \neg \psi }}(\to -\ intro)\qquad \Delta \vdash \neg (\varphi \to \neg \psi )}{{\frac {\Delta \vdash \bot }{\neg (\varphi \to \neg \psi )\vdash \varphi }}(PS)}}(\to -\ elim)$

Następnie wyprowadzimy sekwent $\displaystyle \neg (\varphi \to \neg \psi )\vdash \psi$. Niech $\displaystyle \Delta =\{\neg (\varphi \to \neg \psi ),\neg \psi \}$

$\displaystyle {\frac {{\frac {\Delta ,\varphi \vdash \neg \psi }{\Delta \vdash \varphi \to \neg \psi }}(\to -\ intro)\qquad \Delta \vdash \neg (\varphi \to \neg \psi )}{{\frac {\Delta \vdash \bot }{\neg (\varphi \to \neg \phi )\vdash \phi }}(PS)}}(\to -\ elim)$

Mając wyprowadzone sekwenty $\displaystyle \neg (\varphi \to \neg \psi )\vdash \varphi$ oraz $\displaystyle \neg (\varphi \to \neg \psi )\vdash \psi$, możemy zakończyć dowód (B1).

$\displaystyle {\frac {\neg (\varphi \to \neg \psi )\vdash \varphi \qquad \neg (\varphi \to \neg \psi )\vdash \psi }{{\frac {\neg (\varphi \to \neg \psi )\vdash \varphi \wedge \psi }{\vdash \neg (\varphi \to \neg \psi )\to (\varphi \wedge \psi )}}(\to -\ intro)}}(\wedge -\ intro)$

Rachunek sekwentów

Dla przedstawienia rachunku sekwentów rozszerzymy nieco pojęcie sekwentu. Przez sekwent będziemy teraz rozumieć napis $\displaystyle \Delta \vdash \Gamma$, gdzie $\displaystyle \Delta$ oraz $\displaystyle \Gamma$ są skończonymi zbiorami formuł. Intuicyjnie, wyprowadzalność sekwentu $\displaystyle \Delta \vdash \Gamma$ w rachunku sekwentów będzie oznaczać, że alternatywa formuł z $\displaystyle \Gamma$ wynika z hipotez $\displaystyle \Delta$.

Podobnie jak w poprzedniej części, rozważamy formuły, zbudowane w oparciu o spójniki $\displaystyle \to ,\vee ,\wedge$ oraz stałą zdaniową $\displaystyle \bot$. Negację $\displaystyle \neg$ traktujemy jako spójnik zdefiniowany przez $\displaystyle \to$ i $\displaystyle \bot$.

Charakterystyczną cechą rachunku sekwentów jest specyficzna postać reguł. Reguły w tym systemie naturalnie dzielą się na dwie grupy: jedna grupa reguł opisuje sytuacje kiedy możemy wprowadzić dany spójnik na lewo od znaku $\displaystyle \vdash$, a druga grupa jest odpowiedzialna za wprowadzanie spójnika na prawo od $\displaystyle \vdash$. Dla każdego spójnika mamy odpowiadającą parę reguł. Aksjomat (A$\displaystyle \bot$) można traktować jako regułę (bez przesłanek) wprowadzenia $\displaystyle \bot$ z lewej strony znaku $\displaystyle \vdash$.

Przypomnijmy, że napis $\displaystyle \Delta ,\varphi _{1},\ldots ,\varphi _{n}$ oznacza zbiór $\displaystyle \Delta \cup \{\varphi _{1},\ldots ,\varphi _{n}\}$.

Aksjomaty

$(A00)\ \ \ \displaystyle \Delta ,\varphi \vdash \Gamma ,\varphi$

$(A\bot )\ \ \ \displaystyle \Delta ,\bot \vdash \Gamma$

Reguły dowodzenia

$\displaystyle (\to$ -lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi\qquad \Delta,\psi\vdash\Gamma}{\Delta,\varphi\to\psi\vdash\Gamma} \hspace{1cm}(\to } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma,\psi}{\Delta\vdash\Gamma, \varphi\to\psi}}

$\displaystyle (\wedge$ -lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi,\psi\vdash\Gamma}{\Delta,\varphi\wedge\psi\vdash\Gamma} \hspace{1cm} (\wedge } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma, \varphi\qquad \Delta\vdash\Gamma,\psi}{\Delta\vdash \Gamma,\varphi\wedge\psi}}

$\displaystyle (\vee$ -lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta, \varphi\vdash\Gamma\qquad \Delta,\psi\vdash\Gamma}{\Delta, \varphi\vee\psi \vdash\Gamma} \hspace{1cm} (\vee } -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma, \varphi, \psi}{\Delta\vdash\Gamma, \varphi\vee\psi}}

Dowodem sekwentu $\displaystyle \Delta \vdash \Gamma$, tak jak poprzednio, nazywamy drzewo etykietowane sekwentami tak, że korzeń jest etykietowany przez $\displaystyle \Delta \vdash \Gamma$, liście są etykietowane aksjomatami oraz wierzchołki wewnętrzne są etykietowane sekwentami otrzymanymi poprawnie przez zastosowanie reguł dowodzenia. Jeśli istnieje dowód sekwentu $\displaystyle \Delta \vdash \Gamma$ w rachunku sekwentów to zapisujemy to tak: $\displaystyle \Delta \vdash _{G}\Gamma$. (Litera G pochodzi od nazwiska twórcy tego systemu, G. Gentzena.) Piszemy też $\displaystyle \Delta \vdash _{G}\varphi$, gdy $\displaystyle \Delta$ jest nieskończony, ale $\displaystyle \Delta \vdash _{G}\varphi$ dla pewnego skończonego $\displaystyle \Delta _{0}\subseteq \Delta$.

Zauważmy, że jeśli mamy sekwent $\displaystyle \Delta \vdash \Gamma ,\varphi$ to stosując aksjomat ($A\displaystyle \bot$), a następnie ($\displaystyle \to$ -lewa) dostajemy sekwent $\displaystyle \Delta ,\neg \varphi \vdash \Gamma$. Zatem natępująca reguła jest dopuszczalna w systemie $\displaystyle \vdash _{G}$ (tj. jeśli dodamy ją do systemu, to zbiór wyprowadzalnych sekwentów nie ulegnie zmianie):

$\displaystyle (\neg$ -lewa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi}{\Delta, \neg\varphi\vdash\Gamma}}

Ponadto zauważmy, że jeśli mamy dowód sekwentu $\displaystyle \Delta \vdash \Gamma$, to dla każdej formuły $\displaystyle \varphi$ możemy ją dodać do prawej strony każdego sekwentu w tym dowodzie i otrzymamy dowód sekwentu $\displaystyle \Delta \vdash \Gamma ,\varphi$. Łatwy dowód indukcyjny pozostawiamy Czytelnikowi ( Ćwiczenie 12).
W szczególności, jeśli mamy udowodniony sekwent $\displaystyle \Delta ,\varphi \vdash \Gamma$, to możemy też udowodnić sekwent $\displaystyle \Delta ,\varphi \vdash \Gamma ,\bot$.
Stosując do niego regułę ($\displaystyle \to$ -prawa) otrzymujemy sekwent $\displaystyle \Delta \vdash \Gamma ,\neg \varphi$. Tym samym pokazaliśmy, że następująca reguła jest dopuszczalna w systemie $\displaystyle \vdash _{G}$:

$\displaystyle (\neg$ -prawa Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle)\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma}{\Delta \vdash\Gamma,\neg\varphi}}

Twierdzenie 5.9

Dla każdych $\displaystyle \Delta$ i $\displaystyle \varphi$ mamy następującą równoważność

Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \Delta\vdash_G\varphi\hspace{.2cm} } wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle \hspace{.2cm} \Delta\vdash_{H^+}\varphi.}

Powyższe twierdzenie pozostawimy bez dowodu. Łatwo jest "przetłumaczyć" każde wyprowadzenie w systemie $\displaystyle \vdash _{G}$ na dowód w stylu Hilberta. Dla dowodu implikacji odwrotnej rozszerza się system $\displaystyle \vdash _{G}$ przez dodanie nowej reguły zwanej cięciem.

$\displaystyle ($ cięcie Parser nie mógł rozpoznać (nieznana funkcja „\hspace”): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma\hspace{.7cm} \Delta\vdash\varphi, \Gamma}{\Delta\vdash\Gamma}}

Niech $\displaystyle \vdash _{GC}$ oznacza system gentzenowski z cięciem. Bez trudu można pokazać, że reguła odrywania jest dopuszczalna w $\displaystyle \vdash _{GC}$. Zatem, korzystając z twierdzenia o pełności dla systemu hilbertowskiego, łatwo pokazujemy, że każda tautologia jest twierdzeniem systemu $\displaystyle \vdash _{GC}$. Główna trudność w dowodzie  Twierdzenia 5.9 polega na udowodnieniu następującego twierdzenia o eliminacji cięcia. Twierdzenie to podajemy bez dowodu.

Twierdzenie 5.10 (o eliminacji cięcia)

Jeśli $\displaystyle \Delta \vdash _{GC}\Gamma$, to $\displaystyle \Delta \vdash _{G}\Gamma$.

Główna zaleta dowodów w rachunku sekwentów (bez cięcia) wynika z następującej własności podformuł: wszystkie formuły występujące w przesłance dowolnej reguły są podformułami formuł występujących w konkluzji. Zatem np. w dowodzie sekwentu $\displaystyle ~\vdash \varphi$ mamy do czynienia tylko z podformułami formuły $\displaystyle \varphi$. Dla danej formuły $\displaystyle \varphi$, łatwiej więc znaleźć dowód w sensie Gentzena niż np. dowód w sensie Hilberta. Dlatego systemy zbliżone do rachunku sekwentów znajdują zastosowanie w automatycznym dowodzeniu twierdzeń. Pokażemy to na przykładzie.

Przykład 5.11

1. Poszukamy dowodu sekwentu $\displaystyle \vdash \neg \neg \varphi \to \varphi$ w

$\displaystyle \vdash _{G}$. Ponieważ najbardziej zewnętrznym spójnikiem w rozważanej formule jest $\displaystyle \to$, to ostatnią regułą w poszukiwanym dowodzie musiała być reguła ($\displaystyle \to$ -prawa). Zatem wystarczy znaleźć dowód sekwentu $\displaystyle \neg \neg \varphi \vdash \varphi$. Najbardziej zewnętrznym spójnikiem formuły po lewej stronie jest $\displaystyle \neg$, a zatem na mocy reguły ($\displaystyle \neg$ -lewa) wystarczy udowodnić sekwent $\displaystyle \vdash \varphi ,\neg \varphi$. Podobnie, na mocy reguły ($\displaystyle \neg$ -prawa), wystarczy udowodnić sekwent $\displaystyle \varphi \vdash \varphi$, a on przecież jest aksjomatem.

1. Jeśli zastosujemy powyższą procedurę do formuły, która

nie jest tautologią, to dostaniemy wskazówkę na to gdzie należy szukać wartościowania falsyfikującego tę formułę. (Wartościowanie falsyfikujące sekwent $\displaystyle \Delta \vdash \Gamma$ to takie, które spełnia wszystkie formuły z $\displaystyle \Delta$ oraz falsyfikuje wszystkie formuły z $\displaystyle \Gamma$.) Dla zilustrowania tej tezy weźmy bardzo prosty sekwent $\displaystyle \vdash p\to q$. Postępując podobnie jak poprzednio, dochodzimy do sekwentu $\displaystyle p\vdash q$, który nie jest aksjomatem, i którego nie możemy już dalej rozłożyć. Jako wartościowanie falsyfikujące wystarczy wziąć wartościowanie spełniające $\displaystyle p$ i falsyfikujące $\displaystyle q$.

Z własności podformuł wynika też własność konserwatywności systemu nad swoimi fragmentami: jeśli formuła, w której nie występuje jakiś spójnik jest tautologią, to jej wyprowadzenie nie wymaga reguł związanych z tym spójnikiem.