Logika dla informatyków/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 rachunkupredykatów nie istnieje w ogóle żaden algorytm sprawdzania czy dana formuła jest tautologi± \begin{eqnarray*}Twierdzenie #entscheidungsproblem\end{eqnarray*}. W obu przypadkach istniej± jednak metody dowodzenia\/ pozwalaj±ce na wyprowadzanie prawdziwych formuł za pomoc±\boldsymbol{s}}\def\blank{\hbox{\sf Bstalonych procedursyntaktycznych.

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};
• zbiór operacji przekształcaj±cych wyrażenia w wyrażenia ---operacje te s± nazywane {\em regułami dowodzenia}.

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 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 typuhilbertowskiego \begin{eqnarray*}od nazwiska Davida Hilberta\end{eqnarray*}, system naturalnej dedukcji oraz rachunek sekwentów. Ostatnie dwa systemy znajduj± zastosowanie w pewnych działach sztucznej inteligencji oraz w systemach automatycznego dowodzenia twierdzeń.

Poniższy system dowodzenia dotyczy formuł zbudowanych przy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciujedynie spójnika Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} , stałej $\mathrm{\perp }$ oraz zmiennych zdaniowych.Przypomnijmy, że dladowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} jest skrótem zapisuParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\bot} . Symbole Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi,\vartheta} w poniższym systemie oznaczaj± dowolne formuły.

\vspace{.3cm}\noindentAksjomaty

\begin{eqnarray*}A1\end{eqnarray*} Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\begin{eqnarray*}\psi\arr\var\varphi\end{eqnarray*}} \\\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*} Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\neg\var\varphi\arr\var\varphi}

\vspace{.3cm}\noindentReguła dowodzenia\\ Parser nie mógł rozpoznać (błąd składni): {\displaystyle {\rm \begin{eqnarray*}MP\end{eqnarray*}}\hspace{1cm} \frac{\var\varphi\\hspace{1cm} }

Reguła \begin{eqnarray*}MP\end{eqnarray*} jest nazywana {\em reguł± odrywania} lub teżreguł± {\em modus ponens}.

\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 wcze¶niej występuj±cych formuł w wyniku zastosowania reguły odrywania. Powiemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ma dowód\/}, lub jest \textit{twierdzeniemsystemu hilbertowskiego, co zapiszemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H\var\varphi} ,gdy istnieje dowód zawieraj±cy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Powyższ± definicję możemynieco\boldsymbol{s}}\def\blank{\hbox{\sf Bogólnić. Niech $\mathrm{\Delta }$ będzie dowolnym zbioremformuł. Powiemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ma dowód ze zbioru hipotez $\mathrm{\Delta }$ \begin{eqnarray*}notacja Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} \end{eqnarray*}, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest twierdzeniem systemu, w którym zbiór aksjomatów został poszerzony o formuły ze zbioru $\mathrm{\Delta }$.

Przykład

Niech $p$ będzie zmienn± zdaniow±. Pokażemy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle p\arr p} jest twierdzeniem systemu hilbertowskiego. Poniżej podajemy dowód dla tej formuły. W nawiasach podajemy nazwę aksjomatu, je¶li dana formuła jest instancj± tego aksjomatu, lub też numery formuł z wcze¶niejszych kroków dowodu, do których jest stosowana reguła odrywania.

1. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \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*}} \\hspace{1cm} \begin{eqnarray*}A2\end{eqnarray*}
2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle p\arr\begin{eqnarray*}\begin{eqnarray*}p\arr p\end{eqnarray*}\arr p\end{eqnarray*}} \\hspace{1cm} \begin{eqnarray*}A1\end{eqnarray*}
3. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}p\arr\begin{eqnarray*}p\arr p\end{eqnarray*}\end{eqnarray*}\arr\begin{eqnarray*}p\arr p\end{eqnarray*}} \\hspace{1cm} \begin{eqnarray*}1,2\end{eqnarray*}
4. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle p\arr\begin{eqnarray*}p\arr p\end{eqnarray*}} \\hspace{1cm} \begin{eqnarray*}A1\end{eqnarray*}
5. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle p\arr p} \\hspace{1cm} \begin{eqnarray*}3,4\end{eqnarray*}

Zauważmy, że w powyższym przykładzie możemy wszędzie zast±pićzmienn± $p$ przez dowoln± formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} dostaj±c dowód formułyParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\var\varphi} .

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.

Twierdzenie

