|
|
| Linia 1: |
Linia 1: |
|
| |
|
| |
| Sprawdzenie, czy dana formuła rachunku zdań jest tautologi±, polega zwykle na obliczeniu jej warto¶ci dla <math>2^n</math> różnych warto¶ciowań,gdzie <math>n</math> jest liczb± zmiennych zdaniowych tej formuły. Jak dot±d nie s± znane radykalnie szybsze metody. Dla rachunkupredykatów nie istnieje w 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. | | Sprawdzenie, czy dana formuła rachunku zdań jest tautologi±, polega zwykle na obliczeniu jej warto¶ci dla <math>2^n</math> różnych warto¶ciowań,gdzie <math>n</math> jest liczb± zmiennych zdaniowych tej formuły. Jak dot±d nie s± znane radykalnie szybsze metody. Dla rachunkupredykatów nie istnieje w 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. |
|
| |
|
| Linia 155: |
Linia 153: |
|
| |
|
| </math> | | </math> |
|
| |
| Zauważmy, że szczególnym przypadkiem reguły \begin{eqnarray*}<math>\arr</math>-intro\end{eqnarray*} jestnastępuj±ca reguła, można j± traktować jak regułę wprowadzenia negacji.<span id=""/> <math> \frac{\Delta,\var\varphi\vdash\bot}
| |
|
| |
|
| |
|
| |
| </math>
| |
|
| |
|
| |
|
| |
|
| |
|
| |
| Zauważmy też, że szczególnym przypadkiem reguły \begin{eqnarray*}<math>\arr</math>-elim\end{eqnarray*} jestnastępuj±ca reguła, można j± traktować jak regułę\Delta\vdashliminacji negacji.<span id=""/> <math> \frac{\Delta\vdash\neg\var\varphi\quad
| |
|
| |
|
| |
|
| |
| </math>
| |
|
| |
| 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\/} sekwentu<math>\Delta\vdash\var\varphi</math> w systemie naturalnej dedukcji nazwiemy drzewoetykietowane sekwentami tak, że korzeń ma\Delta\vdashtykietę\mbox{<math>\Delta\vdash\var\varphi</math>}, 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 <math>\Delta\vdash_{N}\var\varphi</math>, gdy sekwent <math>\Delta\vdash\var\varphi</math> ma dowód w systemie naturalnej dedukcji. Gdy <math>\Delta=\emptyset</math>, to mówimy też, że <math>\var\varphi</math> jest ''twierdzeniem\/'' systemu naturalnej dedukcji i zapisujemy to przez <math>\vdash_N\var\varphi</math>.Je¶li <math>\Delta</math> jest zbiorem nieskończonym, to<math>\Delta\vdash_{N}\var\varphi</math> oznacza, że istnieje dowód sekwentu </math>\Delta_0\vdash\var\varphi<math>, dla pewnego skończonego </math>\Delta_0\subseteq\Delta</math>.
| |
|
| |
|
| |
|
| |
| Poniżej podajemy kilka przykładów dowodów w systemie naturalnejdedukcji.
| |
|
| |
|
| |
|
| |
|
| |
|
| |
| {{przyklad||pr-zda-2|
| |
|
| |
|
| |
|
| |
| \
| |
| *Pokażemy <math>\vdash_{N}p\arr p</math>.\[\arintr\prooftree p\vdash p \justifies \vdash p\arr p \using \textrm{\begin{eqnarray*}W\end{eqnarray*}}\endprooftree\]
| |
|
| |
|
| |
| *Pokażemy <math>\vdash_{N} p\arr\begin{eqnarray*}q\arr p\end{eqnarray*}</math>.\[\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 <math>\vdash_{N}\neg\neg p\arr p</math>.
| |
|
| |
| \[\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||malpamysli|
| |
|
| |
|
| |
|
| |
| Dla dowolnego sekwentu <math>\Delta\vdash\var\varphi</math> 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 <math>\vdash_{N}</math> daje się przerobićna dowód w <math>\vdash_{H^+}</math> wystarczy sprawdzić, że każda z regułsystemu naturalnej dedukcji jest ''dopuszczalna\/'' w <math>H^+</math>. Tzn. wystarczy sprawdzić, że je¶li mamy dowody przesłanek w <math>\vdash_{H^+}</math>, to możemy\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić konkluzję. Zauważmy, żewyprowadzalno¶ć reguły\begin{eqnarray*}<math>\arr</math>-intro\end{eqnarray*} jest konsekwencj± twierdzeniao dedukcji, natomiast reguła \begin{eqnarray*}<math>\arr</math>-elim\end{eqnarray*} jest reguł± \begin{eqnarray*}MP\end{eqnarray*}. Przykładowo pokażemy wyprowadzenie \begin{eqnarray*}<math>\vee</math>-elim\end{eqnarray*} oraz \begin{eqnarray*}PS\end{eqnarray*} w <math>H^+</math>, pozostawiaj±c Czytelnikowi wyprowadzenie pozostałych reguł.
| |
|
| |
| Załóżmy, że mamy w <math>H^+</math> dowody następuj±cych sekwentów:<math>\Delta\vdash\var\varphi\vee\psi</math>, \hspace{.1cm}<math>\Delta,\var\varphi\vdash\vartheta</math> \hspace{.1cm}oraz \hspace{.1cm}<math>\Delta,\psi\vdash\vartheta</math>. Wówczas, stosuj±c aksjomat \begin{eqnarray*}B2\end{eqnarray*} i regułę \begin{eqnarray*}MP\end{eqnarray*} mamy<math>\Delta\vdash_{H^+}\neg\var\varphi\arr\psi</math>.Zatem <math>\Delta,\neg\var\varphi\vdash_{H^+}\psi</math> i ponieważ<math>\Delta\vdash_{H^+}\psi\arr\vartheta</math> to również <math>\Delta,\neg\var\varphi\vdash_{H^+}\psi\arr\vartheta</math>. St±d<math>\Delta,\neg\var\varphi\vdash_{H^+}\vartheta</math>. Stosuj±c twierdzenie o dedukcji dostajemy <math>\Delta\vdash_{H^+}\neg\var\varphi\arr\vartheta</math>. Skoro mamy również \mbox{<math>\delta\vdash_{H^+}\var\varphi\arr\vartheta</math>}, to na mocyLematu [[#le-zda-1}\begin{eqnarray*}3\end{eqnarray*} otrzymujemy <math>\Delta\vdash_{H^+]]\vartheta</math>.
| |
|
| |
| Dla wyprowadzenia \begin{eqnarray*}PS\end{eqnarray*} załóżmy, że<math>\Delta,\neg\var\varphi\vdash_{H^+}\bot</math>. Z twierdzenia o dedukcjidostajemy <math>\Delta\vdash_{H^+}\neg\neg\var\varphi</math>. Tak więc z\begin{eqnarray*}A3\end{eqnarray*} i \begin{eqnarray*}MP\end{eqnarray*} dostajemy <math>\Delta\vdash_{H^+}\var\varphi</math>.
| |
|
| |
| Dla pokazania \rightarrowlikacji odwrotnej wystarczy pokazać, że wszystkieaksjomaty systemu <math>H^+</math> 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*}. Niech<math>\Delta=\{\var\varphi\arr\begin{eqnarray*}\psi\arr\vartheta\end{eqnarray*},\ \var\varphi\arr\psi,\ \var\varphi\}</math>.Mamy następuj±cy dowód:
| |
|
| |
| <span id=""/> <math>
| |
|
| |
|
| |
|
| |
| \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</math>Stosuj±c trzy razy \begin{eqnarray*}<math>\arr\mbox{-intro}</math>\end{eqnarray*} do sekwentu <math>\se\vartheta</math>dostajemy wyprowadzenie aksjomatu \begin{eqnarray*}A2\end{eqnarray*}.
| |
|
| |
|
| |
|
| |
| Następnie pokażemy dowód \begin{eqnarray*}B1\end{eqnarray*} w ND. Zaczniemy odwyprowadzenia \mbox{<math>\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\var\varphi</math>}, gdzie<math>\Delta=\{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}, \neg\var\varphi\}</math>:<span id=""/> <math>
| |
|
| |
|
| |
|
| |
| \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}</math><!--%-->Następnie wyprowadzimy sekwent <math>\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\psi</math>. Niech<math>\Delta=\{\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}, \neg\psi\}</math><span id=""/> <math>
| |
|
| |
|
| |
|
| |
| \\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}</math>
| |
|
| |
| Maj±c wyprowadzone sekwenty <math>\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\var\varphi</math>oraz <math>\neg\begin{eqnarray*}\var\varphi\arr\neg\psi\end{eqnarray*}\vdash\psi</math> możemy zakończyć dowód \begin{eqnarray*}B1\end{eqnarray*}. <span id=""/> <math>
| |
|
| |
|
| |
|
| |
| \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*}}</math>\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<math>\Delta\vdash\Gamma</math>, gdzie <math>\Delta</math> oraz <math>\Gamma</math> s± skończonymizbiorami formuł. Intuicyjnie, wyprowadzalno¶ć sekwentu<math>\Delta\vdash\Gamma</math> w rachunku sekwentów będzie oznaczać, żealternatywa formuł z <math>\Gamma</math> wynika z hipotez <math>\Delta</math>.
| |
|
| |
| Podobnie jak w poprzedniej czę¶ci, rozważamy formuły, zbudowane w oparciu o spójniki <math>\arr,\vee,\wedge</math> oraz stał±zdaniow± <math>\bot</math>. Negację <math>\neg</math> traktujemy jako spójnikzdefiniowany przez <math>\arr</math> i <math>\bot</math>.
| |
|
| |
| Charakterystyczn± cech± rachunku sekwentów jest specyficzna postać reguł. Reguły w tym systemie naturalnie dziel± się na dwie grupy: jedna grupa reguł opisuje sytuacje kiedy możemy wprowadzić dany spójnik na lewo od znaku <math>\vdash</math>, a druga grupa jest odpowiedzialna za wprowadzanie spójnika na prawo od <math>\vdash</math>. Dla każdego spójnika mamy odpowiadaj±c± parę reguł.Aksjomat \begin{eqnarray*}A<math>\bot</math>\end{eqnarray*} można traktować jako regułę \begin{eqnarray*}bezprzesłanek\end{eqnarray*} wprowadzenia <math>\bot</math> z lewej strony znaku <math>\vdash</math>.
| |
|
| |
| Przypomnijmy, że napis <math>\Delta,\var\varphi_1,\ldots,\var\varphi_n</math> oznacza zbiór <math>\Delta\cup\{\var\varphi_1,\ldots,\var\varphi_n\}</math>.
| |
|
| |
| \vspace{.5cm}\noindent'''Aksjomaty'''
| |
|
| |
| \begin{eqnarray*}A00\end{eqnarray*} <math>\Delta,\var\varphi\vdash\Gamma,\var\varphi</math>
| |
|
| |
| \begin{eqnarray*}A<math>\bot</math>\end{eqnarray*} <math>\Delta,\bot\vdash\Gamma</math>
| |
|
| |
| \vspace{.5cm}\noindent'''Reguły dowodzenia'''\\<span id=""/> <math> \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,</math>
| |
|
| |
| <span id=""/> <math> \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}</math>
| |
|
| |
| <span id=""/> <math> \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,</math>
| |
|
| |
| {\em Dowodem} sekwentu <math>\Delta\vdash\Gamma</math>, tak jak poprzednio,nazywamy drzewo\Delta\vdashtykietowane sekwentami tak, że korzeń jestetykietowany przez <math>\Delta\vdash\Gamma</math>, li¶cie s±\Delta\vdashtykietowaneaksjomatami oraz wierzchołki wewnętrznes±\Delta\vdashtykietowane sekwentami otrzymanymi poprawnie przez zastosowaniereguł dowodzenia. Je¶li istnieje dowód sekwentu<math>\Delta\vdash\Gamma</math> w rachunku sekwentów to zapisujemy to tak:<math>\Delta\vdash_G\Gamma</math>. \begin{eqnarray*}Litera G pochodzi od nazwiska twórcy tegosystemu, G. Gentzena.\end{eqnarray*} Piszemy też <math>\Delta\vdash_{G}\var\varphi</math>, gdy <math>\Delta</math>jest nieskończony, ale <math>\Delta\vdash_G\var\varphi</math> dla pewnego skończonego <math>\Delta_0 \subseteq\Delta</math>.
| |
|
| |
| Zauważmy, że je¶li mamy sekwent <math>\Delta\vdash\Gamma,\var\varphi</math> tostosuj±c aksjomat \begin{eqnarray*}A<math>\bot</math>\end{eqnarray*}, a następnie \begin{eqnarray*}<math>\arr</math>-lewa\end{eqnarray*} dostajemysekwent <math>\Delta,\neg\var\varphi\vdash\Gamma</math>. Zatem natępuj±ca regułajest ''dopuszczalna\/'' w systemie <math>\vdash_G</math> \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*}:<!--%--><span id=""/> <math> \begin{eqnarray*}\neg\mbox{-lewa}\end{eqnarray*}\hspace{.2cm}
| |
|
| |
|
| |
|
| |
| </math><!--%-->Ponadto zauważmy, że je¶li mamy dowód sekwentu<math>\Delta\vdash\Gamma</math>, to dla każdej formuły <math>\var\varphi</math> możemy j±dodać do prawej strony każdego sekwentu w tym dowodzie i otrzymamydowód sekwentu <math>\Delta\vdash\Gamma,\var\varphi</math>.Ł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 <math>\Delta,\var\varphi\vdash\Gamma</math>, to możemy teżudowodnić sekwent <math>\Delta,\var\varphi\vdash\Gamma,\bot</math>. Stosuj±c doniego regułę \begin{eqnarray*}<math>\arr</math>-prawa\end{eqnarray*} otrzymujemy sekwent<math>\Delta\vdash\Gamma,\neg\var\varphi</math>. Tym samym pokazali¶my, żenastępuj±ca reguła jest dopuszczalna w systemie <math>\vdash_G</math>:<!--%--><span id=""/> <math> \begin{eqnarray*}\neg\mbox{-prawa}\end{eqnarray*}\hspace{.2cm}
| |
|
| |
|
| |
|
| |
| </math><!--%-->{{twierdzenie||milo|
| |
|
| |
|
| |
|
| |
| Dla każdych <math>\Delta</math> i <math>\var\varphi</math> mamy następuj±c± równoważno¶ć</math></center>\Delta\vdash_G\var\varphi\hspace{.2cm}\mbox{ wtedy i tylko wtedy, gdy }\hspace{.2cm} \Delta\vdash_{H^+}\var\varphi.</math></center>}}
| |
|
| |
| Powyższe twierdzenie pozostawimy bez dowodu. Łatwo jest ,,przetłumaczyć'' każde wyprowadzenie w systemie <math>\vdash_G</math>na dowód w stylu Hilberta. Dla dowodu \rightarrowlikacji odwrotnej rozszerza się system <math>\vdash_G</math> przezdodanie nowej reguły zwanej {\em cięciem}.<!--%--><span id=""/> <math> \begin{eqnarray*}\mbox{cięcie}\end{eqnarray*}\hspace{.2cm} \frac{\Delta,\var\varphi\vdash\Gamma\hspace{.7cm}
| |
|
| |
|
| |
|
| |
| </math><!--%-->Niech <math>\vdash_{GC}</math> oznacza system gentzenowski z cięciem. Bez trudu możnapokazać, że reguła odrywania jest dopuszczalna w<math>\vdash_{GC}</math>. Zatem, korzystaj±c z twierdzenia o pełno¶ci dlasystemu hilbertowskiego, łatwo pokazujemy, że każda tautologiajest twierdzeniem systemu <math>\vdash_{GC}</math>. 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||
| |
|
| |
|
| |
|
| |
| <!--%%Dla każdego sekwentu <math>\Delta\vdash\Gamma</math>, j-->Je¶li<math>\Delta\vdash_{GC}\Gamma</math>, to <math>\Delta\vdash_G\Gamma</math>.}}
| |
|
| |
| G\lówna zaleta dowodów w rachunku sekwentów \begin{eqnarray*}bez cięcia\end{eqnarray*} wynika z następuj±cej''wł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 <math> \vdash\var\varphi</math> mamy do czynienia tylko z podformułami formuły <math>\var\varphi</math>. Dla danej formuły <math>\var\varphi</math>, ł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.
| |
|
| |
| {{przyklad|||
| |
|
| |
| \
| |
| #Poszukamy dowodu sekwentu <math>\vdash\neg\neg\var\varphi\arr\var\varphi</math> w<math>\vdash_G</math>. Ponieważ najbardziej zewnętrznym spójnikiem wrozważanej formule jest <math>\arr</math>, to ostatni± reguł± w poszukiwanymdowodzie musiała być reguła \begin{eqnarray*}<math>\arr</math>-prawa\end{eqnarray*}. Zatem wystarczyznaleĽć dowód sekwentu <math>\neg\neg\var\varphi\vdash\var\varphi</math>. Najbardziejzewnętrznym spójnikiem formuły po lewej stronie jest <math>\neg</math>, azatem na mocy reguły \begin{eqnarray*}<math>\neg</math>-lewa\end{eqnarray*} wystarczy\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić sekwent<math>\vdash\var\varphi, \neg\var\varphi</math>. Podobnie, na mocy reguły \mbox{\begin{eqnarray*}<math>\neg</math>-prawa\end{eqnarray*}},wystarczy\boldsymbol{s}}\def\blank{\hbox{\sf Bdowodnić sekwent <math>\var\varphi\vdash\var\varphi</math>, 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 <math>\Delta\vdash\Gamma</math> to takie,które spełnia wszystkie formuły z <math>\Delta</math> oraz falsyfikujewszystkie formuły z <math>\Gamma</math>.\end{eqnarray*}Dla zilustrowania tej tezy weĽmy bardzo prostysekwent <math>\vdash p\arr q</math>. Postępuj±c podobnie jak porzedniodochodzimy do sekwentu <math>p\vdash q</math>, 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 <math>p</math> i falsyfikuj±ce <math>q</math>.
| |
| }}
| |
|
| |
| 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}
| |
|
| |
|
| |
|
| |
|
| |
| #Niech <math>\vdash_{H_1}</math> oznacza system dowodzenia otrzymanyz systemu <math>\vdash_H</math> 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 <math>\Delta\vdash\var\varphi</math>, zachodzi<math>\Delta\vdash_H\var\varphi</math> \wtw, gdy <math>\Delta\vdash_{H_1}\var\varphi</math>.
| |
|
| |
|
| |
|
| |
|
| |
| #Niech <math>\vdash_{H_2}</math> oznacza system dowodzenia otrzymanyz systemu <math>\vdash_H</math> przez zamianę aksjomatu \begin{eqnarray*}A3\end{eqnarray*} na <math>\vdash_H</math>,następuj±cy aksjomat:
| |
|
| |
| \begin{eqnarray*}A3''\end{eqnarray*} <math>\begin{eqnarray*}\neg\var\varphi\arr\neg\psi\end{eqnarray*}\arr\begin{eqnarray*}\psi\arr\var\varphi\end{eqnarray*}.</math>
| |
|
| |
| Dowie¶ć, że obydwa systemy s± równoważne, tzn., że dladowolnego sekwentu <math>\Delta\vdash\var\varphi</math>, zachodzi<math>\Delta\vdash_H\var\varphi</math> \wtw, gdy <math>\Delta\vdash_{H_2}\var\varphi</math>.
| |
|
| |
|
| |
| #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.
| |
|
| |
|
| |
| #Dowie¶ć <math>\vdash_H\neg p \arr\begin{eqnarray*}p\arr q\end{eqnarray*}</math>\boldsymbol{s}}\def\blank{\hbox{\sf Bżywaj±c twierdzenia odedukcji oraz bez\boldsymbol{s}}\def\blank{\hbox{\sf Bżycia tego twierdzenia.
| |
|
| |
|
| |
| #Pokazać, że w systemie <math>\vdash_H</math> dopuszczalna jestnastępuj±ca reguła:<span id=""/> <math> \frac{\var\varphi\arr\psi\\hspace{1cm}
| |
|
| |
|
| |
|
| |
| </math>tzn. pokazać, że je¶li <math>\Delta\vdash_H\var\varphi\arr\psi</math> oraz <math>\Delta\vdash_H\neg\psi</math>, to również mamy <math> \Delta\vdash_H\neg\var\varphi</math>.
| |
|
| |
|
| |
| #Dowie¶ć, że dla każdej formuły <math>\var\varphi</math>, nie będ±cejtautologi±, istnieje maksymalny zbiór formuł <math>\Delta</math> \begin{eqnarray*}nad dan± sygnatur±\end{eqnarray*}o tej własno¶ci, że<math>\Delta\not\vdash_H\var\varphi</math>.
| |
|
| |
|
| |
| #Każdy z poniższych sekwentów wyprowadzić w systemie<math>\vdash_{H^+}</math>, <math>\vdash_{N}</math>, <math>\vdash_G</math>.
| |
| ##<math>\vdash \bot\arr p</math>;
| |
| ##<math>p\arr q,q\arr r\vdash p\arr r</math>;
| |
| ##<math>\vdash\begin{eqnarray*}\neg p\arr p\end{eqnarray*}\arr p</math>;
| |
| ##<math>p,\neg p\vdash q</math>;
| |
| ##<math>p\arr\begin{eqnarray*}q\arr r\end{eqnarray*}\vdash q\arr\begin{eqnarray*}p\arr r\end{eqnarray*}</math>;
| |
| ##<math>\vdash \begin{eqnarray*}\neg p\arr \neg q\end{eqnarray*}\arr \begin{eqnarray*}q\arr p\end{eqnarray*}</math>;
| |
| ##<math>\vdash \neg\begin{eqnarray*}p\wedge q\end{eqnarray*}\arr\begin{eqnarray*}\neg p\vee\neg q\end{eqnarray*}</math>.
| |
|
| |
|
| |
| \item Dowie¶ć, że je¶li <math>\Delta\vdash_{N}\var\varphi</math>, to dla dowolnejformuły <math>\psi</math> zachodzi <math>\Delta,\psi\vdash_{N}\var\varphi</math>.
| |
|
| |
| \item Dowie¶ć, że je¶li <math>\Delta\vdash_{N}\bot</math>, to dla dowolnejformuły <math>\var\varphi</math> zachodzi <math>\Delta\vdash_{N}\var\varphi</math>.
| |
|
| |
| \item Dla każdego z sytemów <math>\vdash_{H^+}</math>, <math>\vdash_{N}</math>,<math>\vdash_G</math> dowie¶ć, że je¶li sekwent <math>\Delta\vdash\var\varphi</math> jestwyprowadzalny w tym systemie oraz <math>S</math> jest podstawieniem formuł nazmienne zdaniowe, to sekwent <math>\vec{S}\begin{eqnarray*}\Delta\end{eqnarray*}\vdash S\begin{eqnarray*}\var\varphi\end{eqnarray*}</math>powstaj±cy w wyniku podstawienia jest też wyprowadzalny w tym systemie.\item <span id="prawa-addytywna" \> Udowodnić, że w rachunku sekwentów zamiana reguły <math>\begin{eqnarray*}\vee\mbox{-prawa}\end{eqnarray*}</math> na dwie reguły:<!--%--><span id=""/> <math> \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}</math><!--%-->daje w wyniku równoważny system dowodzenia\begin{eqnarray*}wyprowadzalne s± te same sekwenty\end{eqnarray*}.
| |
|
| |
| \item <span id="weakening" \> Udowodnić, że następuj±ce reguły ''osłabiania\/'' s± dopuszczalnew rachunku sekwentów:<!--%--><span id=""/> <math> \prooftree{\Delta\vdash\Gamma}\justifies{\Delta,\var\varphi\vdash\Gamma}
| |
|
| |
|
| |
|
| |
| \endprooftree\hspace{3cm} \prooftree{\Delta\vdash\Gamma}\justifies{\Delta\vdash\Gamma,\var\varphi}</math><!--%-->\item Wyprowadzić w rachunku sekwentów:
| |
| #<math>\vdash p\vee \neg p</math>;
| |
| #<math>\vdash \begin{eqnarray*}\begin{eqnarray*}p\to q\end{eqnarray*}\to p\end{eqnarray*}\to p</math>.
| |
| Czy można to zrobić\boldsymbol{s}}\def\blank{\hbox{\sf Bżywaj±c tylko sekwentów postaci <math>\Delta\vdash\var\varphi</math>\begin{eqnarray*}z jedn± formuł± po prawej\end{eqnarray*}?
| |
Sprawdzenie, czy dana formuła rachunku zdań jest tautologi±, polega zwykle na obliczeniu jej warto¶ci dla różnych warto¶ciowań,gdzie 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 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 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 \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 .
Przykład
Niech 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.
- 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*}
- 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*}
- 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*}
- 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*}
- 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± 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ł
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 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 . Druga możliwo¶ć jest taka, że lub też, że jest aksjomatem. W każdym z tychprzypadków mamy . Wówczas stosuj±c regułęodrywania do 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 jest zastosowanie reguły \begin{eqnarray*}MP\end{eqnarray*} do formuł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \vartheta\arr\psi}
oraz, dla pewnej formuły . 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 , następuj±ce formuły s± twierdzeniami systemu hilbertowskiego.
- 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*}}
;
- Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \bot\arr\var\varphi}
;
- 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 .
Twierdzenie
Dla dowolnego zbioru formuł
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 , 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 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 . 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} }
