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 $2^n$ różnych wartościowań, gdzie $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 $\to$, stałej $\mathrm{\perp }$ oraz zmiennych zdaniowych. Przypomnijmy, że dla dowolnej formuły $\phi$, napis $\mathrm{\neg }\phi$ jest skrótem zapisu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\bot} . Symbole $\phi ,\psi ,\vartheta$ w poniższym systemie oznaczają dowolne formuły.

Aksjomaty

$(A1)\phi \to (\psi \to \phi )$
$(A2)(\phi \to (\psi \to \vartheta ))\to ((\phi \to \psi )\to (\phi \to \vartheta ))$
$(A3)\mathrm{\neg }\mathrm{\neg }\phi \to \phi$

Reguła dowodzenia

Parser nie mógł rozpoznać (błąd składni): {\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 $\phi$ ma dowód, lub jest twierdzeniem systemu hilbertowskiego, co zapiszemy ${⊢}_H\phi$, gdy istnieje dowód zawierający $\phi$. Powyższą definicję możemy nieco uogólnić. Niech $\mathrm{\Delta }$ będzie dowolnym zbiorem formuł. Powiemy, że formuła $\phi$ ma dowód ze zbioru hipotez $\mathrm{\Delta }$ (notacja $\mathrm{\Delta }{⊢}_H\phi$), gdy $\phi$ jest twierdzeniem systemu, w którym zbiór aksjomatów został poszerzony o formuły ze zbioru $\mathrm{\Delta }$.

Przykład 5.1

Niech $p$ będzie zmienną zdaniową. Pokażemy, że formuła $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. $(p\to ((p\to p)\to p))\to ((p\to (p\to p))\to (p\to p))(A2)$
2. $p\to ((p\to p)\to p)(A1)$
3. $(p\to (p\to p))\to (p\to p)(1,2)$
4. $p\to (p\to p)(A1)$
5. $p\to p(3,4)$

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

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ł $\mathrm{\Delta }$ oraz dowolnych formuł $\phi ,\psi$, jeśli $\mathrm{\Delta }\cup \{\phi \}{⊢}_H\psi$, to $\mathrm{\Delta }{⊢}_H\phi \to \psi$.

Dowód

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

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

Twierdzenie 5.3 (o poprawności)

Jeśli $\mathrm{\Delta }{⊢}_H\phi$, to $\mathrm{\Delta }\models \phi$. W szczególności, jeśli ${⊢}_H\phi$, to $\phi$ jest tautologią.

Dowód

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

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

$\mathrm{\Delta }\models \psi \to \phi$ oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \Delta\models\psi. \hspace{3cm}(1) }

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

Lemat 5.4

Dla dowolnych formuł $\phi ,\psi$ zbudowanych przy użyciu $\to$ oraz $\mathrm{\perp }$, następujące formuły są twierdzeniami systemu hilbertowskiego.

1. $\phi \to (\mathrm{\neg }\psi \to \mathrm{\neg }(\phi \to \psi ))$;
2. $\mathrm{\perp }\to \phi$;
3. $(\phi \to \psi )\to ((\mathrm{\neg }\phi \to \psi )\to \psi )$;

Dowód

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

${⊢}_H\phi \to ((\psi \to \mathrm{\perp })\to ((\phi \to \psi )\to \mathrm{\perp })),$

czyli

${⊢}_H\phi \to (\mathrm{\neg }\psi \to \mathrm{\neg }(\phi \to \psi )).$

(2)  Ponieważ $\{\mathrm{\perp },\mathrm{\neg }\phi \}{⊢}_H\mathrm{\perp }$, więc z twierdzenia o dedukcji wynika $\mathrm{\perp }{⊢}_H\mathrm{\neg }\mathrm{\neg }\phi$. Stosując teraz (MP) do tej formuły oraz do aksjomatu (A3) w postaci $\mathrm{\neg }\mathrm{\neg }\phi \to \phi$ otrzymujemy $\mathrm{\perp }{⊢}_H\phi$. Ponowne zastosowanie twierdzenia o dedukcji daje nam ${⊢}_H\mathrm{\perp }\to \phi$.

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

$\mathrm{\Delta }\cup \{\mathrm{\neg }\psi \}{⊢}_H\mathrm{\neg }\phi .$

