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

<span id="rownanie1"></span>

$\mathrm{\Delta }\models \psi \to \phi$ oraz $\mathrm{\Delta }\models \psi .$

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

Dla dowolnych formuł $\phi ,\psi$ zbudowanych przy użyciu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} oraz $\mathrm{\perp }$, następuj±ce formuły s± twierdzeniami systemu hilbertowskiego.

1. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi \arr(\neg\psi\arr\neg(\varphi\arr\psi))} ;
2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \bot\arr\varphi} ;
3. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr\psi)\arr((\neg\varphi\arr\psi)\arr\psi)} ;

Dowód

(1)  Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\varphi,\psi\arr\bot,\varphi\arr\psi\}} . Stosuj±c regułę odrywania do formuł $\phi$ oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} dostajemy $\psi$. Przez ponowne zastosowanie (MP) do tej formuły oraz do Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr\bot} otrzymujemy wyprowadzenie $\mathrm{\perp }$. Tym samym pokazali¶my, że $\mathrm{\Delta }{⊢}_H\mathrm{\perp }$. Stosuj±c teraz trzy razy twierdzenie o dedukcji dostajemy

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\varphi\arr((\psi\arr\bot)\arr((\varphi\arr\psi)\arr\bot)),}

czyli

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\varphi \arr(\neg\psi\arr\neg(\varphi\arr\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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\varphi\arr\varphi} otrzymujemy $\mathrm{\perp }{⊢}_H\phi$. Ponowne zastosowanie twierdzenia o dedukcji daje nam Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\bot\arr\varphi} .

(3)  Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\varphi\arr\psi,\neg\varphi\arr\psi\}} . Zaczynamy od zbioru hipotez $\mathrm{\Delta }\cup \{\phi ,\mathrm{\neg }\psi \}$. Stosuj±c (MP) do formuł $\phi$ oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\cup\{\neg\psi\}\vdash_H\neg\varphi\arr\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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\psi\arr\psi} otrzymujemy $\mathrm{\Delta }{⊢}_H\psi$. Dwukrotne zastosowanie twierdzenia o dedukcji daje nam Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H(\varphi\arr\psi)\arr((\neg\varphi\arr\psi)\arr\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)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\wedge \psi\arr\neg(\varphi\arr\neg\psi)}
(B2)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\arr\varphi\wedge \psi}
(B3)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\vee\psi\arr(\neg\varphi\arr\psi)}
(B4)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\neg\varphi\arr\psi)\arr\varphi\vee\psi}

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

Twierdzenie 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 Uzupelnic tw-zda-2| o poprawno¶ci dla ${⊢}_H$.

Lemat

Dla dowolnej formuły $\phi$ istnieje formuła $\tilde{\phi }$ zbudowana przy użyciu jedynie Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} oraz $\mathrm{\perp }$, taka że Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\varphi\arr\tilde{\varphi}} {.1cm} oraz {.1cm} Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\tilde{\varphi}\arr\varphi} .

Dowód

W danej formule $\phi$, zast±pmy każd± podformułę postaci $\psi \wedge \vartheta$ formuł± Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\psi\arr\neg\vartheta)} oraz każd± podformułę postaci $\psi \vee \vartheta$ formuł± Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\psi\arr\vartheta} . Aksjomaty (B1)--(B4) mówi±, że zast±pione formuły s± równoważne. Tak więc łatwo dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\varphi\arr\tilde{\varphi}} oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\tilde{\varphi}\arr\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 $\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łę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\bot} .

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

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

• Pokażemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{N}p\arr p} .

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{p\vdash p}{\vdash p\arr p} }

• Pokażemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{N} p\arr(q\arr p)} .

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{\arintro{p,q\vdash p}{p\vdash q\arr p}}{\vdash p\arr (q\arr p)} }

• Pokażemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{N}\neg\neg p\arr p} .

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{\ps{\arelim{\neg\neg p,\neg p\vdash\neg\neg p} {\neg\neg p,\neg p\vdash\neg p}{\neg\neg p,\neg p\vdash p}} {\neg\neg p\vdash p}}{\vdash\neg\neg p\arr p} }

Twierdzenie

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(Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -intro) jest konsekwencj± twierdzenia o dedukcji, natomiast reguła (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_{H^+}\neg\varphi\arr\psi} . Zatem $\mathrm{\Delta },\mathrm{\neg }\phi {⊢}_{H^{+}}\psi$ i ponieważ Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_{H^+}\psi\arr\vartheta} to również Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta,\neg\varphi\vdash_{H^+}\psi\arr\vartheta} . St±d $\mathrm{\Delta },\mathrm{\neg }\phi {⊢}_{H^{+}}\vartheta$. Stosuj±c twierdzenie o dedukcji dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_{H^+}\neg\varphi\arr\vartheta} . Skoro mamy również Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \delta\vdash_{H^+}\varphi\arr\vartheta} , to na mocy Lematu Uzupelnic le-zda-1|(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 Uzupelnic pr-zda-2|. Przykładowo pokażemy wyprowadzenia (A2) i (B1). Zaczniemy od wyprowadzenia (A2). Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\varphi\arr(\psi\arr\vartheta),\ \varphi\arr\psi,\ \varphi\}} . Mamy następuj±cy dowód:

Parser nie mógł rozpoznać (nieznana funkcja „\arelim”): {\displaystyle \displaystyle \arelim{\arelim{\se\varphi\arr(\psi\arr\vartheta)}{\se\varphi} {\se\psi\arr\vartheta}} {\arelim{\se\varphi\arr\psi}{\se\varphi}{\se\psi}}{\se\vartheta} }

Stosuj±c trzy razy (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr } -intro ) do sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\se”): {\displaystyle \displaystyle \se\vartheta} dostajemy wyprowadzenie aksjomatu (A2).

Następnie pokażemy dowód (B1) w ND. Zaczniemy od wyprowadzenia Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\varphi} , gdzie Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\neg(\varphi\arr\neg\psi), \neg\varphi\}} :

Parser nie mógł rozpoznać (nieznana funkcja „\ps”): {\displaystyle \displaystyle \ps{\arelim{\arintro{\arintro{\arelim{\Delta,\varphi,\psi\vdash\neg\varphi} {\Delta,\varphi,\psi\vdash\varphi}{\Delta,\varphi,\psi\vdash\bot}} {\Delta,\varphi\vdash\neg\psi}}{\se\varphi\arr\neg\psi}} {\se\neg(\varphi\arr\neg\psi)}{\se\bot}} {\neg(\varphi\arr\neg\psi)\vdash\varphi} }

Następnie wyprowadzimy sekwent Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\psi} . Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\neg(\varphi\arr\neg\psi), \neg\psi\}}

Parser nie mógł rozpoznać (nieznana funkcja „\ps”): {\displaystyle \displaystyle \ps{\arelim{\arintro{\Delta,\varphi\vdash\neg\psi}{\se\varphi\arr\neg\psi}} {\se\neg(\varphi\arr\neg\psi)}{\se\bot}}{\neg(\varphi\arr\neg\psi)\vdash\psi} }

Maj±c wyprowadzone sekwenty Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\varphi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\psi} możemy zakończyć dowód (B1).

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{\wedgeintro{\neg(\varphi\arr\neg\psi)\vdash\varphi} {\neg(\varphi\arr\neg\psi)\vdash\psi} {\neg(\varphi\arr\neg\psi)\vdash\varphi\wedge\psi}} {\vdash\neg(\varphi\arr\neg\psi)\arr(\varphi\wedge\psi)} }

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.