Logika dla informatyków/Paradygmaty dowodzenia: Różnice pomiędzy wersjami

Aktualna wersja na dzień 22:11, 11 wrz 2023

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 $⊥$ oraz zmiennych zdaniowych. Przypomnijmy, że dla dowolnej formuły $φ$ , napis $\neg φ$ jest skrótem zapisu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \varphi\arr\bot} . Symbole $φ, ψ, ϑ$ w poniższym systemie oznaczają dowolne formuły.

Aksjomaty

$(A 1) φ \to (ψ \to φ)$
$(A 2) (φ \to (ψ \to ϑ)) \to ((φ \to ψ) \to (φ \to ϑ))$
$(A 3) \neg \neg φ \to φ$

Reguła dowodzenia

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

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.

$(p \to ((p \to p) \to p)) \to ((p \to (p \to p)) \to (p \to p)) (A 2)$
$p \to ((p \to p) \to p) (A 1)$
$(p \to (p \to p)) \to (p \to p) (1, 2)$
$p \to (p \to p) (A 1)$
$p \to p (3, 4)$

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

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ł $Δ$ oraz dowolnych formuł $φ, ψ$ , jeśli $Δ \cup {φ} ⊢_{H} ψ$ , to $Δ ⊢_{H} φ \to ψ$ .

Dowód

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

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

Twierdzenie 5.3 (o poprawności)

Jeśli $Δ ⊢_{H} φ$ , to $Δ ⊨ φ$ . W szczególności, jeśli $⊢_{H} φ$ , to $φ$ jest tautologią.

Dowód

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

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

Δ ⊨ ψ \to φ

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

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

Lemat 5.4

Dla dowolnych formuł $φ, ψ$ zbudowanych przy użyciu $\to$ oraz $⊥$ , następujące formuły są twierdzeniami systemu hilbertowskiego.

$φ \to (\neg ψ \to \neg (φ \to ψ))$ ;
$⊥ \to φ$ ;
$(φ \to ψ) \to ((\neg φ \to ψ) \to ψ)$ ;

Dowód

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

⊢_{H} φ \to ((ψ \to ⊥) \to ((φ \to ψ) \to ⊥))

,

czyli

⊢_{H} φ \to (\neg ψ \to \neg (φ \to ψ))

.

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

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

Δ \cup {\neg ψ} ⊢_{H} \neg φ

Ponieważ mamy $Δ \cup {\neg ψ} ⊢_{H} \neg φ \to ψ$ , to stosując (MP) otrzymujemy $Δ \cup {\neg ψ} ⊢_{H} ψ$ . Jeszcze raz używamy (MP) aby z $\neg ψ$ i $ψ$ otrzymać $⊥$ i mamy

Δ \cup {\neg ψ} ⊢_{H} ⊥

Na mocy twierdzenia o dedukcji $Δ ⊢_{H} \neg \neg ψ$ . Stosując (MP) do formuły $\neg \neg ψ$ oraz do aksjomatu $\neg \neg ψ \to ψ$ otrzymujemy $Δ ⊢_{H} ψ$ . Dwukrotne zastosowanie twierdzenia o dedukcji daje nam $⊢_{H} (φ \to ψ) \to ((\neg φ \to ψ) \to ψ)$ . 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.

$(B 1) φ \land ψ \to \neg (φ \to \neg ψ)$
$(B 2) \neg (φ \to \neg ψ) \to φ \land ψ$
$(B 3) φ \lor ψ \to (\neg φ \to ψ)$
$(B 4) (\neg φ \to ψ) \to φ \lor ψ$

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

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

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

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 $φ$ istnieje formuła $\tilde{φ}$ zbudowana przy użyciu jedynie $\to$ oraz $⊥$ , taka że $⊢_{H^{+}} φ \to \tilde{φ}$ oraz $⊢_{H^{+}} \tilde{φ} \to φ$ .

Dowód

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

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

Aksjomat

$(A 0) Δ, φ ⊢ φ$

Reguły dowodzenia