Ponieważ mamy $\mathrm{\Delta }\cup \{\mathrm{\neg }\psi \}{⊢}_H\mathrm{\neg }\phi \to \psi$, to stosując (MP) otrzymujemy $\mathrm{\Delta }\cup \{\mathrm{\neg }\psi \}{⊢}_H\psi$. Jeszcze raz używamy (MP) aby z $\mathrm{\neg }\psi$ i $\psi$ otrzymać $\mathrm{\perp }$ i mamy

$\mathrm{\Delta }\cup \{\mathrm{\neg }\psi \}{⊢}_H\mathrm{\perp }.$

Na mocy twierdzenia o dedukcji $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\mathrm{\neg }\psi$. Stosując (MP) do formuły $\mathrm{\neg }\mathrm{\neg }\psi$ oraz do aksjomatu $\mathrm{\neg }\mathrm{\neg }\psi \to \psi$ otrzymujemy $\mathrm{\Delta }{⊢}_H\psi$. Dwukrotne zastosowanie twierdzenia o dedukcji daje nam ${⊢}_H(\phi \to \psi )\to ((\mathrm{\neg }\phi \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)\phi \wedge \psi \to \mathrm{\neg }(\phi \to \mathrm{\neg }\psi )$
$(B2)\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )\to \phi \wedge \psi$
$(B3)\phi \vee \psi \to (\mathrm{\neg }\phi \to \psi )$
$(B4)(\mathrm{\neg }\phi \to \psi )\to \phi \vee \psi$

Tak otrzymany system oznaczymy przez ${⊢}_{H^{+}}$.

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

Dla dowolnego zbioru formuł $\mathrm{\Delta }$ i dla dowolnej formuły $\phi$ 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 $\mathrm{\Delta }\models \phi$.

Dowód

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

Lemat 5.6

Dla dowolnej formuły $\phi$ istnieje formuła $\tilde{\phi }$ zbudowana przy użyciu jedynie $\to$ oraz $\mathrm{\perp }$, taka że ${⊢}_{H^{+}}\phi \to \tilde{\phi }$ oraz ${⊢}_{H^{+}}\tilde{\phi }\to \phi$.

Dowód

W danej formule $\phi$, zastąpmy każdą podformułę postaci $\psi \wedge \vartheta$ formułą $\mathrm{\neg }(\psi \to \mathrm{\neg }\vartheta )$ oraz każdą podformułę postaci $\psi \vee \vartheta$ formułą $\mathrm{\neg }\psi \to \vartheta$. Aksjomaty (B1)-(B4) mówią, że zastąpione formuły są równoważne. Tak więc łatwo dostajemy ${⊢}_{H^{+}}\phi \to \tilde{\phi }$ oraz ${⊢}_{H^{+}}\tilde{\phi }\to \phi$. 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 $\mathrm{\Delta }⊢\phi$, gdzie $\mathrm{\Delta }$ jest pewnym skończonym zbiorem formuł, a $\phi$ 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 $⊢$ (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 $\mathrm{\perp }$. Pamiętajmy, że $\mathrm{\neg }\phi$ oznacza formułę $\phi \to \mathrm{\perp }$.

Poniżej będziemy stosować następującą konwencję: Napis $\mathrm{\Delta },{\phi }_1,\dots ,{\phi }_n$ oznacza zbiór $\mathrm{\Delta }\cup \{{\phi }_1,\dots ,{\phi }_n\}$, przy czym nie zakładamy tu, że ${\phi }_i\in ̸\mathrm{\Delta }$.

Aksjomat

$(A0)\mathrm{\Delta },\phi ⊢\phi$

Reguły dowodzenia

$(\to$ -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\to\psi} \hspace{1cm} (\to } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta\vdash\varphi\to\psi\qquad \Delta\vdash\varphi}{\Delta\vdash\psi}}

$(\wedge$ -intro Parser nie mógł rozpoznać (błąd składni): {\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ć (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}}

$(\vee$ -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm} (\vee } -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi} }

$(\vee$ -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\qquad \Delta,\varphi\vdash\vartheta\qquad \Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}}

$($ PS Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\neg\varphi\vdash\bot}{\Delta\vdash\varphi}}

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