Dla dowolnego zbioru formuł $\mathrm{\Delta }$ oraz dowolnych formuł Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi} ,je¶li Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\cup\{\var\varphi\}\vdash_H\psi} , to \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi\arr\psi} }.

<span id="

Dowód jest indukcyjny ze względu na liczbę kroków w dowodzie formuły$\psi$ ze zbioru hipotez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\cup\{\var\varphi\}} . Przypu¶ćmy najpierw, że dowód tenskłada się tylko z jednego kroku. Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \psi=\var\varphi} , to stosuj±c wyprowadzenie z Przykładu #pr-zda-1a dostajemy dowódformuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\var\varphi} . Możemy oczywi¶cie przyj±ć, że formuła tajest wyprowadzona ze zbioru hipotez $\mathrm{\Delta }$. Druga możliwo¶ć jest taka, że$\psi \in \mathrm{\Delta }$ lub też, że $\psi$ jest aksjomatem. W każdym z tychprzypadków mamy $\mathrm{\Delta }{⊢}_H\psi$. Wówczas stosuj±c regułęodrywania do $\psi$ oraz aksjomatu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \psi\arr\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}} dostajemy formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\psi} .

Założmy teraz, że ostatnim krokiem w wyprowadzeniu formuły $\psi$ jest zastosowanie reguły \begin{eqnarray*}MP\end{eqnarray*} do formuł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vartheta\arr\psi} oraz$\vartheta$, dla pewnej formuły $\vartheta$. Z założenia indukcyjnego mamy </math>\Delta\vdash_H\var\varphi\arr\begin{eqnarray*}\vartheta\arr\psi\end{eqnarray*}</math> oraz Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi\arr\vartheta} . 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łę Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\var\varphi\arr\vartheta\end{eqnarray*}\arr\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}} . Ponownie stosuj±c regułę odrywania do tej formuły oraz do Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\vartheta} dostajemy ż±dan± formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\psi} . \Rightarrow kończy dowód twierdzenia o dedukcji." style="font-variant:small-caps">Dowód

{{{3}}}

Twierdzenie

Je¶li Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} , to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} . W szczególno¶ci, je¶li Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_H\var\varphi} , to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologi±.

Dowód eq-zad-1

{{{3}}}

\def\blank{\hbox{\sf Bdowodnili¶my, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} . \Rightarrowkończy dowód.}}

\begin{lemat} Dla dowolnych formuł Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi,\psi} zbudowanych przy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} oraz $\mathrm{\perp }$, następuj±ce formuły s± twierdzeniami systemu hilbertowskiego.

1. Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi \arr\begin{eqnarray*}\neg\psi\arr\neg\begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\end{eqnarray*}} ;
2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \bot\arr\var\varphi} ;
3. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\var\varphi\arr\psi\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}\arr\psi\end{eqnarray*}} ;

\end{lemat}

Dowód

{{{3}}}

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.

\noindent\begin{eqnarray*}B1\end{eqnarray*}  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\wedge \psi\arr\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}} \\\begin{eqnarray*}B2\end{eqnarray*}  Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\arr\var\varphi\wedge \psi} \\\begin{eqnarray*}B3\end{eqnarray*}  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\vee\psi\arr\begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}} \\\begin{eqnarray*}B4\end{eqnarray*}  Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}\arr\var\varphi\vee\psi}

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

Twierdzenie

Dla dowolnego zbioru formuł $\mathrm{\Delta }$ i dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} 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^+}\var\varphi} to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\models\var\varphi} .

Dowód

{{{3}}}

\begin{lemat} Dla dowolnej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} istnieje formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \tilde{\var\varphi}} zbudowana przy\boldsymbol{s}}\def\blank{\hbox{\sf Bżyciu jedynie Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} oraz $\mathrm{\perp }$, taka żeParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\var\varphi\arr\tilde{\var\varphi}} \hspace{.1cm} oraz \hspace{.1cm}Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_{H^+}\tilde{\var\varphi}\arr\var\varphi} . \end{lemat}

Dowód

{{{3}}}

System naturalnej dedukcji \begin{eqnarray*}wprowadzony przez S. Ja¶kowskiego i G. Gentzena\end{eqnarray*} operuje wyrażeniami zwanymi \textit{sekwentami}. S± to wyrażenia postaci Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} , gdzie $\mathrm{\Delta }$ jest pewnym skończonym zbiorem formuł, a Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} 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 $⊢$\begin{eqnarray*}tj. 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. 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 $\mathrm{\perp }$. Pamiętajmy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} oznacza formułęParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\arr\bot} .

