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

Wersja z 19:56, 21 wrz 2006

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

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.

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)

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr((p\arr p)\arr p)} (A1)
Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (p\arr(p\arr p))\arr(p\arr p)} (1,2)
Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr(p\arr p)} (A1)
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łę $φ$ 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ł $Δ$ oraz dowolnych formuł $φ, ψ$ , je¶li $Δ \cup {φ} ⊢_{H} ψ$ , 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 $ψ$ 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 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 $Δ$ . 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 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 $ψ$ jest zastosowanie reguły (MP) do formuł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vartheta\arr\psi} oraz $ϑ$ , dla pewnej formuły $ϑ$ . 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 $Δ ⊢_{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ł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr\varphi} oraz $ψ$ . Z założenia indukcyjnego mamy

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

Δ ⊨ ψ .

Niech $ϱ$ będzie dowolnym warto¶ciowaniem spełniaj±cym wszystkie formuły z $Δ$ . Na mocy (Uzupelnic eq-zad-1|), warto¶ciowanie $ϱ$ spełnia Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr\varphi} oraz spełnia $ψ$ . Wynika st±d, że $ϱ$ spełnia $φ$ . Tym samym udowodnili¶my, że $Δ ⊨ φ$ . To kończy dowód.

Lemat

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

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi \arr(\neg\psi\arr\neg(\varphi\arr\psi))} ;
Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \bot\arr\varphi} ;
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ł $φ$ oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} dostajemy $ψ$ . 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 $⊥$ . Tym samym pokazali¶my, że $Δ ⊢_{H} ⊥$ . 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ż ${⊥, \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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\varphi\arr\varphi} otrzymujemy $⊥ ⊢_{H} φ$ . 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 $Δ \cup {φ, \neg ψ}$ . Stosuj±c (MP) do formuł $φ$ oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} 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 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 $Δ \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 Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\psi\arr\psi} otrzymujemy $Δ ⊢_{H} ψ$ . 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.

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

Wersja z 19:56, 21 wrz 2006

Paradygmaty dowodzenia

System hilbertowski

Menu nawigacyjne

Działania na stronie

Opcje strony

Narzędzia osobiste

Nawigacja

Szukaj

Narzędzia

@@ Linia 213: / Linia 213: @@
 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)&nbsp; <math>\displaystyle   \varphi\wedge \psi\arr\neg(\varphi\arr\neg\psi)</math><br>
