Logika dla informatyków/Paradygmaty dowodzenia

Paradygmaty dowodzenia

{twierdzenie}{0}

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 Uzupelnic entscheidungsproblem|). 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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} , 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) Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr(\psi\arr\varphi)}
(A2) Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr(\psi\arr\vartheta))\arr((\varphi\arr\psi) \arr(\varphi\arr\vartheta))}
(A3) Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\varphi\arr\varphi}

Reguła dowodzenia

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\rm (MP)}\hspace{1cm} \frac{\varphi\odstep \varphi\arr\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

Niech $p$ będzie zmienn± zdaniow±. Pokażemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr 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. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (p\arr((p\arr p)\arr p))\arr((p\arr(p\arr p))\arr(p\arr p))}

(A2)

1. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr((p\arr p)\arr p)} (A1)
2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (p\arr(p\arr p))\arr(p\arr p)} (1,2)
3. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr(p\arr p)} (A1)
4. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr 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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\varphi} .

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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_H\varphi\arr\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 Uzupelnic pr-zda-1a| dostajemy dowód formuły Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\varphi} . 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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr(\varphi\arr\psi)} dostajemy formułę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} .

Założmy teraz, że ostatnim krokiem w wyprowadzeniu formuły $\psi$ jest zastosowanie reguły (MP) do formuł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vartheta\arr\psi} oraz $\vartheta$, dla pewnej formuły $\vartheta$. Z założenia indukcyjnego mamy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_H\varphi\arr (\vartheta\arr\psi)} oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_H\varphi\arr\vartheta} . Stosuj±c regułę odrywania do Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr (\vartheta\arr\psi)} oraz do aksjomatu (A2): Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr(\vartheta\arr\psi))\arr ((\varphi\arr\vartheta)\arr(\varphi\arr\psi))} dostajemy formułę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr\vartheta)\arr(\varphi\arr\psi)} . Ponownie stosuj±c regułę odrywania do tej formuły oraz do Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\vartheta} dostajemy ż±dan± formułę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\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ł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr\varphi} oraz $\psi$. Z założenia indukcyjnego mamy

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\models\psi\arr\varphi } oraz $\mathrm{\Delta }\models \psi .$

Niech $\varrho$ będzie dowolnym warto¶ciowaniem spełniaj±cym wszystkie formuły z $\mathrm{\Delta }$. Na mocy (Uzupelnic eq-zad-1|), warto¶ciowanie $\varrho$ spełnia Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr\varphi} 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.

{Ćwiczenia}

1. Niech ${⊢}_{H_1}$ oznacza system dowodzenia otrzymany

z systemu ${⊢}_H$ przez zamianę aksjomatu (A3) na następuj±cy aksjomat:

(A3')  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\neg\varphi\arr\neg\psi)\arr((\neg\varphi\arr \psi)\arr\varphi).}

Dowie¶ć, że obydwa systemy s± równoważne, tzn., że dla dowolnego sekwentu $\mathrm{\Delta }⊢\phi$, zachodzi $\mathrm{\Delta }{⊢}_H\phi$ , gdy $\mathrm{\Delta }{⊢}_{H_1}\phi$.

1. Niech ${⊢}_{H_2}$ oznacza system dowodzenia otrzymany

z systemu ${⊢}_H$ przez zamianę aksjomatu (A3) na ${⊢}_H$, następuj±cy aksjomat:

(A3")  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\neg\varphi\arr\neg\psi)\arr(\psi\arr\varphi).}

Dowie¶ć, że obydwa systemy s± równoważne, tzn., że dla dowolnego sekwentu $\mathrm{\Delta }⊢\phi$, zachodzi $\mathrm{\Delta }{⊢}_H\phi$ , gdy $\mathrm{\Delta }{⊢}_{H_2}\phi$.

1. Dowie¶ć, że aksjomatu (A3) nie da się wyprowadzić z

aksjomatów (A0--2) przy pomocy reguły odrywania.

1. Dowie¶ć Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\neg p \arr(p\arr q)} używaj±c twierdzenia o

dedukcji oraz bez użycia tego twierdzenia.

1. Pokazać, że w systemie ${⊢}_H$ dopuszczalna jest

następuj±ca reguła:

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \frac{\varphi\arr\psi\odstep \neg\psi}{\neg\varphi}}

tzn. pokazać, że je¶li Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_H\varphi\arr\psi} oraz $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\psi$, to również mamy $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\phi$.

1. Dowie¶ć, że dla każdej formuły $\phi$, nie będ±cej

tautologi±, istnieje maksymalny zbiór formuł $\mathrm{\Delta }$ (nad dan± sygnatur±) o tej własno¶ci, że $\mathrm{\Delta }{⊢}_H\phi$.

1. Każdy z poniższych sekwentów wyprowadzić w systemie

${⊢}_{H^{+}}$, ${⊢}_N$, ${⊢}_G$.

 =   2pt

1. 1. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash \bot\arr p} ;
   2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr q,q\arr r\vdash p\arr r} ;
   3. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash(\neg p\arr p)\arr p} ;
   4. $p,\mathrm{\neg }p⊢q$;
   5. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr(q\arr r)\vdash q\arr(p\arr r)} ;
   6. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash (\neg p\arr \neg q)\arr (q\arr p)} ;
   7. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash \neg(p\wedge q)\arr(\neg p\vee\neg q)} .
2. Dowie¶ć, że je¶li $\mathrm{\Delta }{⊢}_N\phi$, to dla dowolnej

formuły $\psi$ zachodzi $\mathrm{\Delta },\psi {⊢}_N\phi$.

1. Dowie¶ć, że je¶li $\mathrm{\Delta }{⊢}_N\mathrm{\perp }$, to dla dowolnej

formuły $\phi$ zachodzi $\mathrm{\Delta }{⊢}_N\phi$.

1. Dla każdego z sytemów ${⊢}_{H^{+}}$, ${⊢}_N$,

${⊢}_G$ dowie¶ć, że je¶li sekwent $\mathrm{\Delta }⊢\phi$ jest wyprowadzalny w tym systemie oraz $S$ jest podstawieniem formuł na zmienne zdaniowe, to sekwent $\overrightarrow{S}(\mathrm{\Delta })⊢S(\phi )$ powstaj±cy w wyniku podstawienia jest też wyprowadzalny w tym systemie.

Udowodnić, że w rachunku sekwentów zamiana reguły $(\vee$ -prawa $)$ 

na dwie reguły:

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \displaystyle \prooftree{\Delta\vdash\Gamma,\varphi} \justifies{\Delta\vdash\Gamma,\varphi\vee\psi} \endprooftree \hspace{3cm} \prooftree{\Delta\vdash\Gamma,\psi} \justifies{\Delta\vdash\Gamma,\varphi\vee\psi} \endprooftree}

daje w wyniku równoważny system dowodzenia (wyprowadzalne s± te same sekwenty).

Udowodnić, że następuj±ce reguły osłabiania s± dopuszczalne w rachunku sekwentów:

Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \displaystyle \prooftree{\Delta\vdash\Gamma}\justifies{\Delta,\varphi\vdash\Gamma} \endprooftree \hspace{3cm} \prooftree{\Delta\vdash\Gamma}\justifies{\Delta\vdash\Gamma,\varphi} \endprooftree}

1. Wyprowadzić w rachunku sekwentów:
   1. $⊢p\vee \mathrm{\neg }p$;
   2. $⊢((p\to q)\to p)\to p$.

Czy można to zrobić używaj±c tylko sekwentów postaci $\mathrm{\Delta }⊢\phi$ (z jedn± formuł± po prawej)?