Poniżej będziemy stosować następuj±c± konwencję: Napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi_1,\ldots,\var\varphi_n} oznacza zbiór Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\cup\{\var\varphi_1,\ldots,\var\varphi_n\}} , przy czym nie zakładamy tu, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_i\not\in\Delta} .

\vspace{.3cm}\noindentAksjomat

\begin{eqnarray*}A0\end{eqnarray*}  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi\vdash\var\varphi}

\vspace{.4cm}\noindentReguły dowodzenia

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\arr\mbox{-intro}\end{eqnarray*} \hspace{.2cm} \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}}

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

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\vee\mbox{-intro}\end{eqnarray*}\hspace{.2cm} \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}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\vee\mbox{-elim}\end{eqnarray*}\hspace{.2cm} \frac{\Delta\vdash\var\varphi\vee\psi\\hspace{1cm} \Delta,\var\varphi\vdash\vartheta\\hspace{1cm}}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\mbox{PS}\end{eqnarray*}\hspace{.2cm} }

Zauważmy, że szczególnym przypadkiem reguły \begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} -intro\end{eqnarray*} jestnastępuj±ca reguła, można j± traktować jak regułę wprowadzenia negacji. Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \frac{\Delta,\var\varphi\vdash\bot} }

Zauważmy też, że szczególnym przypadkiem reguły \begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} -elim\end{eqnarray*} jestnastępuj±ca reguła, można j± traktować jak regułę\Delta\vdashliminacji negacji. Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \frac{\Delta\vdash\neg\var\varphi\quad }

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ędzyprzesłankami i konkluzj± stosowanych reguł. \textit{Dowodem\/} sekwentuParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} w systemie naturalnej dedukcji nazwiemy drzewoetykietowane sekwentami tak, że korzeń ma\Delta\vdashtykietę\mbox{Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} }, li¶cie s±\Delta\vdashtykietowane wyst±pieniami aksjomatuoraz każdy wewnętrzny wierzchołek jest\Delta\vdashtykietowany sekwentemotrzymanym z\Delta\vdashtykiet p\leftrightarrowmków tego wierzchołka przy zastosowaniujednej z reguł. Piszemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{N}\var\varphi} , gdy sekwent Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} ma dowód w systemie naturalnej dedukcji. Gdy $\mathrm{\Delta }=\mathrm{\varnothing }$, to mówimy też, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest twierdzeniem\/ systemu naturalnej dedukcji i zapisujemy to przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash_N\var\varphi} .Je¶li $\mathrm{\Delta }$ jest zbiorem nieskończonym, toParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{N}\var\varphi} oznacza, że istnieje dowód sekwentu </math>\Delta_0\vdash\var\varphiParser nie mógł rozpoznać (błąd składni): {\displaystyle , dla pewnego skończonego } \Delta_0\subseteq\Delta</math>.

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

Przykład

\

• Pokażemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vdash_{N}p\arr p} .\[\arintr\prooftree p\vdash p \justifies \vdash p\arr p \using \textrm{\begin{eqnarray*}W\end{eqnarray*

\endprooftree\]

• Pokażemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vdash_{N} p\arr\begin{eqnarray*}q\arr p\end{eqnarray*}} .\[\arintro{\arintr\prooftree p,q\vdash p}{p\vdash q\arr p} \justifies \vdash p\arr \begin{eqnarray*}q\arr p\end{eqnarray*} \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\]

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

\[\arintro{\ps{\arelim{\neg\neg p,\neg p\vdash\neg\neg p}{\neg\neg p,\neg p\vdash\neg p}{\neg\neg p,\neg p\vdash p}}{\neg\neg p\vdash p}}{\vdash\neg\neg p\arr p}\]

}}

Twierdzenie

Dla dowolnego sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} mamy następuj±c±równoważno¶ć:\[\Delta\vdash_{N}\var\varphi\hspace{.2cm} \mbox{ \wtw, gdy }\hspace{.2cm}\Delta\vdash_{H^+}\var\varphi.\]

\begin{dowodbezqed}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\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić konkluzję. Zauważmy, żewyprowadzalno¶ć reguły\begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} -intro\end{eqnarray*} jest konsekwencj± twierdzeniao dedukcji, natomiast reguła \begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} -elim\end{eqnarray*} jest reguł± \begin{eqnarray*}MP\end{eqnarray*}. Przykładowo pokażemy wyprowadzenie \begin{eqnarray*}$\vee$-elim\end{eqnarray*} oraz \begin{eqnarray*}PS\end{eqnarray*} w $H^{+}$, pozostawiaj±c Czytelnikowi wyprowadzenie pozostałych reguł.