$\frac{\mathrm{\Delta },\phi ⊢\mathrm{\perp }}{\mathrm{\Delta }⊢\mathrm{\neg }\phi }$

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

$\frac{\mathrm{\Delta }⊢\mathrm{\neg }\phi \mathrm{\Delta }⊢\phi }{\mathrm{\Delta }⊢\mathrm{\perp }}$

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 $\mathrm{\Delta }⊢\phi$ w systemie naturalnej dedukcji nazwiemy drzewo etykietowane sekwentami tak, że korzeń ma etykietę $\mathrm{\Delta }⊢\phi$, 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 $\mathrm{\Delta }{⊢}_N\phi$, gdy sekwent $\mathrm{\Delta }⊢\phi$ ma dowód w systemie naturalnej dedukcji. Gdy $\mathrm{\Delta }=\mathrm{\varnothing }$, to mówimy też, że $\phi$ jest twierdzeniem systemu naturalnej dedukcji i zapisujemy to przez ${⊢}_N\phi$. Jeśli $\mathrm{\Delta }$ jest zbiorem nieskończonym, to $\mathrm{\Delta }{⊢}_N\phi$ oznacza, że istnieje dowód sekwentu ${\mathrm{\Delta }}_0⊢\phi$, dla pewnego skończonego ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$.

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

Przykład 5.7

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

$\frac{p⊢p}{⊢p\to p}(\to -intro)$

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

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

• Pokażemy ${⊢}_N\mathrm{\neg }\mathrm{\neg }p\to p$.

$\frac{\frac{\frac{\mathrm{\neg }\mathrm{\neg }p,\mathrm{\neg }p⊢\mathrm{\neg }\mathrm{\neg }p\mathrm{\neg }\mathrm{\neg }p,\mathrm{\neg }p⊢\mathrm{\neg }p}{\mathrm{\neg }\mathrm{\neg }p,\mathrm{\neg }p⊢p}}{\mathrm{\neg }\mathrm{\neg }p⊢p}}{⊢\mathrm{\neg }\mathrm{\neg }p\to p}$

Twierdzenie 5.8

Dla dowolnego sekwentu $\mathrm{\Delta }⊢\phi$ mamy następującą równoważność:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \Delta\vdash_{N}\varphi\hspace{.2cm} } , gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \hspace{.2cm} \Delta\vdash_{H^+}\varphi.}

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

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

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

Dla pokazania implikacji odwrotnej wystarczy pokazać, że wszystkie aksjomaty systemu $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 $\mathrm{\Delta }=\{\phi \to (\psi \to \vartheta ),\phi \to \psi ,\phi \}$. Mamy następujący dowód:

$\frac{\frac{\mathrm{\Delta }⊢\phi \to (\psi \to \vartheta )\mathrm{\Delta }⊢\phi }{\mathrm{\Delta }⊢\psi \to \vartheta }(\to -elim)\frac{\mathrm{\Delta }⊢\phi \to \psi \mathrm{\Delta }⊢\phi }{\mathrm{\Delta }⊢\psi }(\to -elim)}{\mathrm{\Delta }⊢\vartheta }(\to -elim)$

Stosując trzy razy ($\to$ -intro ) do sekwentu $\mathrm{\Delta }⊢\vartheta$ dostajemy wyprowadzenie aksjomatu (A2).

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

$\frac{\frac{\frac{\frac{\mathrm{\Delta },\phi ,\psi ⊢\mathrm{\neg }\phi \mathrm{\Delta },\phi ,\psi ⊢\phi }{\mathrm{\Delta },\phi ,\psi ⊢\mathrm{\perp }}(\to -elim)}{\mathrm{\Delta },\phi ⊢\mathrm{\neg }\psi }(\to -intro)}{\mathrm{\Delta }⊢\phi \to \mathrm{\neg }\psi }(\to -intro)\mathrm{\Delta }⊢\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )}{\frac{\mathrm{\Delta }⊢\mathrm{\perp }}{\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )⊢\phi }(PS)}(\to -elim)$

Następnie wyprowadzimy sekwent $\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )⊢\psi$. Niech $\mathrm{\Delta }=\{\mathrm{\neg }(\phi \to \mathrm{\neg }\psi ),\mathrm{\neg }\psi \}$