(\to

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

(\land

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

(\lor

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

(\lor

-elim Parser nie mógł rozpoznać (błąd składni): {\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 )\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{Δ, φ ⊢ ⊥}{Δ ⊢ \neg φ}

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{Δ ⊢ \neg φ Δ ⊢ φ}{Δ ⊢ ⊥}

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

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 - i n t r o)

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

\frac{\frac{p, q ⊢ p}{p ⊢ q \to p} (\to - i n t r o)}{⊢ p \to (q \to p)} (\to - i n t r o)

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

\frac{\neg \neg p, \neg p ⊢ \neg \neg p \neg \neg p, \neg p ⊢ \neg p}{\frac{\neg \neg p, \neg p ⊢ p}{\frac{\neg \neg p ⊢ p}{⊢ \neg \neg p \to p} (\to - i n t r o)} (P S)} (\to - e l i m)

Twierdzenie 5.8

Dla dowolnego sekwentu $Δ ⊢ φ$ mamy następującą równoważność:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \Delta\vdash_{N}\varphi\hspace{.2cm}} , gdy Parser nie mógł rozpoznać (błąd składni): {\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 ( $\lor -$ elim) oraz (PS) w $H^{+}$ , pozostawiając Czytelnikowi wyprowadzenie pozostałych reguł.

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

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

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 $Δ = {φ \to (ψ \to ϑ), φ \to ψ, φ}$ . Mamy następujący dowód:

\frac{\frac{Δ ⊢ φ \to (ψ \to ϑ) Δ ⊢ φ}{Δ ⊢ ψ \to ϑ} (\to - e l i m) \frac{Δ ⊢ φ \to ψ Δ ⊢ φ}{Δ ⊢ ψ} (\to - e l i m)}{Δ ⊢ ϑ} (\to - e l i m)

Stosując trzy razy ( $\to$ -intro ) do sekwentu $Δ ⊢ ϑ$ dostajemy wyprowadzenie aksjomatu (A2).

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

\frac{\frac{\frac{\frac{Δ, φ, ψ ⊢ \neg φ Δ, φ, ψ ⊢ φ}{Δ, φ, ψ ⊢ ⊥} (\to - e l i m)}{Δ, φ ⊢ \neg ψ} (\to - i n t r o)}{Δ ⊢ φ \to \neg ψ} (\to - i n t r o) Δ ⊢ \neg (φ \to \neg ψ)}{\frac{Δ ⊢ ⊥}{\neg (φ \to \neg ψ) ⊢ φ} (P S)} (\to - e l i m)

Następnie wyprowadzimy sekwent $\neg (φ \to \neg ψ) ⊢ ψ$ . Niech $Δ = {\neg (φ \to \neg ψ), \neg ψ}$

\frac{\frac{Δ, φ ⊢ \neg ψ}{Δ ⊢ φ \to \neg ψ} (\to - i n t r o) Δ ⊢ \neg (φ \to \neg ψ)}{\frac{Δ ⊢ ⊥}{\neg (φ \to \neg ϕ) ⊢ ϕ} (P S)} (\to - e l i m)

Mając wyprowadzone sekwenty $\neg (φ \to \neg ψ) ⊢ φ$ oraz $\neg (φ \to \neg ψ) ⊢ ψ$ , możemy zakończyć dowód (B1).

\frac{\neg (φ \to \neg ψ) ⊢ φ \neg (φ \to \neg ψ) ⊢ ψ}{\frac{\neg (φ \to \neg ψ) ⊢ φ \land ψ}{⊢ \neg (φ \to \neg ψ) \to (φ \land ψ)} (\to - i n t r o)} (\land - i n t r o)

Rachunek sekwentów

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

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

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 $⊥$ ) można traktować jako regułę (bez przesłanek) wprowadzenia $⊥$ z lewej strony znaku $⊢$ .

Przypomnijmy, że napis $Δ, φ_{1}, \dots, φ_{n}$ oznacza zbiór $Δ \cup {φ_{1}, \dots, φ_{n}}$ .

Aksjomaty

$(A 00) Δ, φ ⊢ Γ, φ$

$(A ⊥) Δ, ⊥ ⊢ Γ$

Reguły dowodzenia

(\to

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

(\land

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

(\lor

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

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

Zauważmy, że jeśli mamy sekwent $Δ ⊢ Γ, φ$ to stosując aksjomat ( $A ⊥$ ), a następnie ( $\to$ -lewa) dostajemy sekwent $Δ, \neg φ ⊢ Γ$ . 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):

(\neg

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

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

(\neg

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

Twierdzenie 5.9

Dla każdych $Δ$ i $φ$ mamy następującą równoważność

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \Delta\vdash_G\varphi\hspace{.2cm}} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (błąd składni): {\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 )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma\hspace{.7cm} \Delta\vdash\varphi, \Gamma}{\Delta\vdash\Gamma}}

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

Twierdzenie 5.10 (o eliminacji cięcia)

Jeśli $Δ ⊢_{G C} Γ$ , to $Δ ⊢_{G} Γ$ .

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

Przykład 5.11

Poszukamy dowodu sekwentu $⊢ \neg \neg φ \to φ$ w

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

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 $Δ ⊢ Γ$ to takie, które spełnia wszystkie formuły z $Δ$ oraz falsyfikuje wszystkie formuły z $Γ$ .) Dla zilustrowania tej tezy weźmy bardzo prosty sekwent $⊢ p \to q$ . Postępując podobnie jak poprzednio, 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 podformuł wynika też własność konserwatywności systemu nad swoimi fragmentami: jeśli formuła, w której nie występuje jakiś spójnik jest tautologią, to jej wyprowadzenie nie wymaga reguł związanych z tym spójnikiem.

Logika dla informatyków/Paradygmaty dowodzenia: Różnice pomiędzy wersjami

Aktualna wersja na dzień 22:11, 11 wrz 2023

Spis treści

Paradygmaty dowodzenia

System hilbertowski

System naturalnej dedukcji

Rachunek sekwentów

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 1: / Linia 1: @@
-Sprawdzenie, czy dana formuła rachunku zdań jest tautologi±, polega zwykle na obliczeniu jej warto¶ci dla&nbsp;<math>2^n</math> różnych warto¶ciowań,gdzie <math>n</math> jest liczb± zmiennych zdaniowych tej formuły. Jak dot±d nie s± znane radykalnie szybsze metody. Dla rachunkupredykatów nie istnieje w&nbsp;ogóle żaden algorytm sprawdzania czy dana formuła jest tautologi± \begin{eqnarray*}Twierdzenie&nbsp;[[#entscheidungsproblem]]\end{eqnarray*}. W&nbsp;obu przypadkach istniej± jednak metody ''dowodzenia\/'' pozwalaj±ce na wyprowadzanie prawdziwych formuł za pomoc±\boldsymbol{s}}\def\blank{\hbox{\sf Bstalonych procedursyntaktycznych.
+==Paradygmaty dowodzenia==
+Sprawdzenie, czy dana formuła rachunku zdań jest tautologią,
+polega zwykle na obliczeniu jej wartości dla&nbsp;<math>2^n</math> różnych wartościowań,
+gdzie <math>n</math> jest liczbą zmiennych zdaniowych tej formuły. Jak dotąd nie są
+znane radykalnie szybsze metody. Dla rachunku
+predykatów nie istnieje w&nbsp;ogóle żaden algorytm sprawdzania czy
+dana formuła jest tautologią [[Logika dla informatyków/Logika pierwszego rzędu. Sposób użycia#entscheidungsproblem|(Twierdzenie 3.8)]]. W&nbsp;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ł \begin{eqnarray*}lub wyrażeń zbudowanych z wielu formuł\end{eqnarray*} zwanych {\em aksjomatami};
+* 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 {\em regułami dowodzenia}.
+* 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&nbsp;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&nbsp;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 <math>\to</math>, stałej <math>\bot</math> oraz zmiennych zdaniowych. Przypomnijmy, że dla dowolnej formuły <math>\varphi</math>, napis <math>\neg\varphi</math> jest skrótem zapisu <math>\varphi\arr\bot</math>.
+Symbole <math>\varphi,\psi,\vartheta</math> w poniższym systemie oznaczają dowolne
+formuły.
+'''Aksjomaty'''
+<math>(A1)\ \ \ \varphi\to(\psi\to\varphi)</math><br>
+<math>(A2)\ \ \ (\varphi\to(\psi\to\vartheta))\to((\varphi\to\psi)\to(\varphi\to\vartheta))</math><br>
+<math>(A3)\ \ \ \neg\neg\varphi\to\varphi</math>
+'''Reguła dowodzenia'''<br>
+<center><math>{\rm (MP)}\hspace{1cm} \frac{\varphi\ \ \
+\varphi\to\psi}{\psi}</math></center>
+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&nbsp;wcześniej
+występujących formuł w wyniku zastosowania reguły odrywania. Powiemy,
+że formuła <math>\varphi</math> ''ma dowód'' lub jest ''twierdzeniem''
+systemu hilbertowskiego, co zapiszemy <math>\vdash_H\varphi</math>,
+gdy istnieje dowód zawierający <math>\varphi</math>. Powyższą definicję możemy
+nieco uogólnić. Niech <math>\Delta</math> będzie dowolnym zbiorem
+formuł. Powiemy, że formuła <math>\varphi</math> ma dowód
+ze zbioru hipotez <math>\Delta</math> (notacja <math>\Delta\vdash_H\varphi</math>),
+gdy <math>\varphi</math> jest twierdzeniem systemu, w&nbsp;którym zbiór aksjomatów został
+poszerzony o formuły ze zbioru <math>\Delta</math>.
+{{przyklad|5.1|prz5.1|
+Niech <math>p</math> będzie zmienną zdaniową. Pokażemy, że formuła <math>p\to p</math> 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.
+# <math>(p\to((p\to p)\to p))\to((p\to(p\to p))\to(p\to p))\ \ \ \ (A2)</math>
+# <math>p\to((p\to p)\to p)\ \ \ \ (A1)</math>
+# <math>(p\to(p\to p))\to(p\to p)\ \ \ \ (1,2)</math>
+# <math>p\to(p\to p)\ \ \ \ (A1)</math>
+# <math>p\to p\ \ \ \ (3,4)</math>
+}}
+Zauważmy, że w powyższym przykładzie możemy wszędzie zastąpić
+zmienną <math>p</math> przez dowolną formułę <math>\varphi</math> dostając dowód formuły
+<math>\varphi\to\varphi</math>.
+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ł <math>\Delta</math> oraz dowolnych formuł <math>\varphi,\psi</math>,
+jeśli <math>\Delta\cup\{\varphi\}\vdash_H\psi</math>,
+to <math>\Delta\vdash_H\varphi\to\psi</math>.
+}}
+{{dowod|||
+Dowód jest indukcyjny ze względu na liczbę kroków w dowodzie formuły
+<math>\psi</math> ze zbioru hipotez <math>\Delta\cup\{\varphi\}</math>. Przypuśćmy najpierw, że dowód ten
+składa się tylko z jednego kroku. Jeśli <math>\psi=\varphi</math>, to
+stosując wyprowadzenie z Przykładu&nbsp;[[#prz5.1|5.1]] dostajemy dowód
+formuły <math>\varphi\to\varphi</math>. Możemy oczywiście przyjąć, że formuła ta
+jest wyprowadzona ze zbioru hipotez <math>\Delta</math>. Druga możliwość jest taka, że
+<math>\psi\in\Delta</math> lub też, że <math>\psi</math> jest aksjomatem.
+W każdym z tych
+przypadków mamy <math>\Delta\vdash_H\psi</math>. Wówczas stosując regułę
+odrywania do <math>\psi</math> oraz aksjomatu <math>\psi\to(\varphi\to\psi)</math>,
+dostajemy formułę <math>\varphi\to\psi</math>.
+Założmy teraz, że ostatnim krokiem w wyprowadzeniu formuły <math>\psi</math>
+jest zastosowanie reguły (MP) do formuł <math>\vartheta\to\psi</math> oraz
+<math>\vartheta</math>, dla pewnej formuły <math>\vartheta</math>.
+Z&nbsp;założenia indukcyjnego mamy <math>\Delta\vdash_H\varphi\to
+(\vartheta\to\psi)</math> oraz <math>\Delta\vdash_H\varphi\to\vartheta</math>.
+Stosując regułę odrywania do <math>\varphi\to
+(\vartheta\to\psi)</math> oraz do aksjomatu (A2):
+<math>(\varphi\to(\vartheta\to\psi))\to
+((\varphi\to\vartheta)\to(\varphi\to\psi))</math> dostajemy formułę
+<math>(\varphi\to\vartheta)\to(\varphi\to\psi)</math>. Ponownie stosując regułę
+odrywania
+do tej formuły oraz do <math>\varphi\to\vartheta</math> dostajemy żądaną formułę
+<math>\varphi\to\psi</math>. To kończy dowód twierdzenia o dedukcji.
+}}
+{{twierdzenie|5.3 (o poprawności)|popraw|
+Jeśli <math>\Delta\vdash_H\varphi</math>, to <math>\Delta\models\varphi</math>. W&nbsp;szczególności,
+jeśli <math>\vdash_H\varphi</math>, to <math>\varphi</math> jest tautologią.
+}}
+{{dowod|||
+Dowód jest indukcyjny ze względu na liczbę kroków w&nbsp;wyprowadzeniu
+formuły&nbsp;<math>\varphi</math> w systemie hilbertowskim ze zbioru hipotez
+<math>\Delta</math>. Jeśli dowód ten składa się tylko z jednego kroku, to albo
+<math>\varphi\in\Delta</math>, albo <math>\varphi</math> jest aksjomatem. W obu przypadkach
+oczywiście zachodzi <math>\Delta\models\varphi</math>.
+Załóżmy teraz, że <math>\varphi</math> jest otrzymana przez zastosowanie reguły odrywania
+do formuł <math>\psi\to\varphi</math> oraz&nbsp;<math>\psi</math>. Z założenia indukcyjnego mamy
+<center><math>
+\Delta\models\psi\to\varphi</math>  oraz  <math>\Delta\models\psi.
+\hspace{3cm}(1)
+</math></center>
+Niech <math>\varrho</math> będzie dowolnym wartościowaniem spełniającym wszystkie
+formuły z <math>\Delta</math>. Na mocy&nbsp; (1), wartościowanie
+<math>\varrho</math> spełnia
+<math>\psi\to\varphi</math> oraz spełnia <math>\psi</math>. Wynika stąd, że <math>\varrho</math> spełnia
+<math>\varphi</math>. Tym samym udowodniliśmy, że <math>\Delta\models\varphi</math>. To
+kończy dowód.
+}}
+{{lemat|5.4|lem5.4|
-Reguły dowodzenia opisuj± warunki, przy pomocy których można otrzymaćnowe wyrażenie \begin{eqnarray*}nazywane {\em konkluzj±}\end{eqnarray*} z otrzymanych już wyrażeń\begin{eqnarray*}nazywanych {\em przesłankami}\end{eqnarray*}. Dowody w&nbsp;systemach formalnych s±ci±gami wyrażeń, być może posiadaj±cymi dodatkow± strukturępozwalaj±c± na lepsz± wizualizację.
+Dla dowolnych formuł <math>\varphi,\psi</math> zbudowanych przy użyciu <math>\to</math>
+oraz <math>\bot</math>, następujące formuły są twierdzeniami systemu hilbertowskiego.
+# <math>\varphi \to(\neg\psi\to\neg(\varphi\to\psi))</math>;
+# <math>\bot\to\varphi</math>;
+# <math>(\varphi\to\psi)\to((\neg\varphi\to\psi)\to\psi)</math>;
+}}
-W dalszej czę¶ci opiszemy trzy systemy dowodzenia: system typuhilbertowskiego \begin{eqnarray*}od nazwiska Davida Hilberta\end{eqnarray*}, system naturalnej dedukcji oraz rachunek sekwentów. Ostatnie dwa systemy znajduj± zastosowanie w&nbsp;pewnych działach sztucznej inteligencji oraz w systemach automatycznego dowodzenia twierdzeń.
+{{dowod|||
+(1)&nbsp;
+Niech <math>\Delta=\{\varphi,\psi\to\bot,\varphi\to\psi\}</math>. Stosując regułę
+odrywania do formuł <math>\varphi</math> oraz <math>\varphi\to\psi</math> dostajemy&nbsp;<math>\psi</math>.
+Przez ponowne zastosowanie (MP) do tej formuły oraz do <math>\psi\to\bot</math>
+otrzymujemy
+wyprowadzenie <math>\bot</math>. Tym samym pokazaliśmy, że <math>\Delta\vdash_H\bot</math>. Stosując
+teraz trzy razy twierdzenie o dedukcji dostajemy
+<center><math>\vdash_H\varphi\to((\psi\to\bot)\to((\varphi\to\psi)\to\bot))</math>,</center>
+czyli
-Poniższy system dowodzenia dotyczy formuł zbudowanych przy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciujedynie spójnika <math>\arr</math>, stałej <math>\bot</math> oraz zmiennych zdaniowych.Przypomnijmy, że dladowolnej formuły <math>\var\varphi</math>, napis <math>\neg\var\varphi</math> jest skrótem zapisu<math>\var\varphi\arr\bot</math>. Symbole  <math>\var\varphi,\psi,\vartheta</math> w poniższym systemie oznaczaj± dowolne formuły.
+<center><math>\vdash_H\varphi \to(\neg\psi\to\neg(\varphi\to\psi))</math>.</center>
-\vspace{.3cm}\noindent'''Aksjomaty'''
+(2)&nbsp;
+Ponieważ <math>\{\bot,\neg\varphi\}\vdash_H\bot</math>, więc z twierdzenia o dedukcji
+wynika <math>\bot\vdash_H\neg\neg\varphi</math>.
+Stosując teraz&nbsp;(MP) do tej formuły oraz do aksjomatu
+(A3) w postaci <math>\neg\neg\varphi\to\varphi</math> otrzymujemy <math>\bot\vdash_H\varphi</math>.
+Ponowne zastosowanie twierdzenia o dedukcji daje nam <math>\vdash_H\bot\to\varphi</math>.
-\begin{eqnarray*}A1\end{eqnarray*} <math>\var\varphi\arr\begin{eqnarray*}\psi\arr\var\varphi\end{eqnarray*}</math>\\\begin{eqnarray*}A2\end{eqnarray*} </math>\begin{eqnarray*}\var\varphi\arr\begin{eqnarray*}\psi\arr\vartheta\end{eqnarray*}\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\arr\begin{eqnarray*}\var\varphi\arr\vartheta\end{eqnarray*}\end{eqnarray*}</math>\\\begin{eqnarray*}A3\end{eqnarray*} <math>\neg\neg\var\varphi\arr\var\varphi</math>
+(3)&nbsp;
+Niech <math>\Delta=\{\varphi\to\psi,\neg\varphi\to\psi\}</math>. Zaczynamy od zbioru
+hipotez <math>\Delta\cup\{\varphi,\neg\psi\}</math>. Stosując (MP) do formuł <math>\varphi</math>
+oraz <math>\varphi\to\psi</math> dostajemy <math>\psi</math>. Ponowne zastosowanie (MP) do tej
+formuły oraz do&nbsp;<math>\neg\psi</math> daje nam <math>\bot</math>. Używając teraz twierdzenia
+o&nbsp;dedukcji do formuły <math>\bot</math> otrzymujemy
-\vspace{.3cm}\noindent'''Reguła dowodzenia'''\\<span id=""/> <math> {\rm \begin{eqnarray*}MP\end{eqnarray*}}\hspace{1cm} \frac{\var\varphi\\hspace{1cm}
+<center><math>\Delta\cup\{\neg\psi\}\vdash_H\neg\varphi</math></center>
+Ponieważ mamy <math>\Delta\cup\{\neg\psi\}\vdash_H\neg\varphi\to\psi</math>, to stosując
+(MP) otrzymujemy <math>\Delta\cup\{\neg\psi\}\vdash_H\psi</math>. Jeszcze raz
+używamy (MP) aby z <math>\neg\psi</math> i <math>\psi</math> otrzymać <math>\bot</math> i mamy
+<center><math>\Delta\cup\{\neg\psi\}\vdash_H\bot</math></center>
-</math>
+Na mocy twierdzenia o dedukcji <math>\Delta\vdash_H\neg\neg\psi</math>.
+Stosując (MP) do formuły <math>\neg\neg\psi</math>
+oraz do aksjomatu <math>\neg\neg\psi\to\psi</math>
+otrzymujemy <math>\Delta\vdash_H\psi</math>. Dwukrotne zastosowanie twierdzenia
+o dedukcji daje nam
+<math>\vdash_H(\varphi\to\psi)\to((\neg\varphi\to\psi)\to\psi)</math>.
+To kończy dowód lematu.
+}}
-Reguła \begin{eqnarray*}MP\end{eqnarray*} jest nazywana {\em reguł± odrywania} lub teżreguł± {\em modus ponens}.
+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.
-\textit{Dowodem} w powyższym systemie nazywamy taki ci±g formuł, w którymkażda formuła albo jest aksjomatem, albo też została otrzymana z&nbsp;wcze¶niej występuj±cych formuł w wyniku zastosowania reguły odrywania. Powiemy, że formuła <math>\var\varphi</math> ''ma dowód\/}, lub jest \textit{twierdzeniem''systemu hilbertowskiego, co zapiszemy <math>\vdash_H\var\varphi</math>,gdy istnieje dowód zawieraj±cy <math>\var\varphi</math>. Powyższ± definicję możemynieco\boldsymbol{s}}\def\blank{\hbox{\sf Bogólnić. Niech <math>\Delta</math> będzie dowolnym zbioremformuł. Powiemy, że formuła <math>\var\varphi</math> ma dowód ze zbioru hipotez <math>\Delta</math> \begin{eqnarray*}notacja <math>\Delta\vdash_H\var\varphi</math>\end{eqnarray*}, gdy <math>\var\varphi</math> jest twierdzeniem systemu, w&nbsp;którym zbiór aksjomatów został poszerzony o formuły ze zbioru <math>\Delta</math>.
+<math>(B1)\ \ \   \varphi\wedge \psi\to\neg(\varphi\to\neg\psi)</math><br>
+<math>(B2)\ \ \   \neg(\varphi\to\neg\psi)\to\varphi\wedge \psi</math><br>
+<math>(B3)\ \ \   \varphi\vee\psi\to(\neg\varphi\to\psi)</math><br>
+<math>(B4)\ \ \   (\neg\varphi\to\psi)\to\varphi\vee\psi</math>
-{{przyklad||pr-zda-1a|
+Tak otrzymany system oznaczymy przez <math>\vdash_{H^+}</math>.
+{{twierdzenie|5.5 (o poprawności dla <math>\vdash_{H^+}</math>)||
+Dla dowolnego zbioru formuł <math>\Delta</math> i dla dowolnej formuły <math>\varphi</math>
+w języku z <math>\vee,\wedge,\arr,\bot</math>,
+jeśli <math>\se_{H^+}\varphi</math> to <math>\Delta\models\varphi</math>.
+}}
-Niech <math>p</math> będzie zmienn± zdaniow±. Pokażemy, że formuła <math>p\arr p</math> 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.
+{{dowod|||
-#<math>\begin{eqnarray*}p\arr\begin{eqnarray*}\begin{eqnarray*}p\arr p\end{eqnarray*}\arr p\end{eqnarray*}\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}p\arr\begin{eqnarray*}p\arr p\end{eqnarray*}\end{eqnarray*}\arr\begin{eqnarray*}p\arr p\end{eqnarray*}\end{eqnarray*}</math> \\hspace{1cm} \begin{eqnarray*}A2\end{eqnarray*}
+Wystarczy sprawdzić, że aksjomaty (B1)-(B4) są tautologiami.
-#<math>p\arr\begin{eqnarray*}\begin{eqnarray*}p\arr p\end{eqnarray*}\arr p\end{eqnarray*}</math> \\hspace{1cm} \begin{eqnarray*}A1\end{eqnarray*}
+Konkluzja wynika
-#<math>\begin{eqnarray*}p\arr\begin{eqnarray*}p\arr p\end{eqnarray*}\end{eqnarray*}\arr\begin{eqnarray*}p\arr p\end{eqnarray*}</math> \\hspace{1cm} \begin{eqnarray*}1,2\end{eqnarray*}
+z &nbsp;[[#popraw|Twierdzenia 5.3]] o poprawności dla <math>\vdash_H</math>.
-#<math>p\arr\begin{eqnarray*}p\arr p\end{eqnarray*}</math> \\hspace{1cm} \begin{eqnarray*}A1\end{eqnarray*}
-#<math>p\arr p</math> \\hspace{1cm} \begin{eqnarray*}3,4\end{eqnarray*}
 }}
-Zauważmy, że w powyższym przykładzie możemy wszędzie zast±pićzmienn± <math>p</math> przez dowoln± formułę <math>\var\varphi</math> dostaj±c dowód formuły<math>\var\varphi\arr\var\varphi</math>.
+{{lemat|5.6||
+Dla dowolnej formuły <math>\varphi</math> istnieje formuła <math>\tilde{\varphi}</math>
+zbudowana przy użyciu jedynie <math>\to</math> oraz&nbsp;<math>\bot</math>, taka że
+<math>\vdash_{H^+}\varphi\to\tilde{\varphi}</math> oraz
+<math>\vdash_{H^+}\tilde{\varphi}\to\varphi</math>.
+}}
-Następuj±ce twierdzenie jest bardzo\boldsymbol{s}}\def\blank{\hbox{\sf Bżyteczne, gdy trzeba\boldsymbol{s}}\def\blank{\hbox{\sf Bzasadnić,że jaka¶ formuła jest twierdzeniem.
+{{dowod|||
+W danej formule <math>\varphi</math>, zastąpmy każdą podformułę postaci
+<math>\psi\wedge\vartheta</math> formułą <math>\neg(\psi\to\neg\vartheta)</math> oraz
+każdą podformułę postaci <math>\psi\vee\vartheta</math> formułą
+<math>\neg\psi\to\vartheta</math>. Aksjomaty (B1)-(B4) mówią, że zastąpione
+formuły są równoważne. Tak więc łatwo dostajemy
+<math>\vdash_{H^+}\varphi\to\tilde{\varphi}</math> oraz
+<math>\vdash_{H^+}\tilde{\varphi}\to\varphi</math>. Szczegóły dowodu pozostawimy
+Czytelnikowi.
+}}
+{{kotwica|sekcja5.2|}}
-{{twierdzenie||tw-zad-1|
+===System naturalnej dedukcji===
+System naturalnej dedukcji (wprowadzony przez S.&nbsp;Jaśkowskiego
+i G.&nbsp;Gentzena) operuje wyrażeniami zwanymi ''sekwentami''.
+Są to wyrażenia postaci <math>\Delta\vdash\varphi</math>, gdzie <math>\Delta</math> jest
+pewnym skończonym zbiorem formuł, a <math>\varphi</math> 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 <math>\vdash</math>
+(tj.&nbsp;wywnioskować formułę danego kształtu).
+''Reguły eliminacji'' mówią o tym, w jakiej sytuacji można
+ten spójnik wyeliminować, tzn.&nbsp;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 <math>\bot</math>. Pamiętajmy, że <math>\neg\varphi</math> oznacza formułę
+<math>\varphi\to\bot</math>.
+Poniżej będziemy stosować następującą konwencję:
+Napis <math>\Delta,\varphi_1,\ldots,\varphi_n</math> oznacza zbiór
+<math>\Delta\cup\{\varphi_1,\ldots,\varphi_n\}</math>,
+przy czym nie zakładamy tu, że <math>\varphi_i\not\in\Delta</math>.
-Dla dowolnego zbioru formuł <math>\Delta</math> oraz dowolnych formuł <math>\var\varphi,\psi</math>,je¶li <math>\Delta\cup\{\var\varphi\}\vdash_H\psi</math>, to \mbox{<math>\Delta\vdash_H\var\varphi\arr\psi</math>}.}}
+'''Aksjomat'''
-{{dowod||
+<math>(A0)\ \ \ \Delta,\varphi\vdash\varphi</math>
-Dowód jest indukcyjny ze względu na liczbę kroków w dowodzie formuły<math>\psi</math> ze zbioru hipotez <math>\Delta\cup\{\var\varphi\}</math>. Przypu¶ćmy najpierw, że dowód tenskłada się tylko z jednego kroku. Je¶li <math>\psi=\var\varphi</math>, to stosuj±c wyprowadzenie z Przykładu&nbsp;[[#pr-zda-1a]] dostajemy dowódformuły <math>\var\varphi\arr\var\varphi</math>. Możemy oczywi¶cie przyj±ć, że formuła tajest wyprowadzona ze zbioru hipotez <math>\Delta</math>. Druga możliwo¶ć jest taka, że<math>\psi\in\Delta</math> lub też, że <math>\psi</math> jest aksjomatem. W każdym z tychprzypadków mamy <math>\Delta\vdash_H\psi</math>. Wówczas stosuj±c regułęodrywania do <math>\psi</math> oraz aksjomatu <math>\psi\arr\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}</math>dostajemy formułę <math>\var\varphi\arr\psi</math>.
+'''Reguły dowodzenia'''
-Założmy teraz, że ostatnim krokiem w wyprowadzeniu formuły <math>\psi</math> jest zastosowanie reguły \begin{eqnarray*}MP\end{eqnarray*} do formuł <math>\vartheta\arr\psi</math> oraz<math>\vartheta</math>, dla pewnej formuły <math>\vartheta</math>. Z&nbsp;założenia indukcyjnego mamy </math>\Delta\vdash_H\var\varphi\arr\begin{eqnarray*}\vartheta\arr\psi\end{eqnarray*}</math> oraz <math>\Delta\vdash_H\var\varphi\arr\vartheta</math>. Stosuj±c regułę odrywania do </math>\var\varphi\arr\begin{eqnarray*}\vartheta\arr\psi\end{eqnarray*}</math> oraz do aksjomatu \begin{eqnarray*}A2\end{eqnarray*}:  </math>\begin{eqnarray*}\var\varphi\arr\begin{eqnarray*}\vartheta\arr\psi\end{eqnarray*}\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}\var\varphi\arr\vartheta\end{eqnarray*}\arr\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\end{eqnarray*}</math> dostajemy formułę <math>\begin{eqnarray*}\var\varphi\arr\vartheta\end{eqnarray*}\arr\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}</math>. Ponownie stosuj±c regułę odrywania do tej formuły oraz do <math>\var\varphi\arr\vartheta</math> dostajemy ż±dan± formułę <math>\var\varphi\arr\psi</math>. \Rightarrow kończy dowód twierdzenia o dedukcji.}}
+<center><math>(\to</math> -intro <math>) \hspace{.2cm}
+\frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\to\psi}
+\hspace{1cm} (\to</math> -elim <math>) \hspace{.2cm}
+\frac{\Delta\vdash\varphi\to\psi\qquad
+\Delta\vdash\varphi}{\Delta\vdash\psi}</math></center>
-{{twierdzenie||tw-zda-2|
+<center><math>(\wedge</math> -intro <math>)\hspace{.2cm} \frac{\Delta\vdash\varphi\qquad
+\Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi} \hspace{1cm}
+(\wedge</math> -elim <math>)
+\hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi}
+\hspace{1cm}
+(\wedge</math> -elim <math>)
+\hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}</math></center>
-Je¶li <math>\Delta\vdash_H\var\varphi</math>, to <math>\Delta\models\var\varphi</math>. W&nbsp;szczególno¶ci, je¶li <math>\vdash_H\var\varphi</math>, to <math>\var\varphi</math> jest tautologi±.}}
+<center><math>(\vee</math> -intro <math>)\hspace{.2cm}
+\frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm}
+(\vee</math> -intro <math>)\hspace{.2cm}
+\frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi}</math></center>
-{{dowod|eq-zad-1|
-Dowód jest indukcyjny ze względu na liczbę kroków w&nbsp;wyprowadzeniu formuły&nbsp;<math>\var\varphi</math> w systemie hilbertowskim ze zbioru hipotez <math>\Delta</math>. Je¶li dowód ten składa się tylko z jednego kroku to albo <math>\var\varphi\in\Delta</math> albo <math>\var\varphi</math> jest aksjomatem. W obu przypadkach oczywi¶cie zachodzi <math>\Delta\models\var\varphi</math>.
+<center><math>(\vee</math> -elim <math>)\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\qquad
+\Delta,\varphi\vdash\vartheta\qquad
+\Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}</math></center>
-Załóżmy teraz, że <math>\var\varphi</math> jest otrzymana przez zastosowanie reguły odrywania do formuł <math>\psi\arr\var\varphi</math> oraz&nbsp;<math>\psi</math>. Z założeniaindukcyjnego mamy<!--%-->
-\Delta\models\psi\arr\var\varphi \mbox{ oraz } \Delta\models\psi.\end{equation}Niech <math>\varrho</math> będzie dowolnym warto¶ciowaniem spełniaj±cym wszystkieformuły z <math>\Delta</math>. Na mocy&nbsp;\begin{eqnarray*}[[#eq-zad-1]]\end{eqnarray*}, warto¶ciowanie<math>\varrho</math> spełnia <math>\psi\arr\var\varphi</math> oraz spełnia <math>\psi</math>. Wynika st±d, że <math>\varrho</math> spełnia<math>\var\varphi</math>. Tym samym\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnili¶my, że <math>\Delta\models\var\varphi</math>. \Rightarrowkończy dowód.}}
+<center><math>(</math> PS <math>)\hspace{.2cm}
+\frac{\Delta,\neg\varphi\vdash\bot}{\Delta\vdash\varphi}</math></center>
+Zauważmy, że szczególnym przypadkiem reguły (<math>\to</math> -intro) jest
+następująca reguła, można ją traktować jak regułę wprowadzenia negacji.
+<center><math>\frac{\Delta,\varphi\vdash\bot}
+{\Delta\vdash\neg\varphi}</math></center>
+Zauważmy też, że szczególnym przypadkiem reguły (<math>\to</math> -elim) jest
+następująca reguła, można ją traktować jak regułę eliminacji negacji.
-\begin{lemat} <span id="le-zda-1" \> Dla dowolnych formuł <math>\var\varphi,\psi</math> zbudowanych przy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciu <math>\arr</math>oraz <math>\bot</math>, następuj±ce formuły s± twierdzeniami systemu hilbertowskiego.
+<center><math>\frac{\Delta\vdash\neg\varphi\quad
+\Delta\vdash\varphi}{\Delta\vdash\bot}</math></center>
+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
+<math>\Delta\vdash\varphi</math> w systemie naturalnej dedukcji nazwiemy drzewo
+etykietowane sekwentami tak, że korzeń ma etykietę
+<math>\Delta\vdash\varphi</math>, 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 <math>\Delta\vdash_{N}\varphi</math>, gdy sekwent
+<math>\Delta\vdash\varphi</math> ma dowód w&nbsp;systemie
+naturalnej dedukcji. Gdy <math>\Delta=\emptyset</math>, to mówimy też,
+że <math>\varphi</math> jest ''twierdzeniem'' systemu naturalnej dedukcji
+i zapisujemy to przez <math>\vdash_N\varphi</math>.
+Jeśli <math>\Delta</math> jest zbiorem nieskończonym, to
+<math>\Delta\vdash_{N}\varphi</math> oznacza, że istnieje dowód sekwentu
+<math>\Delta_0\vdash\varphi</math>, dla pewnego skończonego <math>\Delta_0\subseteq\Delta</math>.
-#<span id="le-1" \>  <math>\var\varphi \arr\begin{eqnarray*}\neg\psi\arr\neg\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\end{eqnarray*}</math>;
+Poniżej podajemy kilka przykładów dowodów w systemie naturalnej
-#<span id="le-2" \> <math>\bot\arr\var\varphi</math>;
+dedukcji.
-#<span id="le-3" \> <math>\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}\arr\psi\end{eqnarray*}</math>;
-\end{lemat}
-{{dowod||
+{{przyklad|5.7|przyk5.7|
+* Pokażemy <math>\vdash_{N}p\to p</math>.
-\begin{eqnarray*}1\end{eqnarray*}&nbsp; Niech <math>\Delta=\{\var\varphi,\psi\arr\bot,\var\varphi\arr\psi\}</math>. Stosuj±c regułę odrywania do formuł <math>\var\varphi</math> oraz <math>\var\varphi\arr\psi</math> dostajemy&nbsp;<math>\psi</math>. Przez ponowne zastosowanie \begin{eqnarray*}MP\end{eqnarray*} do tej formuły oraz do <math>\psi\arr\bot</math> otrzymujemy wyprowadzenie <math>\bot</math>. Tym samym pokazali¶my, że <math>\Delta\vdash_H\bot</math>. Stosuj±c teraz trzy razy twierdzenie o dedukcji dostajemy\[\vdash_H\var\varphi\arr\begin{eqnarray*}\begin{eqnarray*}\psi\arr\bot\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\arr\bot\end{eqnarray*}\end{eqnarray*},\]czyli\[\vdash_H\var\varphi \arr\begin{eqnarray*}\neg\psi\arr\neg\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\end{eqnarray*}.\]
+<center><math>\frac{p\vdash p}{\vdash p\to p}(\to\ -intro)
+</math></center>
+* Pokażemy <math>\vdash_{N} p\to(q\to p)</math>.
-\begin{eqnarray*}2\end{eqnarray*}&nbsp; Ponieważ <math>\{\bot,\neg\var\varphi\}\vdash_H\bot</math>, więc z twierdzenia o dedukcjiwynika <math>\bot\vdash_H\neg\neg\var\varphi</math>. Stosuj±c teraz&nbsp;\begin{eqnarray*}MP\end{eqnarray*} do tej formuły oraz do aksjomatu \begin{eqnarray*}A3\end{eqnarray*} w postaci <math>\neg\neg\var\varphi\arr\var\varphi</math> otrzymujemy <math>\bot\vdash_H\var\varphi</math>. Ponowne zastosowanie twierdzenia o dedukcji daje nam <math>\vdash_H\bot\arr\var\varphi</math>.
+<center><math>\frac{\frac{p,q\vdash p}{p\vdash q\to p}(\to-intro)}{\vdash p\to (q\to p)}(\to -intro)
+</math></center>
+* Pokażemy <math>\vdash_{N}\neg\neg p\to p</math>.
-\begin{eqnarray*}3\end{eqnarray*}&nbsp;Niech <math>\Delta=\{\var\varphi\arr\psi,\neg\var\varphi\arr\psi\}</math>. Zaczynamy od zbioru hipotez <math>\Delta\cup\{\var\varphi,\neg\psi\}</math>. Stosuj±c \begin{eqnarray*}MP\end{eqnarray*} do formuł <math>\var\varphi</math> oraz <math>\var\varphi\arr\psi</math> dostajemy <math>\psi</math>. Ponowne zastosowanie \begin{eqnarray*}MP\end{eqnarray*} do tej formuły oraz do&nbsp;<math>\neg\psi</math> daje nam <math>\bot</math>. Używaj±c teraz twierdzeniao&nbsp;dedukcji do formuły <math>\bot</math> otrzymujemy\[\Delta\cup\{\neg\psi\}\vdash_H\neg\var\varphi.\]Ponieważ mamy <math>\Delta\cup\{\neg\psi\}\vdash_H\neg\var\varphi\arr\psi</math>, to stosuj±c \begin{eqnarray*}MP\end{eqnarray*} otrzymujemy <math>\Delta\cup\{\neg\psi\}\vdash_H\psi</math>. Jeszcze raz używamy \begin{eqnarray*}MP\end{eqnarray*} aby z <math>\neg\psi</math> i <math>\psi</math> otrzymać <math>\bot</math> i mamy<!--%-->\[\Delta\cup\{\neg\psi\}\vdash_H\bot.\]Na mocy twierdzenia o dedukcji <math>\Delta\vdash_H\neg\neg\psi</math>. Stosuj±c \begin{eqnarray*}MP\end{eqnarray*} do formuły <math>\neg\neg\psi</math> oraz do aksjomatu <math>\neg\neg\psi\arr\psi</math> otrzymujemy <math>\Delta\vdash_H\psi</math>. Dwukrotne zastosowanie twierdzenia o dedukcji daje nam <math>\vdash_H\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}\arr\psi\end{eqnarray*}</math>. \Rightarrow kończy dowód lematu.}}
+<center><math>
+\frac{\neg\neg p,\neg p\vdash\neg\neg p\qquad\neg\neg p,\neg p\vdash\neg p}
+{\frac{\neg\neg p,\neg p\vdash p}{\frac{\neg\neg p\vdash p}{\vdash \neg\neg p\to p}
+(\to -\ intro)}(PS)}(\to -\ elim)
+</math></center>
+}}
-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.
+{{twierdzenie|5.8||
-\noindent\begin{eqnarray*}B1\end{eqnarray*}&nbsp; <math>  \var\varphi\wedge \psi\arr\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}</math>\\\begin{eqnarray*}B2\end{eqnarray*}&nbsp; <math>  \neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\arr\var\varphi\wedge \psi</math>\\\begin{eqnarray*}B3\end{eqnarray*}&nbsp; <math>  \var\varphi\vee\psi\arr\begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}</math>\\\begin{eqnarray*}B4\end{eqnarray*}&nbsp; <math>  \begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}\arr\var\varphi\vee\psi</math>
+Dla dowolnego sekwentu <math>\Delta\vdash\varphi</math> mamy następującą
+równoważność:
-Tak otrzymany system oznaczymy przez <math>\vdash_{H^+}</math>.
+<center><math>\Delta\vdash_{N}\varphi\hspace{.2cm}</math>, gdy <math>\hspace{.2cm}
+\Delta\vdash_{H^+}\varphi</math>.</center>
+}}
+Aby pokazać, że każdy dowód w <math>\vdash_{N}</math> daje się przerobić
+na dowód w <math>\vdash_{H^+}</math> wystarczy sprawdzić, że każda z reguł
+systemu naturalnej dedukcji jest ''dopuszczalna'' w <math>H^+</math>.
+Tzn.&nbsp;wystarczy sprawdzić, że jeśli mamy dowody przesłanek w&nbsp;<math>\vdash_{H^+}</math>,
+to możemy udowodnić konkluzję. Zauważmy, że wyprowadzalność reguły(<math>\to -</math> intro) jest konsekwencją twierdzenia
+o dedukcji, natomiast reguła (<math>\to -</math> elim) jest regułą&nbsp;(MP).
+Przykładowo pokażemy wyprowadzenie (<math>\vee -</math> elim) oraz (PS) w&nbsp;<math>H^+</math>,
+pozostawiając Czytelnikowi wyprowadzenie pozostałych reguł.
+Załóżmy, że mamy w <math>H^+</math> dowody następujących sekwentów:
+<math>\Delta\vdash\varphi\vee\psi</math>, {.1cm}
+<math>\Delta,\varphi\vdash\vartheta</math> {.1cm}oraz {.1cm}
+<math>\Delta,\psi\vdash\vartheta</math>. Wówczas,
+stosując aksjomat (B2) i regułę (MP) mamy
+<math>\Delta\vdash_{H^+}\neg\varphi\to\psi</math>.
+Zatem <math>\Delta,\neg\varphi\vdash_{H^+}\psi</math> i ponieważ
+<math>\Delta\vdash_{H^+}\psi\to\vartheta</math> to również
+<math>\Delta,\neg\varphi\vdash_{H^+}\psi\to\vartheta</math>. Stąd
+<math>\Delta,\neg\varphi\vdash_{H^+}\vartheta</math>. Stosując twierdzenie o dedukcji
+dostajemy <math>\Delta\vdash_{H^+}\neg\varphi\to\vartheta</math>. Skoro mamy również
+<math>\delta\vdash_{H^+}\varphi\to\vartheta</math>, to na mocy
+&nbsp;[[#lem5.4|Lematu 5.4]] (3) otrzymujemy <math>\Delta\vdash_{H^+}\vartheta</math>.
+Dla wyprowadzenia (PS) załóżmy, że
+<math>\Delta,\neg\varphi\vdash_{H^+}\bot</math>. Z twierdzenia o dedukcji
+dostajemy <math>\Delta\vdash_{H^+}\neg\neg\varphi</math>. Tak więc z
+(A3) i (MP) dostajemy <math>\Delta\vdash_{H^+}\varphi</math>.
+Dla pokazania implikacji odwrotnej wystarczy pokazać, że wszystkie
+aksjomaty systemu <math>H^+</math> są twierdzeniami systemu naturalnej dedukcji.
+Wyprowadzenia (A1) i
+(A3) w ND zostały podane w &nbsp;[[#przyk5.7|Przykładzie 5.7]]. Przykładowo pokażemy
+wyprowadzenia
+(A2) i (B1). Zaczniemy od wyprowadzenia (A2). Niech
+<math>\Delta=\{\varphi\to(\psi\to\vartheta),\ \varphi\to\psi,\ \varphi\}</math>.
+Mamy następujący dowód:
+<center><math>
+\frac{
+\frac{\Delta\vdash\varphi\to(\psi\to\vartheta)\qquad\Delta\vdash\varphi}{\Delta\vdash\psi\to\vartheta}
+(\to -\ elim)\qquad
+\frac{\Delta\vdash\varphi\to\psi\qquad\Delta\vdash\varphi}{\Delta\vdash\psi}(\to -\ elim)
+}{\Delta\vdash\vartheta}(\to -\ elim)
+</math></center>
+Stosując trzy razy (<math>\to</math> -intro ) do sekwentu <math>\Delta\vdash\vartheta</math> dostajemy wyprowadzenie aksjomatu (A2).
+Następnie pokażemy dowód (B1) w ND.  Zaczniemy od
+wyprowadzenia <math>\neg(\varphi\to\neg\psi)\vdash\varphi</math>, gdzie
+<math>\Delta=\{\neg(\varphi\to\neg\psi), \neg\varphi\}</math>:
+<center><math>
+\frac{
+\frac{
+\frac{
+\frac{\Delta,\varphi,\psi\vdash\neg\varphi \qquad \Delta,\varphi,\psi\vdash\varphi}{\Delta,\varphi,\psi\vdash\bot}(\to -\ elim)}
+{\Delta,\varphi\vdash\neg\psi}(\to -\ intro)}
+{\Delta\vdash\varphi\to\neg\psi}(\to -\ intro)\qquad \Delta\vdash\neg(\varphi\to\neg\psi)}
+{\frac{\Delta\vdash\bot}{\neg(\varphi\to\neg\psi)\vdash\varphi}(PS)}(\to -\ elim)
+</math></center>
+Następnie wyprowadzimy sekwent <math>\neg(\varphi\to\neg\psi)\vdash\psi</math>. Niech
+<math>\Delta=\{\neg(\varphi\to\neg\psi), \neg\psi\}</math>
-{{twierdzenie||poprawnosc|
+<center><math>
+\frac{
+\frac{\Delta,\varphi\vdash\neg\psi}
+{\Delta\vdash\varphi\to\neg\psi}(\to -\ intro)\qquad \Delta\vdash\neg(\varphi\to\neg\psi)}
+{\frac{\Delta\vdash\bot}{\neg(\varphi\to\neg\phi)\vdash\phi}(PS)}(\to -\ elim)
+</math></center>
-Dla dowolnego zbioru formuł <math>\Delta</math> i dla dowolnej formuły <math>\var\varphi</math>w języku z <math>\vee,\wedge,\arr,\bot</math>,je¶li <math>\se_{H^+}\var\varphi</math> to <math>\Delta\models\var\varphi</math>.}}
+Mając wyprowadzone sekwenty <math>\neg(\varphi\to\neg\psi)\vdash\varphi</math>
+oraz <math>\neg(\varphi\to\neg\psi)\vdash\psi</math>, możemy zakończyć dowód&nbsp;(B1).
-{{dowod||
-Wystarczy sprawdzić, że aksjomaty \begin{eqnarray*}B1\end{eqnarray*}--\begin{eqnarray*}B4\end{eqnarray*} s± tautologiami. Konkluzja wynika z Twierdzenia&nbsp;[[#tw-zda-2]] o poprawno¶ci dla <math>\vdash_H</math>.}}
+<center><math>
+\frac{\neg(\varphi\to\neg\psi)\vdash\varphi\qquad \neg(\varphi\to\neg\psi)\vdash\psi}
+{\frac{\neg(\varphi\to\neg\psi)\vdash\varphi\wedge\psi}
+{\vdash\neg(\varphi\to\neg\psi)\to(\varphi\wedge\psi)}(\to-\ intro)}(\wedge -\ intro)
-\begin{lemat} <span id="le-zda-2a" \> Dla dowolnej formuły <math>\var\varphi</math> istnieje formuła <math>\tilde{\var\varphi}</math>zbudowana przy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciu jedynie <math>\arr</math> oraz&nbsp;<math>\bot</math>, taka że<math>\vdash_{H^+}\var\varphi\arr\tilde{\var\varphi}</math>\hspace{.1cm} oraz \hspace{.1cm}<math>\vdash_{H^+}\tilde{\var\varphi}\arr\var\varphi</math>. \end{lemat}
+</math></center>
+{{kotwica|sekcja5.3|}}
-{{dowod||
+===Rachunek sekwentów===
-W danej formule <math>\var\varphi</math>, zast±pmy każd± podformułę postaci <math>\psi\wedge\vartheta</math> formuł± <math>\neg\begin{eqnarray*}\psi\arr\neg\vartheta\end{eqnarray*}</math> orazkażd± podformułę postaci <math>\psi\vee\vartheta</math> formuł±<math>\neg\psi\arr\vartheta</math>. Aksjomaty \begin{eqnarray*}B1\end{eqnarray*}--\begin{eqnarray*}B4\end{eqnarray*} mówi±, że zast±pioneformuły s± równoważne. Tak więc łatwo dostajemy<math>\vdash_{H^+}\var\varphi\arr\tilde{\var\varphi}</math> oraz<math>\vdash_{H^+}\tilde{\var\varphi}\arr\var\varphi</math>. Szczegóły dowodu pozostawimyCzytelnikowi. }}
+Dla przedstawienia rachunku sekwentów rozszerzymy nieco pojęcie
+sekwentu. Przez ''sekwent'' będziemy teraz rozumieć napis
+<math>\Delta\vdash\Gamma</math>, gdzie <math>\Delta</math> oraz <math>\Gamma</math> są skończonymi
+zbiorami formuł. Intuicyjnie, wyprowadzalność  sekwentu
+<math>\Delta\vdash\Gamma</math> w rachunku sekwentów będzie oznaczać, że
+alternatywa formuł z <math>\Gamma</math> wynika z&nbsp;hipotez <math>\Delta</math>.
+Podobnie jak w poprzedniej części, rozważamy formuły,
+zbudowane w oparciu o spójniki <math>\to,\vee,\wedge</math> oraz stałą
+zdaniową <math>\bot</math>. Negację <math>\neg</math> traktujemy jako spójnik zdefiniowany przez <math>\to</math> i&nbsp;<math>\bot</math>.
+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
+<math>\vdash</math>, a druga grupa jest odpowiedzialna za wprowadzanie spójnika na
+prawo od <math>\vdash</math>. Dla każdego spójnika mamy odpowiadającą parę reguł.
+Aksjomat (A<math>\bot</math>) można traktować jako regułę (bez
+przesłanek) wprowadzenia <math>\bot</math> z lewej strony znaku <math>\vdash</math>.
-System naturalnej dedukcji \begin{eqnarray*}wprowadzony przez S.&nbsp;Ja¶kowskiego i G.&nbsp;Gentzena\end{eqnarray*} operuje wyrażeniami zwanymi \textit{sekwentami}. S± to wyrażenia postaci <math>\Delta\vdash\var\varphi</math>, gdzie <math>\Delta</math> jest pewnym skończonym zbiorem formuł, a <math>\var\varphi</math> jest formuł±. W odróżnieniu od systemuhilbertowskiego, w naturalnej dedukcji istotne s± reguły dowodzenia,a aksjomat jest bardzo prosty. Charakterystyczn± cech± naturalnej dedukcji jest to, że reguły dowodzenia \begin{eqnarray*}za wyj±tkiem reguły \begin{eqnarray*}PS\end{eqnarray*} ,,przez sprzeczno¶ć''\end{eqnarray*} s± podzielone na grupy, po jednej dla każdego spójnika. W ramach jednej takiej grupy mamy dwa rodzaje reguł. {\em Reguły  wprowadzania} mówi± o tym w jakiejsytuacji można wprowadzić dany spójnik na prawo od znaku <math>\vdash</math>\begin{eqnarray*}tj.&nbsp;wywnioskować formułę danego kształtu\end{eqnarray*}.{\em Reguły\Delta\vdashliminacji} mówi± o tym w jakiej sytuacji możnaten spójnik wyeliminować, tzn.&nbsp;jak można\boldsymbol{s}}\def\blank{\hbox{\sf Bżyć formuły zbudowanej z jegopomoc± do wyprowadzenia innej formuły. Regułę dowodzenia ,,przez sprzeczno¶ć'' można traktować jako ,,siln±'' regułęeliminacji <math>\bot</math>. Pamiętajmy, że <math>\neg\var\varphi</math> oznacza formułę<math>\var\varphi\arr\bot</math>.
+Przypomnijmy, że napis <math>\Delta,\varphi_1,\ldots,\varphi_n</math>
+oznacza zbiór <math>\Delta\cup\{\varphi_1,\ldots,\varphi_n\}</math>.
-Poniżej będziemy stosować następuj±c± konwencję: Napis <math>\Delta,\var\varphi_1,\ldots,\var\varphi_n</math> oznacza zbiór <math>\Delta\cup\{\var\varphi_1,\ldots,\var\varphi_n\}</math>, przy czym nie zakładamy tu, że <math>\var\varphi_i\not\in\Delta</math>.
+'''Aksjomaty'''
-\vspace{.3cm}\noindent'''Aksjomat'''
+<math>(A00)\ \ \ \Delta,\varphi\vdash\Gamma,\varphi</math>
-\begin{eqnarray*}A0\end{eqnarray*}&nbsp; <math>\Delta,\var\varphi\vdash\var\varphi</math>
+<math>(A\bot)\ \ \ \Delta,\bot\vdash\Gamma</math>
-\vspace{.4cm}\noindent'''Reguły dowodzenia'''
+'''Reguły dowodzenia'''<br>
-<span id=""/> <math> \begin{eqnarray*}\arr\mbox{-intro}\end{eqnarray*} \hspace{.2cm}
+<center><math>(\to</math> -lewa <math>)\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi\qquad
+\Delta,\psi\vdash\Gamma}{\Delta,\varphi\to\psi\vdash\Gamma}
+\hspace{1cm}(\to</math> -prawa <math>)\hspace{.2cm}
+\frac{\Delta,\varphi\vdash\Gamma,\psi}{\Delta\vdash\Gamma,
+\varphi\to\psi}</math></center>
+<center><math>(\wedge</math> -lewa <math>)\hspace{.2cm}
+\frac{\Delta,\varphi,\psi\vdash\Gamma}{\Delta,\varphi\wedge\psi\vdash\Gamma}
+\hspace{1cm} (\wedge</math> -prawa <math>)\hspace{.2cm}
+\frac{\Delta\vdash\Gamma, \varphi\qquad
+\Delta\vdash\Gamma,\psi}{\Delta\vdash \Gamma,\varphi\wedge\psi}</math></center>
-\fra\prooftree \Delta,\var\varphi\vdash\psi \justifies \Delta\vdash\var\varphi\arr\psi \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\hspace{1cm} \begin{eqnarray*}\arr\mbox{-elim}\end{eqnarray*} \hspace{.2cm}\frac{\Delta\vdash\var\varphi\arr\psi\\hspace{1cm}</math>
-<span id=""/> <math> \begin{eqnarray*}\wedge\mbox{-intro}\end{eqnarray*}\hspace{.2cm} \frac{\Delta\vdash\var\varphi\\hspace{1cm}
+<center><math>(\vee</math> -lewa <math>)\hspace{.2cm} \frac{\Delta,
+\varphi\vdash\Gamma\qquad
+\Delta,\psi\vdash\Gamma}{\Delta, \varphi\vee\psi \vdash\Gamma}
+\hspace{1cm} (\vee</math> -prawa <math>)\hspace{.2cm}
+\frac{\Delta\vdash\Gamma, \varphi, \psi}{\Delta\vdash\Gamma,
+\varphi\vee\psi}</math></center>
+''Dowodem'' sekwentu <math>\Delta\vdash\Gamma</math>, tak jak poprzednio,
+nazywamy drzewo etykietowane sekwentami tak, że korzeń jest
+etykietowany przez <math>\Delta\vdash\Gamma</math>, 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
+<math>\Delta\vdash\Gamma</math> w rachunku sekwentów to zapisujemy to tak:
+<math>\Delta\vdash_G\Gamma</math>. (Litera G pochodzi od nazwiska twórcy tego
+systemu, G.&nbsp;Gentzena.) Piszemy też <math>\Delta\vdash_{G}\varphi</math>, gdy&nbsp;<math>\Delta</math>
+jest nieskończony, ale  <math>\Delta\vdash_G\varphi</math>
+dla pewnego skończonego <math>\Delta_0 \subseteq\Delta</math>.
-\Delta\vdash\psi}{\Delta\vdash\var\varphi\wedge\psi} \hspace{1cm}\begin{eqnarray*}\wedge\mbox{-elim}\end{eqnarray*}\hspace{.2cm}\fra\prooftree \Delta\vdash\var\varphi\wedge\psi \justifies \Delta\vdash\var\varphi \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\hspace{1cm} \begin{eqnarray*}\wedge\mbox{-elim}\end{eqnarray*}</math>
+Zauważmy, że jeśli mamy sekwent <math>\Delta\vdash\Gamma,\varphi</math> to
+stosując aksjomat (<math>A\bot</math>), a następnie (<math>\to</math> -lewa) dostajemy
+sekwent <math>\Delta,\neg\varphi\vdash\Gamma</math>. Zatem natępująca reguła
+jest ''dopuszczalna'' w systemie <math>\vdash_G</math> (tj.&nbsp;jeśli dodamy
+ją do systemu, to zbiór wyprowadzalnych sekwentów nie ulegnie zmianie):
-<span id=""/> <math> \begin{eqnarray*}\vee\mbox{-intro}\end{eqnarray*}\hspace{.2cm}
+<center><math>(\neg</math> -lewa <math>)\hspace{.2cm}
+\frac{\Delta\vdash\Gamma,\varphi}{\Delta, \neg\varphi\vdash\Gamma}</math></center>
+Ponadto zauważmy, że jeśli mamy dowód sekwentu
+<math>\Delta\vdash\Gamma</math>, to dla każdej formuły <math>\varphi</math> możemy ją
+dodać do prawej strony każdego sekwentu w tym dowodzie i otrzymamy
+dowód sekwentu <math>\Delta\vdash\Gamma,\varphi</math>.
+Łatwy dowód indukcyjny
+pozostawiamy Czytelnikowi (&nbsp;[[Logika dla informatyków/Ćwiczenia 5#weakening|Ćwiczenie 12]]). <br>
+W szczególności, jeśli mamy udowodniony sekwent <math>\Delta,\varphi\vdash\Gamma</math>, to możemy też
+udowodnić sekwent <math>\Delta,\varphi\vdash\Gamma,\bot</math>.<br>
+Stosując do niego regułę (<math>\to</math> -prawa) otrzymujemy sekwent
+<math>\Delta\vdash\Gamma,\neg\varphi</math>. Tym samym pokazaliśmy, że
+następująca reguła jest dopuszczalna w systemie <math>\vdash_G</math>:
+<center><math>(\neg</math> -prawa <math>)\hspace{.2cm}
+\frac{\Delta,\varphi\vdash\Gamma}{\Delta \vdash\Gamma,\neg\varphi}</math></center>
-\fra\prooftree \Delta\vdash\var\varphi \justifies \Delta\vdash\var\varphi\vee\psi} \hspace{1cm \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\begin{eqnarray*}\vee\mbox{-intro}\end{eqnarray*}\hspace{.2cm}\fra\prooftree \Delta\vdash\psi \justifies \Delta\vdash\var\varphi\vee\psi} %\hspace{1cm \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree</math>
+{{twierdzenie|5.9|twier5.9|
-<span id=""/> <math> \begin{eqnarray*}\vee\mbox{-elim}\end{eqnarray*}\hspace{.2cm} \frac{\Delta\vdash\var\varphi\vee\psi\\hspace{1cm}
+Dla każdych <math>\Delta</math> i <math>\varphi</math> mamy następującą równoważność
+<center><math>\Delta\vdash_G\varphi\hspace{.2cm}</math> wtedy i tylko wtedy, gdy  <math>
+\hspace{.2cm} \Delta\vdash_{H^+}\varphi</math>.</center>
+}}
+Powyższe twierdzenie pozostawimy bez dowodu. Łatwo jest
+"przetłumaczyć" każde wyprowadzenie w systemie <math>\vdash_G</math>
+na dowód w stylu Hilberta.
+Dla dowodu implikacji odwrotnej rozszerza się system <math>\vdash_G</math> przez
+dodanie nowej reguły zwanej ''cięciem''.
-\Delta,\var\varphi\vdash\vartheta\\hspace{1cm}</math>
+<center><math>(</math> cięcie <math>)\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma\hspace{.7cm}
+\Delta\vdash\varphi, \Gamma}{\Delta\vdash\Gamma}</math></center>
-<span id=""/> <math> \begin{eqnarray*}\mbox{PS}\end{eqnarray*}\hspace{.2cm}
+Niech <math>\vdash_{GC}</math> oznacza system gentzenowski z cięciem. Bez trudu można
+pokazać, że reguła odrywania jest dopuszczalna w
+<math>\vdash_{GC}</math>. Zatem, korzystając z twierdzenia o pełności dla
+systemu hilbertowskiego, łatwo pokazujemy, że każda tautologia
+jest twierdzeniem systemu <math>\vdash_{GC}</math>. Główna trudność w&nbsp;dowodzie
+&nbsp;[[#twier5.9|Twierdzenia 5.9]] polega na
+udowodnieniu następującego twierdzenia ''o eliminacji cięcia''.
+Twierdzenie to podajemy bez dowodu.
+{{twierdzenie|5.10 (o eliminacji cięcia)||
+Jeśli
+<math>\Delta\vdash_{GC}\Gamma</math>, to <math>\Delta\vdash_G\Gamma</math>.
+}}
+Główna zaleta dowodów w rachunku sekwentów (bez cięcia) wynika z następującej
+''własności podformuł:'' wszystkie formuły występujące
+w przesłance dowolnej reguły są  podformułami formuł występujących
+w&nbsp;konkluzji.
+Zatem np.&nbsp;w dowodzie sekwentu <math>~\vdash\varphi</math> mamy do czynienia tylko
+z&nbsp;podformułami formuły&nbsp;<math>\varphi</math>. Dla danej formuły <math>\varphi</math>, łatwiej
+więc znaleźć  dowód  w sensie Gentzena niż np.&nbsp;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.
+{{przyklad|5.11||
+# Poszukamy dowodu sekwentu <math>\vdash\neg\neg\varphi\to\varphi</math> w
+<math>\vdash_G</math>. Ponieważ najbardziej zewnętrznym spójnikiem w
+rozważanej formule jest <math>\to</math>, to ostatnią regułą w poszukiwanym
+dowodzie musiała być reguła (<math>\to</math> -prawa). Zatem wystarczy
+znaleźć dowód sekwentu <math>\neg\neg\varphi\vdash\varphi</math>. Najbardziej
+zewnętrznym spójnikiem formuły po lewej stronie jest <math>\neg</math>, a
+zatem na mocy reguły (<math>\neg</math> -lewa) wystarczy udowodnić sekwent
+<math>\vdash\varphi, \neg\varphi</math>. Podobnie, na mocy reguły (<math>\neg</math> -prawa),
+wystarczy udowodnić sekwent <math>\varphi\vdash\varphi</math>, a on przecież jest
+aksjomatem.
+# 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 <math>\Delta\vdash\Gamma</math> to takie,
+które spełnia wszystkie formuły z <math>\Delta</math> oraz falsyfikuje
+wszystkie formuły z <math>\Gamma</math>.)
+Dla zilustrowania tej tezy weźmy bardzo prosty
+sekwent <math>\vdash p\to q</math>. Postępując podobnie jak poprzednio,
+dochodzimy do sekwentu <math>p\vdash q</math>, 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 <math>p</math> i falsyfikujące <math>q</math>.
+}}
-</math>
+Z własności podformuł wynika też własność ''konserwatywności''
+systemu nad swoimi fragmentami: jeśli formuła, w której nie
+występuje jakiś spójnik jest tautologią, to jej wyprowadzenie
+nie wymaga reguł związanych z tym spójnikiem.