Załóżmy, że mamy w $H^{+}$ dowody następuj±cych sekwentów:Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi\vee\psi} , \hspace{.1cm}Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi\vdash\vartheta} \hspace{.1cm}oraz \hspace{.1cm}$\mathrm{\Delta },\psi ⊢\vartheta$. Wówczas, stosuj±c aksjomat \begin{eqnarray*}B2\end{eqnarray*} i regułę \begin{eqnarray*}MP\end{eqnarray*} mamyParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{H^+}\neg\var\varphi\arr\psi} .Zatem Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\neg\var\varphi\vdash_{H^+}\psi} i ponieważParser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \Delta\vdash_{H^+}\psi\arr\vartheta} to również Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\neg\var\varphi\vdash_{H^+}\psi\arr\vartheta} . St±dParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\neg\var\varphi\vdash_{H^+}\vartheta} . Stosuj±c twierdzenie o dedukcji dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{H^+}\neg\var\varphi\arr\vartheta} . Skoro mamy również \mbox{Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \delta\vdash_{H^+}\var\varphi\arr\vartheta} }, to na mocyLematu [[#le-zda-1}\begin{eqnarray*}3\end{eqnarray*} otrzymujemy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \Delta\vdash_{H^+]]\vartheta} .

Dla wyprowadzenia \begin{eqnarray*}PS\end{eqnarray*} załóżmy, żeParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\neg\var\varphi\vdash_{H^+}\bot} . Z twierdzenia o dedukcjidostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{H^+}\neg\neg\var\varphi} . Tak więc z\begin{eqnarray*}A3\end{eqnarray*} i \begin{eqnarray*}MP\end{eqnarray*} dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{H^+}\var\varphi} .

Dla pokazania \rightarrowlikacji odwrotnej wystarczy pokazać, że wszystkieaksjomaty systemu $H^{+}$ s± twierdzeniami systemu naturalnej dedukcji. Wyprowadzenia \begin{eqnarray*}A1\end{eqnarray*} i\begin{eqnarray*}A3\end{eqnarray*} w ND zostały podane w Przykładzie #pr-zda-2. Przykładowo pokażemy wyprowadzenia\begin{eqnarray*}A2\end{eqnarray*} i \begin{eqnarray*}B1\end{eqnarray*}. Zaczniemy od wyprowadzenia \begin{eqnarray*}A2\end{eqnarray*}. NiechParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta=\{\var\varphi\arr\begin{eqnarray*}\psi\arr\vartheta\end{eqnarray*},\ \var\varphi\arr\psi,\ \var\varphi\}} .Mamy następuj±cy dowód:

Parser nie mógł rozpoznać (nieznana funkcja „\arelim”): {\displaystyle \arelim{\areli\prooftree \se\var\varphi\arr\begin{eqnarray*}\psi\arr\vartheta\end{eqnarray*} \justifies \se\var\varphi \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree{\se\psi\arr\vartheta}}{\areli\prooftree \se\var\varphi\arr\psi}{\se\var\varphi}{\se\psi} \justifies \se\vartheta \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree} Stosuj±c trzy razy \begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr\mbox{-intro}} \end{eqnarray*} do sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\se”): {\displaystyle \se\vartheta} dostajemy wyprowadzenie aksjomatu \begin{eqnarray*}A2\end{eqnarray*}.

Następnie pokażemy dowód \begin{eqnarray*}B1\end{eqnarray*} w ND. Zaczniemy odwyprowadzenia \mbox{Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\var\varphi} }, gdzieParser nie mógł rozpoznać (błąd składni): {\displaystyle \Delta=\{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}, \neg\var\varphi\}} : Parser nie mógł rozpoznać (nieznana funkcja „\ps”): {\displaystyle \ps{\arelim{\arintro{\arintro{\arelim{\Delta,\var\varphi,\psi\vdash\neg\var\varphi}{\Delta,\var\varphi,\psi\vdash\var\varphi}{\Delta,\var\varphi,\psi\vdash\bot}}{\Delta,\var\varphi\vdash\neg\psi}}{\se\var\varphi\arr\neg\psi}}{\se\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}}{\se\bot}}{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\var\varphi}} Następnie wyprowadzimy sekwent Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\psi} . NiechParser nie mógł rozpoznać (błąd składni): {\displaystyle \Delta=\{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}, \neg\psi\}} Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\prooftree \arelim{\arintro{\Delta,\var\varphi\vdash\neg\psi \justifies \se\var\varphi\arr\neg\psi} \using \textrm{\begin{eqnarray*}PS\end{eqnarray*}}\endprooftree{\se\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}}{\se\bot}}{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\psi}}