-(B2)&nbsp; <math>\displaystyle   \neg(\varphi\arr\neg\psi)\arr\varphi\wedge \psi</math><br>
-(B3)&nbsp; <math>\displaystyle   \varphi\vee\psi\arr(\neg\varphi\arr\psi)</math><br>
-(B4)&nbsp; <math>\displaystyle   (\neg\varphi\arr\psi)\arr\varphi\vee\psi</math>
-Tak otrzymany system oznaczymy przez <math>\displaystyle \vdash_{H^+}</math>.
-{{twierdzenie|o poprawno¶ci dla <math>\displaystyle \vdash_{H^+}</math>||
-Dla dowolnego zbioru formuł <math>\displaystyle \Delta</math> i dla dowolnej formuły <math>\displaystyle \varphi</math>
-w języku z <math>\displaystyle \vee,\wedge,\arr,\bot</math>,
-je¶li <math>\displaystyle \se_{H^+}\varphi</math> to <math>\displaystyle \Delta\models\varphi</math>.
-}}
-{{dowod|||
-Wystarczy sprawdzić, że aksjomaty (B1)--(B4) s± tautologiami.
-Konkluzja wynika
-z Twierdzenia&nbsp;[[##tw-zda-2|Uzupelnic tw-zda-2|]] o poprawno¶ci dla <math>\displaystyle \vdash_H</math>.
-}}
-{{lemat|||
-Dla dowolnej formuły <math>\displaystyle \varphi</math> istnieje formuła <math>\displaystyle \tilde{\varphi}</math>
-zbudowana przy użyciu jedynie <math>\displaystyle \arr</math> oraz&nbsp;<math>\displaystyle \bot</math>, taka że
-<math>\displaystyle \vdash_{H^+}\varphi\arr\tilde{\varphi}</math>{.1cm} oraz {.1cm}
-<math>\displaystyle \vdash_{H^+}\tilde{\varphi}\arr\varphi</math>.
-}}
-{{dowod|||
-W danej formule <math>\displaystyle \varphi</math>, zast±pmy każd± podformułę postaci
-<math>\displaystyle \psi\wedge\vartheta</math> formuł± <math>\displaystyle \neg(\psi\arr\neg\vartheta)</math> oraz
-każd± podformułę postaci <math>\displaystyle \psi\vee\vartheta</math> formuł±
-<math>\displaystyle \neg\psi\arr\vartheta</math>. Aksjomaty (B1)--(B4) mówi±, że zast±pione
-formuły s± równoważne. Tak więc łatwo dostajemy
-<math>\displaystyle \vdash_{H^+}\varphi\arr\tilde{\varphi}</math> oraz
-<math>\displaystyle \vdash_{H^+}\tilde{\varphi}\arr\varphi</math>. Szczegóły dowodu pozostawimy
-Czytelnikowi.
-}}
-===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>\displaystyle \Delta\vdash\varphi</math>, gdzie <math>\displaystyle \Delta</math> jest
-pewnym skończonym
-zbiorem formuł, a <math>\displaystyle \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>\displaystyle \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>\displaystyle \bot</math>. Pamiętajmy, że <math>\displaystyle \neg\varphi</math> oznacza formułę
-<math>\displaystyle \varphi\arr\bot</math>.
-Poniżej będziemy stosować następuj±c± konwencję:
-Napis <math>\displaystyle \Delta,\varphi_1,\ldots,\varphi_n</math> oznacza zbiór
-<math>\displaystyle \Delta\cup\{\varphi_1,\ldots,\varphi_n\}</math>,
-przy czym nie zakładamy tu, że <math>\displaystyle \varphi_i\not\in\Delta</math>.
-'''Aksjomat'''
-(A0)&nbsp; <math>\displaystyle \Delta,\varphi\vdash\varphi</math>
-'''Reguły dowodzenia'''
-<center><math>\displaystyle (\arr </math> -intro <math>\displaystyle  ) \hspace{.2cm}
-\frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\arr\psi}
-\hspace{1cm} (\arr </math> -elim <math>\displaystyle  ) \hspace{.2cm}
-\frac{\Delta\vdash\varphi\arr\psi\odstep
-\Delta\vdash\varphi}{\Delta\vdash\psi}</math></center>
-<center><math>\displaystyle (\wedge </math> -intro <math>\displaystyle  )\hspace{.2cm} \frac{\Delta\vdash\varphi\odstep
-\Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi} \hspace{1cm}
-(\wedge </math> -elim <math>\displaystyle  )
-\hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi}
-\hspace{1cm}
-(\wedge </math> -elim <math>\displaystyle  )
-\hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}</math></center>
-<center><math>\displaystyle (\vee </math> -intro <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm}
-(\vee </math> -intro <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi} </math></center>
-<center><math>\displaystyle (\vee </math> -elim <math>\displaystyle  )\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\odstep
-\Delta,\varphi\vdash\vartheta\odstep
-\Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}</math></center>
-<center><math>\displaystyle ( </math> PS <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta,\neg\varphi\vdash\bot}{\Delta\vdash\varphi}</math></center>
-Zauważmy, że szczególnym przypadkiem reguły (<math>\displaystyle \arr</math>-intro) jest
-następuj±ca reguła, można j± traktować jak regułę wprowadzenia negacji.
-<center><math>\displaystyle \frac{\Delta,\varphi\vdash\bot}
-{\Delta\vdash\neg\varphi}</math></center>
-Zauważmy też, że szczególnym przypadkiem reguły (<math>\displaystyle \arr</math>-elim) jest
-następuj±ca reguła, można j± traktować jak regułę eliminacji negacji.
-<center><math>\displaystyle \frac{\Delta\vdash\neg\varphi\quad
-\Delta\vdash\varphi}{\Delta\vdash\bot}</math></center>
-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
-<math>\displaystyle \Delta\vdash\varphi</math> w systemie naturalnej dedukcji nazwiemy drzewo
-etykietowane sekwentami tak, że korzeń ma etykietę
-<math>\displaystyle \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>\displaystyle \Delta\vdash_{N}\varphi</math>, gdy sekwent
-<math>\displaystyle \Delta\vdash\varphi</math> ma dowód w&nbsp;systemie
-naturalnej dedukcji. Gdy <math>\displaystyle \Delta=\emptyset</math>, to mówimy też,
-że <math>\displaystyle \varphi</math> jest ''twierdzeniem'' systemu naturalnej dedukcji
-i zapisujemy to przez <math>\displaystyle \vdash_N\varphi</math>.
-Je¶li <math>\displaystyle \Delta</math> jest zbiorem nieskończonym, to
-<math>\displaystyle \Delta\vdash_{N}\varphi</math> oznacza, że istnieje dowód sekwentu
-<math>\displaystyle \Delta_0\vdash\varphi</math>, dla pewnego skończonego <math>\displaystyle \Delta_0
-\subseteq\Delta</math>.
-Poniżej podajemy kilka przykładów dowodów w systemie naturalnej
-dedukcji.
-{{przyklad|||
-* Pokażemy <math>\displaystyle \vdash_{N}p\arr p</math>.
-<center><math>\displaystyle \arintro{p\vdash p}{\vdash p\arr p}
-</math></center>
-* Pokażemy <math>\displaystyle \vdash_{N} p\arr(q\arr p)</math>.
-<center><math>\displaystyle \arintro{\arintro{p,q\vdash p}{p\vdash q\arr p}}{\vdash p\arr (q\arr p)}
-</math></center>
-* Pokażemy <math>\displaystyle \vdash_{N}\neg\neg p\arr p</math>.
-<center><math>\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}
-</math></center>
-}}
-{{twierdzenie|||
-Dla dowolnego sekwentu <math>\displaystyle \Delta\vdash\varphi</math> mamy następuj±c±
-równoważno¶ć:
-<center><math>\displaystyle \Delta\vdash_{N}\varphi\hspace{.2cm}  </math>  , gdy  <math>\displaystyle  \hspace{.2cm}
-\Delta\vdash_{H^+}\varphi.</math></center>
-}}
-Aby pokazać, że każdy dowód w <math>\displaystyle \vdash_{N}</math> daje się przerobić
-na dowód w <math>\displaystyle \vdash_{H^+}</math> wystarczy sprawdzić, że każda z reguł
-systemu naturalnej dedukcji jest ''dopuszczalna'' w <math>\displaystyle H^+</math>.
-Tzn.&nbsp;wystarczy sprawdzić, że je¶li mamy dowody przesłanek w&nbsp;<math>\displaystyle \vdash_{H^+}</math>,
-to możemy udowodnić konkluzję.    Zauważmy, że
-wyprowadzalno¶ć reguły(<math>\displaystyle \arr</math>-intro) jest konsekwencj± twierdzenia
-o dedukcji, natomiast reguła (<math>\displaystyle \arr</math>-elim) jest reguł±&nbsp;(MP).
-Przykładowo pokażemy wyprowadzenie (<math>\displaystyle \vee</math>-elim) oraz (PS) w&nbsp;<math>\displaystyle H^+</math>,
-pozostawiaj±c Czytelnikowi wyprowadzenie pozostałych reguł.
-Załóżmy, że mamy w <math>\displaystyle H^+</math> dowody następuj±cych sekwentów:
-<math>\displaystyle \Delta\vdash\varphi\vee\psi</math>, {.1cm}
-<math>\displaystyle \Delta,\varphi\vdash\vartheta</math> {.1cm}oraz {.1cm}
-<math>\displaystyle \Delta,\psi\vdash\vartheta</math>. Wówczas,
-stosuj±c aksjomat (B2) i regułę (MP) mamy
-<math>\displaystyle \Delta\vdash_{H^+}\neg\varphi\arr\psi</math>.
-Zatem <math>\displaystyle \Delta,\neg\varphi\vdash_{H^+}\psi</math> i ponieważ
-<math>\displaystyle \Delta\vdash_{H^+}\psi\arr\vartheta</math> to również
-<math>\displaystyle \Delta,\neg\varphi\vdash_{H^+}\psi\arr\vartheta</math>. St±d
-<math>\displaystyle \Delta,\neg\varphi\vdash_{H^+}\vartheta</math>. Stosuj±c twierdzenie o dedukcji
-dostajemy <math>\displaystyle \Delta\vdash_{H^+}\neg\varphi\arr\vartheta</math>. Skoro mamy również
-<math>\displaystyle \delta\vdash_{H^+}\varphi\arr\vartheta</math>, to na mocy
-Lematu&nbsp;[[##le-zda-1|Uzupelnic le-zda-1|]](3) otrzymujemy <math>\displaystyle \Delta\vdash_{H^+}\vartheta</math>.
-Dla wyprowadzenia (PS) załóżmy, że
-<math>\displaystyle \Delta,\neg\varphi\vdash_{H^+}\bot</math>. Z twierdzenia o dedukcji
-dostajemy <math>\displaystyle \Delta\vdash_{H^+}\neg\neg\varphi</math>. Tak więc z
-(A3) i (MP) dostajemy <math>\displaystyle \Delta\vdash_{H^+}\varphi</math>.
-Dla pokazania implikacji odwrotnej wystarczy pokazać, że wszystkie
-aksjomaty systemu <math>\displaystyle H^+</math> s± twierdzeniami systemu naturalnej dedukcji.
-Wyprowadzenia (A1) i
-(A3) w ND zostały podane w Przykładzie&nbsp;[[##pr-zda-2|Uzupelnic pr-zda-2|]]. Przykładowo pokażemy
-wyprowadzenia
-(A2) i (B1). Zaczniemy od wyprowadzenia (A2). Niech
-<math>\displaystyle \Delta=\{\varphi\arr(\psi\arr\vartheta),\ \varphi\arr\psi,\ \varphi\}</math>.
-Mamy następuj±cy dowód:
-<center><math>\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}
-</math></center>
-Stosuj±c trzy razy (<math>\displaystyle \arr </math> -intro ) do sekwentu <math>\displaystyle \se\vartheta</math>
-dostajemy wyprowadzenie aksjomatu (A2).
-Następnie pokażemy dowód (B1) w ND.  Zaczniemy od
-wyprowadzenia <math>\displaystyle \neg(\varphi\arr\neg\psi)\vdash\varphi</math>, gdzie
-<math>\displaystyle \Delta=\{\neg(\varphi\arr\neg\psi), \neg\varphi\}</math>:
-<center><math>\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}
-</math></center>
-Następnie wyprowadzimy sekwent <math>\displaystyle \neg(\varphi\arr\neg\psi)\vdash\psi</math>. Niech
-<math>\displaystyle \Delta=\{\neg(\varphi\arr\neg\psi), \neg\psi\}</math>
-<center><math>\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}
-</math></center>
-Maj±c wyprowadzone sekwenty <math>\displaystyle \neg(\varphi\arr\neg\psi)\vdash\varphi</math>
-oraz <math>\displaystyle \neg(\varphi\arr\neg\psi)\vdash\psi</math> możemy zakończyć dowód&nbsp;(B1).
-<center><math>\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)}
-</math></center>
-===Rachunek sekwentów===
-Dla przedstawienia rachunku sekwentów rozszerzymy nieco pojęcie
-sekwentu. Przez ''sekwent'' będziemy teraz rozumieć napis
-<math>\displaystyle \Delta\vdash\Gamma</math>, gdzie <math>\displaystyle \Delta</math> oraz <math>\displaystyle \Gamma</math> s± skończonymi
-zbiorami formuł. Intuicyjnie, wyprowadzalno¶ć  sekwentu
-<math>\displaystyle \Delta\vdash\Gamma</math> w rachunku sekwentów będzie oznaczać, że
-alternatywa formuł z <math>\displaystyle \Gamma</math> wynika z&nbsp;hipotez <math>\displaystyle \Delta</math>.
-Podobnie jak w poprzedniej czę¶ci, rozważamy formuły,
-zbudowane w oparciu o spójniki <math>\displaystyle \arr,\vee,\wedge</math> oraz stał±
-zdaniow± <math>\displaystyle \bot</math>. Negację <math>\displaystyle \neg</math> traktujemy jako spójnik
-zdefiniowany przez <math>\displaystyle \arr</math> i&nbsp;<math>\displaystyle \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>\displaystyle \vdash</math>, a druga grupa jest odpowiedzialna za wprowadzanie spójnika na
-prawo od <math>\displaystyle \vdash</math>. Dla każdego spójnika mamy odpowiadaj±c± parę reguł.
-Aksjomat (A<math>\displaystyle \bot</math>) można traktować jako regułę (bez
-przesłanek) wprowadzenia <math>\displaystyle \bot</math> z lewej strony znaku <math>\displaystyle \vdash</math>.
-Przypomnijmy, że  napis <math>\displaystyle \Delta,\varphi_1,\ldots,\varphi_n</math>
-oznacza zbiór <math>\displaystyle \Delta\cup\{\varphi_1,\ldots,\varphi_n\}</math>.
-'''Aksjomaty'''
-(A00)&nbsp; <math>\displaystyle \Delta,\varphi\vdash\Gamma,\varphi</math>
-(A<math>\displaystyle \bot</math>)&nbsp; <math>\displaystyle \Delta,\bot\vdash\Gamma</math>
-'''Reguły dowodzenia'''<br>
-<center><math>\displaystyle (\arr </math> -lewa <math>\displaystyle  )\hspace{.2cm} \frac{\Delta\vdash\Gamma,\varphi\odstep
-\Delta,\psi\vdash\Gamma}{\Delta,\varphi\arr\psi\vdash\Gamma}
-\hspace{1cm}(\arr </math> -prawa <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta,\varphi\vdash\Gamma,\psi}{\Delta\vdash\Gamma,
-\varphi\arr\psi}</math></center>
-<center><math>\displaystyle (\wedge </math> -lewa <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta,\varphi,\psi\vdash\Gamma}{\Delta,\varphi\wedge\psi\vdash\Gamma}
-\hspace{1cm} (\wedge </math> -prawa <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta\vdash\Gamma, \varphi\odstep
-\Delta\vdash\Gamma,\psi}{\Delta\vdash \Gamma,\varphi\wedge\psi}</math></center>
-<center><math>\displaystyle (\vee </math> -lewa <math>\displaystyle  )\hspace{.2cm} \frac{\Delta,
-\varphi\vdash\Gamma\odstep
-\Delta,\psi\vdash\Gamma}{\Delta, \varphi\vee\psi \vdash\Gamma}
-\hspace{1cm} (\vee </math> -prawa <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta\vdash\Gamma, \varphi, \psi}{\Delta\vdash\Gamma,
-\varphi\vee\psi}</math></center>
-''Dowodem'' sekwentu <math>\displaystyle \Delta\vdash\Gamma</math>, tak jak poprzednio,
-nazywamy drzewo etykietowane sekwentami tak, że korzeń jest
-etykietowany przez <math>\displaystyle \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>\displaystyle \Delta\vdash\Gamma</math> w rachunku sekwentów to zapisujemy to tak:
-<math>\displaystyle \Delta\vdash_G\Gamma</math>. (Litera G pochodzi od nazwiska twórcy tego
-systemu, G.&nbsp;Gentzena.) Piszemy też <math>\displaystyle \Delta\vdash_{G}\varphi</math>, gdy&nbsp;<math>\displaystyle \Delta</math>
-jest nieskończony, ale  <math>\displaystyle \Delta\vdash_G\varphi</math>
-dla pewnego skończonego <math>\displaystyle \Delta_0 \subseteq\Delta</math>.
-Zauważmy, że je¶li mamy sekwent <math>\displaystyle \Delta\vdash\Gamma,\varphi</math> to
-stosuj±c aksjomat (A<math>\displaystyle \bot</math>), a następnie (<math>\displaystyle \arr</math>-lewa) dostajemy
-sekwent <math>\displaystyle \Delta,\neg\varphi\vdash\Gamma</math>.  Zatem natępuj±ca reguła
-jest ''dopuszczalna'' w systemie <math>\displaystyle \vdash_G</math> (tj.&nbsp;je¶li dodamy
-j± do systemu, to zbiór wyprowadzalnych sekwentów nie ulegnie zmianie):
-<center><math>\displaystyle (\neg </math> -lewa <math>\displaystyle  )\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>\displaystyle \Delta\vdash\Gamma</math>, to dla każdej formuły <math>\displaystyle \varphi</math> możemy j±
-dodać do prawej strony każdego sekwentu w tym dowodzie i otrzymamy
-dowód sekwentu <math>\displaystyle \Delta\vdash\Gamma,\varphi</math>.
-Łatwy dowód indukcyjny
-pozostawiamy Czytelnikowi (Ćwiczenie&nbsp;[[##weakening|Uzupelnic weakening|]]). W szczególno¶ci,
-je¶li mamy udowodniony sekwent <math>\displaystyle \Delta,\varphi\vdash\Gamma</math>, to możemy też
-udowodnić sekwent <math>\displaystyle \Delta,\varphi\vdash\Gamma,\bot</math>. Stosuj±c do
-niego  regułę (<math>\displaystyle \arr</math>-prawa) otrzymujemy sekwent
-<math>\displaystyle \Delta\vdash\Gamma,\neg\varphi</math>. Tym samym pokazali¶my, że
-następuj±ca reguła jest dopuszczalna w systemie <math>\displaystyle \vdash_G</math>:
-<center><math>\displaystyle (\neg </math> -prawa <math>\displaystyle  )\hspace{.2cm}
-\frac{\Delta,\varphi\vdash\Gamma}{\Delta \vdash\Gamma,\neg\varphi}</math></center>
-{{twierdzenie|||
-Dla każdych <math>\displaystyle \Delta</math> i <math>\displaystyle \varphi</math> mamy następuj±c± równoważno¶ć
-<center><math>\displaystyle \Delta\vdash_G\varphi\hspace{.2cm} </math>  wtedy i tylko wtedy, gdy  <math>\displaystyle
-\hspace{.2cm} \Delta\vdash_{H^+}\varphi.</math></center>
-}}
-Powyższe twierdzenie pozostawimy bez dowodu. Łatwo jest
-"przetłumaczyć" każde wyprowadzenie w systemie <math>\displaystyle \vdash_G</math>
-na dowód w stylu Hilberta.
-Dla dowodu implikacji odwrotnej rozszerza się system <math>\displaystyle \vdash_G</math> przez
-dodanie nowej reguły zwanej ''cięciem''.
-<center><math>\displaystyle ( </math> cięcie <math>\displaystyle  )\hspace{.2cm} \frac{\Delta,\varphi\vdash\Gamma\hspace{.7cm}
-\Delta\vdash\varphi, \Gamma}{\Delta\vdash\Gamma}</math></center>
-Niech <math>\displaystyle \vdash_{GC}</math> oznacza system gentzenowski z cięciem. Bez trudu można
-pokazać, że reguła odrywania jest dopuszczalna w
-<math>\displaystyle \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>\displaystyle \vdash_{GC}</math>. Główna trudno¶ć w&nbsp;dowodzie
-Twierdzenia&nbsp;[[##milo|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
-<math>\displaystyle \Delta\vdash_{GC}\Gamma</math>, to <math>\displaystyle \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 formuwystępuj±cych
-w&nbsp;konkluzji.
-Zatem np.&nbsp;w dowodzie sekwentu <math>\displaystyle ~\vdash\varphi</math> mamy do czynienia tylko
-z&nbsp;podformułami formuły&nbsp;<math>\displaystyle \varphi</math>. Dla danej formuły <math>\displaystyle \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|||
-# Poszukamy dowodu sekwentu <math>\displaystyle \vdash\neg\neg\varphi\arr\varphi</math> w
-<math>\displaystyle \vdash_G</math>. Ponieważ najbardziej zewnętrznym spójnikiem w
-rozważanej formule jest <math>\displaystyle \arr</math>, to ostatni± reguł± w poszukiwanym
-dowodzie musiała być reguła (<math>\displaystyle \arr</math>-prawa). Zatem wystarczy
-znaleĽć dowód sekwentu <math>\displaystyle \neg\neg\varphi\vdash\varphi</math>. Najbardziej
-zewnętrznym spójnikiem formuły po lewej stronie jest <math>\displaystyle \neg</math>, a
-zatem na mocy reguły (<math>\displaystyle \neg</math>-lewa) wystarczy udowodnić sekwent
-<math>\displaystyle \vdash\varphi, \neg\varphi</math>. Podobnie, na mocy reguły (<math>\displaystyle \neg</math>-prawa),
-wystarczy udowodnić sekwent <math>\displaystyle \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>\displaystyle \Delta\vdash\Gamma</math> to takie,
-które spełnia wszystkie formuły z <math>\displaystyle \Delta</math> oraz falsyfikuje
-wszystkie formuły z <math>\displaystyle \Gamma</math>.)
-Dla zilustrowania tej tezy weĽmy bardzo prosty
-sekwent <math>\displaystyle \vdash p\arr q</math>. Postępuj±c podobnie jak porzednio
-dochodzimy do sekwentu <math>\displaystyle 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>\displaystyle p</math> i falsyfikuj±ce <math>\displaystyle q</math>.
-}}
-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}
-# Niech <math>\displaystyle \vdash_{H_1}</math> oznacza system dowodzenia otrzymany
-z systemu <math>\displaystyle \vdash_H</math> przez zamianę aksjomatu (A3) na
-następuj±cy aksjomat:
-(A3')&nbsp; <math>\displaystyle (\neg\varphi\arr\neg\psi)\arr((\neg\varphi\arr
-\psi)\arr\varphi).</math>
-Dowie¶ć, że obydwa systemy s± równoważne, tzn., że dla
-dowolnego sekwentu <math>\displaystyle \Delta\vdash\varphi</math>, zachodzi
-<math>\displaystyle \Delta\vdash_H\varphi</math> , gdy <math>\displaystyle \Delta\vdash_{H_1}\varphi</math>.
-# Niech <math>\displaystyle \vdash_{H_2}</math> oznacza system dowodzenia otrzymany
-z systemu <math>\displaystyle \vdash_H</math> przez zamianę aksjomatu (A3) na <math>\displaystyle \vdash_H</math>,
-następuj±cy aksjomat:
-(A3")&nbsp; <math>\displaystyle (\neg\varphi\arr\neg\psi)\arr(\psi\arr\varphi).</math>
-Dowie¶ć, że obydwa systemy s± równoważne, tzn., że dla
-dowolnego sekwentu <math>\displaystyle \Delta\vdash\varphi</math>, zachodzi
-<math>\displaystyle \Delta\vdash_H\varphi</math> , gdy <math>\displaystyle \Delta\vdash_{H_2}\varphi</math>.
-# Dowie¶ć, że aksjomatu (A3) nie da się wyprowadzić z
-aksjomatów (A0--2) przy pomocy reguły odrywania.
-# Dowie¶ć <math>\displaystyle \vdash_H\neg p \arr(p\arr q)</math> używaj±c twierdzenia o
-dedukcji oraz bez użycia tego twierdzenia.
-# Pokazać, że w systemie <math>\displaystyle \vdash_H</math> dopuszczalna jest
-następuj±ca reguła:
-<center><math>\displaystyle \frac{\varphi\arr\psi\odstep
-\neg\psi}{\neg\varphi}</math></center>
-tzn.&nbsp;pokazać, że je¶li <math>\displaystyle \Delta\vdash_H\varphi\arr\psi</math> oraz
-<math>\displaystyle \Delta\vdash_H\neg\psi</math>, to również mamy <math>\displaystyle  \Delta\vdash_H\neg\varphi</math>.
-# Dowie¶ć, że dla każdej formuły <math>\displaystyle \varphi</math>, nie będ±cej
-tautologi±, istnieje maksymalny zbiór formuł&nbsp;<math>\displaystyle \Delta</math> (nad dan± sygnatur±)
-o&nbsp;tej własno¶ci, że
-<math>\displaystyle \Delta\not\vdash_H\varphi</math>.
-# Każdy z poniższych sekwentów wyprowadzić w  systemie
-<math>\displaystyle \vdash_{H^+}</math>, <math>\displaystyle \vdash_{N}</math>, <math>\displaystyle \vdash_G</math>.
- <nowiki> =</nowiki>   2pt
-## <math>\displaystyle \vdash \bot\arr p</math>;
-## <math>\displaystyle p\arr q,q\arr r\vdash p\arr r</math>;
-## <math>\displaystyle \vdash(\neg p\arr p)\arr p</math>;
-## <math>\displaystyle p,\neg p\vdash q</math>;
-## <math>\displaystyle p\arr(q\arr r)\vdash q\arr(p\arr r)</math>;
-## <math>\displaystyle \vdash (\neg p\arr \neg q)\arr (q\arr p)</math>;
-## <math>\displaystyle \vdash \neg(p\wedge q)\arr(\neg p\vee\neg q)</math>.
-# Dowie¶ć, że je¶li <math>\displaystyle \Delta\vdash_{N}\varphi</math>, to dla dowolnej
-formuły <math>\displaystyle \psi</math> zachodzi <math>\displaystyle \Delta,\psi\vdash_{N}\varphi</math>.
-# Dowie¶ć, że je¶li <math>\displaystyle \Delta\vdash_{N}\bot</math>, to dla dowolnej
-formuły <math>\displaystyle \varphi</math> zachodzi <math>\displaystyle \Delta\vdash_{N}\varphi</math>.
-# Dla każdego z sytemów <math>\displaystyle \vdash_{H^+}</math>, <math>\displaystyle \vdash_{N}</math>,
-<math>\displaystyle \vdash_G</math> dowie¶ć, że je¶li sekwent <math>\displaystyle \Delta\vdash\varphi</math> jest
-wyprowadzalny w&nbsp;tym systemie oraz <math>\displaystyle S</math> jest podstawieniem formuł na
-zmienne zdaniowe, to sekwent <math>\displaystyle \vec{S}(\Delta)\vdash S(\varphi)</math>
-powstaj±cy w  wyniku podstawienia  jest też wyprowadzalny w tym systemie.
-#
- Udowodnić, że w rachunku sekwentów zamiana reguły <math>\displaystyle (\vee </math> -prawa <math>\displaystyle  )</math>
-na dwie reguły:
-<center><math>\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</math></center>
-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:
-<center><math>\displaystyle \prooftree{\Delta\vdash\Gamma}\justifies{\Delta,\varphi\vdash\Gamma}
-      \endprooftree
-\hspace{3cm}
- \prooftree{\Delta\vdash\Gamma}\justifies{\Delta\vdash\Gamma,\varphi}
-      \endprooftree</math></center>
-# Wyprowadzić w rachunku sekwentów:
-## <math>\displaystyle \vdash p\vee \neg p</math>;
-## <math>\displaystyle \vdash ((p\to q)\to p)\to p</math>.
-Czy można to zrobić używaj±c tylko sekwentów postaci <math>\displaystyle \Delta\vdash\varphi</math>
-(z jedn± formuł± po prawej)?