$\frac{\frac{\mathrm{\Delta },\phi ⊢\mathrm{\neg }\psi }{\mathrm{\Delta }⊢\phi \to \mathrm{\neg }\psi }(\to -intro)\mathrm{\Delta }⊢\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )}{\frac{\mathrm{\Delta }⊢\mathrm{\perp }}{\mathrm{\neg }(\phi \to \mathrm{\neg }\varphi )⊢\varphi }(PS)}(\to -elim)$

Mając wyprowadzone sekwenty $\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )⊢\phi$ oraz $\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )⊢\psi$ możemy zakończyć dowód (B1).

h

$\frac{\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )⊢\phi \mathrm{\neg }(\phi \to \mathrm{\neg }\psi )⊢\psi }{\frac{\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )⊢\phi \wedge \psi }{⊢\mathrm{\neg }(\phi \to \mathrm{\neg }\psi )\to (\phi \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 $\mathrm{\Delta }⊢\mathrm{\Gamma }$, gdzie $\mathrm{\Delta }$ oraz $\mathrm{\Gamma }$ s± skończonymi zbiorami formuł. Intuicyjnie, wyprowadzalno¶ć sekwentu $\mathrm{\Delta }⊢\mathrm{\Gamma }$ w rachunku sekwentów będzie oznaczać, że alternatywa formuł z $\mathrm{\Gamma }$ wynika z hipotez $\mathrm{\Delta }$.

Podobnie jak w poprzedniej czę¶ci, rozważamy formuły, zbudowane w oparciu o spójniki Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr,\vee,\wedge} oraz stał± zdaniow± $\mathrm{\perp }$. Negację $\mathrm{\neg }$ traktujemy jako spójnik zdefiniowany przez Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} i $\mathrm{\perp }$.

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 $⊢$, a druga grupa jest odpowiedzialna za wprowadzanie spójnika na prawo od $⊢$. Dla każdego spójnika mamy odpowiadaj±c± parę reguł. Aksjomat (A$\mathrm{\perp }$) można traktować jako regułę (bez przesłanek) wprowadzenia $\mathrm{\perp }$ z lewej strony znaku $⊢$.

Przypomnijmy, że napis $\mathrm{\Delta },{\phi }_1,\dots ,{\phi }_n$ oznacza zbiór $\mathrm{\Delta }\cup \{{\phi }_1,\dots ,{\phi }_n\}$.

Aksjomaty

(A00)  $\mathrm{\Delta },\phi ⊢\mathrm{\Gamma },\phi$

(A$\mathrm{\perp }$)  $\mathrm{\Delta },\mathrm{\perp }⊢\mathrm{\Gamma }$

Reguły dowodzenia

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\arr } -lewa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi\odstep \Delta,\psi\vdash\Gamma}{\Delta,\varphi\arr\psi\vdash\Gamma} \hspace{1cm}(\arr } -prawa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma,\psi}{\Delta\vdash\Gamma, \varphi\arr\psi}} $(\wedge$ -lewa Parser nie mógł rozpoznać (błąd składni): {\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ć (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma, \varphi\odstep \Delta\vdash\Gamma,\psi}{\Delta\vdash \Gamma,\varphi\wedge\psi}} $(\vee$ -lewa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta, \varphi\vdash\Gamma\odstep \Delta,\psi\vdash\Gamma}{\Delta, \varphi\vee\psi \vdash\Gamma} \hspace{1cm} (\vee } -prawa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma, \varphi, \psi}{\Delta\vdash\Gamma, \varphi\vee\psi}}

Dowodem sekwentu $\mathrm{\Delta }⊢\mathrm{\Gamma }$, tak jak poprzednio, nazywamy drzewo etykietowane sekwentami tak, że korzeń jest etykietowany przez $\mathrm{\Delta }⊢\mathrm{\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 $\mathrm{\Delta }⊢\mathrm{\Gamma }$ w rachunku sekwentów to zapisujemy to tak: $\mathrm{\Delta }{⊢}_G\mathrm{\Gamma }$. (Litera G pochodzi od nazwiska twórcy tego systemu, G. Gentzena.) Piszemy też $\mathrm{\Delta }{⊢}_G\phi$, gdy $\mathrm{\Delta }$ jest nieskończony, ale $\mathrm{\Delta }{⊢}_G\phi$ dla pewnego skończonego ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$.

Zauważmy, że je¶li mamy sekwent $\mathrm{\Delta }⊢\mathrm{\Gamma },\phi$ to stosuj±c aksjomat (A$\mathrm{\perp }$), a następnie (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -lewa) dostajemy sekwent $\mathrm{\Delta },\mathrm{\neg }\phi ⊢\mathrm{\Gamma }$. Zatem natępuj±ca reguła jest dopuszczalna w systemie ${⊢}_G$ (tj. je¶li dodamy j± do systemu, to zbiór wyprowadzalnych sekwentów nie ulegnie zmianie):

$(\mathrm{\neg }$ -lewa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi}{\Delta, \neg\varphi\vdash\Gamma}}