Maj±c wyprowadzone sekwenty Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\var\varphi} oraz Parser nie mógł rozpoznać (błąd składni): {\displaystyle \neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\psi} możemy zakończyć dowód \begin{eqnarray*}B1\end{eqnarray*}. Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \arintro{\wedgeintro{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\var\varphi}{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\psi}{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\var\varphi\wedge\psi}}{\vdash\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\arr\begin{eqnarray*}\var\varphi\wedge\psi\end{eqnarray*}}} \vspace{-10mm}

\hfil\hfil\hfil\hfil\qed\end{dowodbezqed}

Dla przedstawienia rachunku sekwentów rozszerzymy nieco pojęciesekwentu. Przez sekwent\/ będziemy teraz rozumieć napis$\mathrm{\Delta }⊢\mathrm{\Gamma }$, gdzie $\mathrm{\Delta }$ oraz $\mathrm{\Gamma }$ s± skończonymizbiorami formuł. Intuicyjnie, wyprowadzalno¶ć sekwentu$\mathrm{\Delta }⊢\mathrm{\Gamma }$ w rachunku sekwentów będzie oznaczać, żealternatywa formuł z $\mathrm{\Gamma }$ wynika z hipotez $\mathrm{\Delta }$.

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

Charakterystyczn± cech± rachunku sekwentów jest specyficzna postać reguł. Reguły w tym systemie naturalnie dziel± się na dwie grupy: jedna grupa reguł opisuje sytuacje kiedy możemy wprowadzić dany spójnik na lewo od znaku $⊢$, a druga grupa jest odpowiedzialna za wprowadzanie spójnika na prawo od $⊢$. Dla każdego spójnika mamy odpowiadaj±c± parę reguł.Aksjomat \begin{eqnarray*}A$\mathrm{\perp }$\end{eqnarray*} można traktować jako regułę \begin{eqnarray*}bezprzesłanek\end{eqnarray*} wprowadzenia $\mathrm{\perp }$ z lewej strony znaku $⊢$.

Przypomnijmy, że napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi_1,\ldots,\var\varphi_n} oznacza zbiór Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\cup\{\var\varphi_1,\ldots,\var\varphi_n\}} .

\vspace{.5cm}\noindentAksjomaty

\begin{eqnarray*}A00\end{eqnarray*}  Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi\vdash\Gamma,\var\varphi}

\begin{eqnarray*}A$\mathrm{\perp }$\end{eqnarray*}  $\mathrm{\Delta },\mathrm{\perp }⊢\mathrm{\Gamma }$

\vspace{.5cm}\noindentReguły dowodzenia\\ Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\arr\mbox{-lewa}\end{eqnarray*}\hspace{.2cm} \frac{\Delta\vdash\Gamma,\var\varphi\\hspace{1cm} \Delta,\psi\vdash\Gamma}{\Delta,\var\varphi\arr\psi\vdash\Gamma}\hspace{1cm}\begin{eqnarray*}\arr\mbox{-prawa}\end{eqnarray*}\hspace{.2cm}\frac{\Delta,\var\varphi\vdash\Gamma,\psi}{\Delta\vdash\Gamma,}

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\wedge\mbox{-lewa}\end{eqnarray*}\hspace{.2cm} \fra\prooftree \Delta,\var\varphi,\psi\vdash\Gamma \justifies \Delta,\var\varphi\wedge\psi\vdash\Gamma \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\hspace{1cm} \begin{eqnarray*}\wedge\mbox{-prawa}\end{eqnarray*}\hspace{.2cm}\frac{\Delta\vdash\Gamma, \var\varphi\\hspace{1cm}}

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

{\em Dowodem} sekwentu $\mathrm{\Delta }⊢\mathrm{\Gamma }$, tak jak poprzednio,nazywamy drzewo\Delta\vdashtykietowane sekwentami tak, że korzeń jestetykietowany przez $\mathrm{\Delta }⊢\mathrm{\Gamma }$, li¶cie s±\Delta\vdashtykietowaneaksjomatami oraz wierzchołki wewnętrznes±\Delta\vdashtykietowane sekwentami otrzymanymi poprawnie przez zastosowaniereguł dowodzenia. Je¶li istnieje dowód sekwentu$\mathrm{\Delta }⊢\mathrm{\Gamma }$ w rachunku sekwentów to zapisujemy to tak:$\mathrm{\Delta }{⊢}_G\mathrm{\Gamma }$. \begin{eqnarray*}Litera G pochodzi od nazwiska twórcy tegosystemu, G. Gentzena.\end{eqnarray*} Piszemy też Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{G}\var\varphi} , gdy $\mathrm{\Delta }$jest nieskończony, ale Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_G\var\varphi} dla pewnego skończonego ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$.

