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