Ponadto zauważmy, że je¶li mamy dowód sekwentu $\mathrm{\Delta }⊢\mathrm{\Gamma }$, to dla każdej formuły $\phi$ możemy j± dodać do prawej strony każdego sekwentu w tym dowodzie i otrzymamy dowód sekwentu $\mathrm{\Delta }⊢\mathrm{\Gamma },\phi$. Łatwy dowód indukcyjny pozostawiamy Czytelnikowi (Ćwiczenie Uzupelnic weakening|). W szczególno¶ci, je¶li mamy udowodniony sekwent $\mathrm{\Delta },\phi ⊢\mathrm{\Gamma }$, to możemy też udowodnić sekwent $\mathrm{\Delta },\phi ⊢\mathrm{\Gamma },\mathrm{\perp }$. Stosuj±c do niego regułę (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -prawa) otrzymujemy sekwent $\mathrm{\Delta }⊢\mathrm{\Gamma },\mathrm{\neg }\phi$. Tym samym pokazali¶my, że następuj±ca reguła jest dopuszczalna w systemie ${⊢}_G$:

$(\mathrm{\neg }$ -prawa Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma}{\Delta \vdash\Gamma,\neg\varphi}}

Twierdzenie

Dla każdych $\mathrm{\Delta }$ i $\phi$ mamy następuj±c± równoważno¶ć

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \Delta\vdash_G\varphi\hspace{.2cm} } wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \hspace{.2cm} \Delta\vdash_{H^+}\varphi.}

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

$($ cięcie Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma\hspace{.7cm} \Delta\vdash\varphi, \Gamma}{\Delta\vdash\Gamma}}

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

Twierdzenie o eliminacji cięcia

Je¶li $\mathrm{\Delta }{⊢}_{GC}\mathrm{\Gamma }$, to $\mathrm{\Delta }{⊢}_G\mathrm{\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 formuwystępuj±cych w konkluzji. Zatem np. w dowodzie sekwentu $⊢\phi$ mamy do czynienia tylko z podformułami formuły $\phi$. Dla danej formuły $\phi$, ł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

1. Poszukamy dowodu sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash\neg\neg\varphi\arr\varphi} w

${⊢}_G$. Ponieważ najbardziej zewnętrznym spójnikiem w rozważanej formule jest Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} , to ostatni± reguł± w poszukiwanym dowodzie musiała być reguła (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -prawa). Zatem wystarczy znaleĽć dowód sekwentu $\mathrm{\neg }\mathrm{\neg }\phi ⊢\phi$. Najbardziej zewnętrznym spójnikiem formuły po lewej stronie jest $\mathrm{\neg }$, a zatem na mocy reguły ($\mathrm{\neg }$-lewa) wystarczy udowodnić sekwent $⊢\phi ,\mathrm{\neg }\phi$. Podobnie, na mocy reguły ($\mathrm{\neg }$-prawa), wystarczy udowodnić sekwent $\phi ⊢\phi$, 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 $\mathrm{\Delta }⊢\mathrm{\Gamma }$ to takie, które spełnia wszystkie formuły z $\mathrm{\Delta }$ oraz falsyfikuje wszystkie formuły z $\mathrm{\Gamma }$.) Dla zilustrowania tej tezy weĽmy bardzo prosty sekwent Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash p\arr q} . Postępuj±c podobnie jak porzednio dochodzimy do sekwentu $p⊢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 $p$ i falsyfikuj±ce $q$.

Z własno¶ci podformuwynika 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 reguzwi±zanych z tym spójnikiem.