Zauważmy, że je¶li mamy sekwent Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\Gamma,\var\varphi} tostosuj±c aksjomat \begin{eqnarray*}A

$\mathrm{\perp }$

\end{eqnarray*}, a następnie \begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} -lewa\end{eqnarray*} dostajemysekwent Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\neg\var\varphi\vdash\Gamma} . Zatem natępuj±ca regułajest dopuszczalna\/ w systemie

${⊢}_G$

\begin{eqnarray*}tj. je¶li dodamy j± do systemu, to zbiór wyprowadzalnych sekwentów nie\boldsymbol{s}}\def\blank{\hbox{\sf Blegnie zmianie\end{eqnarray*}:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\neg\mbox{-lewa}\end{eqnarray*}\hspace{.2cm} } Ponadto zauważmy, że je¶li mamy dowód sekwentu$\mathrm{\Delta }⊢\mathrm{\Gamma }$, to dla każdej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} możemy j±dodać do prawej strony każdego sekwentu w tym dowodzie i otrzymamydowód sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\Gamma,\var\varphi} .Łatwy dowód indukcyjny pozostawiamy Czytelnikowi \begin{eqnarray*}Ćwiczenie #weakening\end{eqnarray*}. W szczególno¶ci,je¶li mamy\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodniony sekwent Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi\vdash\Gamma} , to możemy teżudowodnić sekwent Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\var\varphi\vdash\Gamma,\bot} . Stosuj±c doniego regułę \begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} -prawa\end{eqnarray*} otrzymujemy sekwentParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\Gamma,\neg\var\varphi} . Tym samym pokazali¶my, żenastępuj±ca reguła jest dopuszczalna w systemie ${⊢}_G$: Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\neg\mbox{-prawa}\end{eqnarray*}\hspace{.2cm} }

Twierdzenie

Dla każdych $\mathrm{\Delta }$ i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} mamy następuj±c± równoważno¶ć</math>\Delta\vdash_G\var\varphi\hspace{.2cm}\mbox{ wtedy i tylko wtedy, gdy }\hspace{.2cm} \Delta\vdash_{H^+}\var\varphi.</math>

Powyższe twierdzenie pozostawimy bez dowodu. Łatwo jest ,,przetłumaczyć każde wyprowadzenie w systemie ${⊢}_G$na dowód w stylu Hilberta. Dla dowodu \rightarrowlikacji odwrotnej rozszerza się system ${⊢}_G$ przezdodanie nowej reguły zwanej {\em cięciem}. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\mbox{cięcie}\end{eqnarray*}\hspace{.2cm} \frac{\Delta,\var\varphi\vdash\Gamma\hspace{.7cm} } Niech ${⊢}_{GC}$ oznacza system gentzenowski z cięciem. Bez trudu możnapokazać, że reguła odrywania jest dopuszczalna w${⊢}_{GC}$. Zatem, korzystaj±c z twierdzenia o pełno¶ci dlasystemu hilbertowskiego, łatwo pokazujemy, że każda tautologiajest twierdzeniem systemu ${⊢}_{GC}$. Główna trudno¶ć w dowodzie Twierdzenia #milo polega na udowodnieniu następuj±cego twierdzenia {\em o\Delta\vdashliminacji cięcia}.Twierdzenie to podajemy bez dowodu.

Twierdzenie o\Delta\vdashliminacji cięcia

Je¶li$\mathrm{\Delta }{⊢}_{GC}\mathrm{\Gamma }$, to $\mathrm{\Delta }{⊢}_G\mathrm{\Gamma }$.

G\lówna zaleta dowodów w rachunku sekwentów \begin{eqnarray*}bez cięcia\end{eqnarray*} wynika z następuj±cejwłasno¶ci podformu\l:\/ wszystkie formuły występuj±cew przesłance dowolnej reguły s± podformułami formu\l\ występuj±cych w konkluzji. Zatem np. w dowodzie sekwentu Parser nie mógł rozpoznać (błąd składni): {\displaystyle &nbsp;\vdash\var\varphi} mamy do czynienia tylko z podformułami formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Dla danej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , łatwiej więc znaleĽć dowód w sensie Gentzena niż np. dowód w sensieHilberta. Dlatego systemy zbliżone do rachunku sekwentów znajduj± zastosowanie w automatycznymdowodzeniu twierdzeń. Pokażemy to na przykładzie.

Przykład

\

1. Poszukamy dowodu sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash\neg\neg\var\varphi\arr\var\varphi} w${⊢}_G$. Ponieważ najbardziej zewnętrznym spójnikiem wrozważanej formule jest Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} , to ostatni± reguł± w poszukiwanymdowodzie musiała być reguła \begin{eqnarray*}Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \arr} -prawa\end{eqnarray*}. Zatem wystarczyznaleĽć dowód sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\neg\var\varphi\vdash\var\varphi} . Najbardziejzewnętrznym spójnikiem formuły po lewej stronie jest $\mathrm{\neg }$, azatem na mocy reguły \begin{eqnarray*}$\mathrm{\neg }$-lewa\end{eqnarray*} wystarczy\boldsymbol{s

\def\blank{\hbox{\sf Bdowodnić sekwentParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \vdash\var\varphi, \neg\var\varphi} . Podobnie, na mocy reguły \mbox{\begin{eqnarray*}$\mathrm{\neg }$-prawa\end{eqnarray*}},wystarczy\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić sekwent Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\vdash\var\varphi} , a on przecież jestaksjomatem.

Je¶li zastosujemy powyższ± procedurę do formuły, któranie jest tautologi±, to dostaniemy wskazówkę na to gdzie należy szukać warto¶ciowania falsyfikuj±cego tę formułę. \begin{eqnarray*}Warto¶ciowanie falsyfikuj±ce sekwent $\mathrm{\Delta }⊢\mathrm{\Gamma }$ to takie,które spełnia wszystkie formuły z $\mathrm{\Delta }$ oraz falsyfikujewszystkie formuły z $\mathrm{\Gamma }$.\end{eqnarray*}Dla zilustrowania tej tezy weĽmy bardzo prostysekwent Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vdash p\arr q} . Postępuj±c podobnie jak porzedniodochodzimy do sekwentu $p⊢q$, który nie jestaksjomatem, 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\l\ 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 wyprowadzenienie wymaga regu\l\ zwi±zanych z tym spójnikiem.

\subsection*{Ćwiczenia}\begin{small}

1. Niech ${⊢}_{H_1}$ oznacza system dowodzenia otrzymanyz systemu ${⊢}_H$ przez zamianę aksjomatu \begin{eqnarray*}A3\end{eqnarray*} na następuj±cy aksjomat:

\begin{eqnarray*}A3'\end{eqnarray*}  </math>\begin{eqnarray*}\neg\var\varphi\arr\neg\psi\end{eqnarray*}\arr\begin{eqnarray*}\begin{eqnarray*}\neg\var\varphi\arr\psi\end{eqnarray*}\arr\var\varphi\end{eqnarray*}.</math>

Dowie¶ć, że obydwa systemy s± równoważne, tzn., że dladowolnego sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} , zachodziParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} \wtw, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{H_1}\var\varphi} .

1. Niech ${⊢}_{H_2}$ oznacza system dowodzenia otrzymanyz systemu ${⊢}_H$ przez zamianę aksjomatu \begin{eqnarray*}A3\end{eqnarray*} na ${⊢}_H$,następuj±cy aksjomat:

\begin{eqnarray*}A3\end{eqnarray*}  Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\neg\var\varphi\arr\neg\psi\end{eqnarray*}\arr\begin{eqnarray*}\psi\arr\var\varphi\end{eqnarray*}.}

Dowie¶ć, że obydwa systemy s± równoważne, tzn., że dladowolnego sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} , zachodziParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi} \wtw, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{H_2}\var\varphi} .

1. Dowie¶ć, że aksjomatu \begin{eqnarray*}A3\end{eqnarray*} nie da się wyprowadzić zaksjomatów \begin{eqnarray*}A0--2\end{eqnarray*} przy pomocy reguły odrywania.

1. Dowie¶ć Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vdash_H\neg p \arr\begin{eqnarray*}p\arr q\end{eqnarray*}} \boldsymbol{s}}\def\blank{\hbox{\sf Bżywaj±c twierdzenia odedukcji oraz bez\boldsymbol{s}}\def\blank{\hbox{\sf Bżycia tego twierdzenia.

1. Pokazać, że w systemie ${⊢}_H$ dopuszczalna jestnastępuj±ca reguła: Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \frac{\var\varphi\arr\psi\\hspace{1cm} } tzn. pokazać, że je¶li Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\var\varphi\arr\psi} oraz $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\psi$, to również mamy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_H\neg\var\varphi} .

1. Dowie¶ć, że dla każdej formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , nie będ±cejtautologi±, istnieje maksymalny zbiór formuł $\mathrm{\Delta }$ \begin{eqnarray*}nad dan± sygnatur±\end{eqnarray*}o tej własno¶ci, żeParser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\not\vdash_H\var\varphi} .

1. Każdy z poniższych sekwentów wyprowadzić w systemie${⊢}_{H^{+}}$, ${⊢}_N$, ${⊢}_G$.
   1. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vdash \bot\arr p} ;
   2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle p\arr q,q\arr r\vdash p\arr r} ;
   3. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \vdash\begin{eqnarray*}\neg p\arr p\end{eqnarray*}\arr p} ;
   4. $p,\mathrm{\neg }p⊢q$;
   5. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle p\arr\begin{eqnarray*}q\arr r\end{eqnarray*}\vdash q\arr\begin{eqnarray*}p\arr r\end{eqnarray*}} ;
   6. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \vdash \begin{eqnarray*}\neg p\arr \neg q\end{eqnarray*}\arr \begin{eqnarray*}q\arr p\end{eqnarray*}} ;
   7. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \vdash \neg\begin{eqnarray*}p\wedge q\end{eqnarray*}\arr\begin{eqnarray*}\neg p\vee\neg q\end{eqnarray*}} .

\item Dowie¶ć, że je¶li Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{N}\var\varphi} , to dla dowolnejformuły $\psi$ zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta,\psi\vdash_{N}\var\varphi} .

\item Dowie¶ć, że je¶li $\mathrm{\Delta }{⊢}_N\mathrm{\perp }$, to dla dowolnejformuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} zachodzi Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash_{N}\var\varphi} .

\item Dla każdego z sytemów ${⊢}_{H^{+}}$, ${⊢}_N$,${⊢}_G$ dowie¶ć, że je¶li sekwent Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} jestwyprowadzalny w tym systemie oraz $S$ jest podstawieniem formuł nazmienne zdaniowe, to sekwent Parser nie mógł rozpoznać (błąd składni): {\displaystyle \vec{S}\begin{eqnarray*}\Delta\end{eqnarray*}\vdash S\begin{eqnarray*}\var\varphi\end{eqnarray*}} powstaj±cy w wyniku podstawienia jest też wyprowadzalny w tym systemie.\item Udowodnić, że w rachunku sekwentów zamiana reguły Parser nie mógł rozpoznać (błąd składni): {\displaystyle \begin{eqnarray*}\vee\mbox{-prawa}\end{eqnarray*}} na dwie reguły: Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \prooftree{\Delta\vdash\Gamma,\var\varphi} \justifies{\Delta\vdash\Gamma,\var\varphi\vee\psi}\endprooftree\hspace{3cm} \prooftree{\Delta\vdash\Gamma,\psi}\justifies{\Delta\vdash\Gamma,\var\varphi\vee\psi}} daje w wyniku równoważny system dowodzenia\begin{eqnarray*}wyprowadzalne s± te same sekwenty\end{eqnarray*}.

\item Udowodnić, że następuj±ce reguły osłabiania\/ s± dopuszczalnew rachunku sekwentów: Parser nie mógł rozpoznać (nieznana funkcja „\prooftree”): {\displaystyle \prooftree{\Delta\vdash\Gamma}\justifies{\Delta,\var\varphi\vdash\Gamma} \endprooftree\hspace{3cm} \prooftree{\Delta\vdash\Gamma}\justifies{\Delta\vdash\Gamma,\var\varphi}} \item Wyprowadzić w rachunku sekwentów:

1. $⊢p\vee \mathrm{\neg }p$;
2. Parser nie mógł rozpoznać (błąd składni): {\displaystyle \vdash \begin{eqnarray*}\begin{eqnarray*}p\to q\end{eqnarray*}\to p\end{eqnarray*}\to p} .

Czy można to zrobić\boldsymbol{s}}\def\blank{\hbox{\sf Bżywaj±c tylko sekwentów postaci Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Delta\vdash\var\varphi} \begin{eqnarray*}z jedn± formuł± po prawej\end{eqnarray*}?