Logika dla informatyków/Paradygmaty dowodzenia

Paradygmaty dowodzenia

{twierdzenie}{0}

Sprawdzenie, czy dana formuła rachunku zdań jest tautologi±, polega zwykle na obliczeniu jej warto¶ci dla $2^n$ różnych warto¶ciowań, gdzie $n$ jest liczb± zmiennych zdaniowych tej formuły. Jak dot±d nie s± znane radykalnie szybsze metody. Dla rachunku predykatów nie istnieje w ogóle żaden algorytm sprawdzania czy dana formuła jest tautologi± (Twierdzenie Uzupelnic entscheidungsproblem|). W obu przypadkach istniej± jednak metody dowodzenia pozwalaj±ce na wyprowadzanie prawdziwych formuł za pomoc± ustalonych procedur syntaktycznych.

Każdy system dowodzenia zawiera dwa składniki:

• pocz±tkowy zbiór formuł (lub wyrażeń zbudowanych z wielu formuł)

zwanych aksjomatami;

• zbiór operacji przekształcaj±cych wyrażenia w wyrażenia ---

operacje te s± nazywane regułami dowodzenia.

Reguły dowodzenia opisuj± warunki, przy pomocy których można otrzymać nowe wyrażenie (nazywane konkluzj±) z otrzymanych już wyrażeń (nazywanych przesłankami). Dowody w systemach formalnych s± ci±gami wyrażeń, być może posiadaj±cymi dodatkow± strukturę pozwalaj±c± na lepsz± wizualizację.

W dalszej czę¶ci opiszemy trzy systemy dowodzenia: system typu hilbertowskiego (od nazwiska Davida Hilberta), system naturalnej dedukcji oraz rachunek sekwentów. Ostatnie dwa systemy znajduj± zastosowanie w pewnych działach sztucznej inteligencji oraz w systemach automatycznego dowodzenia twierdzeń.

System hilbertowski

Poniższy system dowodzenia dotyczy formuł zbudowanych przy użyciu jedynie spójnika Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} , stałej $\mathrm{\perp }$ oraz zmiennych zdaniowych. Przypomnijmy, że dla dowolnej formuły $\phi$, napis $\mathrm{\neg }\phi$ jest skrótem zapisu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\bot} . Symbole $\phi ,\psi ,\vartheta$ w poniższym systemie oznaczaj± dowolne formuły.

Aksjomaty

(A1) Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr(\psi\arr\varphi)}
(A2) Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr(\psi\arr\vartheta))\arr((\varphi\arr\psi) \arr(\varphi\arr\vartheta))}
(A3) Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\varphi\arr\varphi}

Reguła dowodzenia

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle {\rm (MP)}\hspace{1cm} \frac{\varphi\odstep \varphi\arr\psi}{\psi}}

Reguła (MP) jest nazywana reguł± odrywania lub też reguł± modus ponens.

Dowodem w powyższym systemie nazywamy taki ci±g formuł, w którym każda formuła albo jest aksjomatem, albo też została otrzymana z wcze¶niej występuj±cych formuł w wyniku zastosowania reguły odrywania. Powiemy, że formuła $\phi$ ma dowód, lub jest twierdzeniem systemu hilbertowskiego, co zapiszemy ${⊢}_H\phi$, gdy istnieje dowód zawieraj±cy $\phi$. Powyższ± definicję możemy nieco uogólnić. Niech $\mathrm{\Delta }$ będzie dowolnym zbiorem formuł. Powiemy, że formuła $\phi$ ma dowód ze zbioru hipotez $\mathrm{\Delta }$ (notacja $\mathrm{\Delta }{⊢}_H\phi$), gdy $\phi$ 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 \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ć (nieznana funkcja „\arr”): {\displaystyle \displaystyle (p\arr((p\arr p)\arr p))\arr((p\arr(p\arr p))\arr(p\arr p))}

(A2)

1. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr((p\arr p)\arr p)} (A1)
2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (p\arr(p\arr p))\arr(p\arr p)} (1,2)
3. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr(p\arr p)} (A1)
4. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle p\arr p} (3,4)

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

Następuj±ce twierdzenie jest bardzo użyteczne, gdy trzeba uzasadnić, że jaka¶ formuła jest twierdzeniem.

Twierdzenie o dedukcji

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

Dowód

Dowód jest indukcyjny ze względu na liczbę kroków w dowodzie formuły $\psi$ ze zbioru hipotez $\mathrm{\Delta }\cup \{\phi \}$. Przypu¶ćmy najpierw, że dowód ten składa się tylko z jednego kroku. Je¶li $\psi =\phi$, to stosuj±c wyprowadzenie z Przykładu Uzupelnic pr-zda-1a| dostajemy dowód formuły Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\varphi} . Możemy oczywi¶cie przyj±ć, że formuła ta jest wyprowadzona ze zbioru hipotez $\mathrm{\Delta }$. Druga możliwo¶ć jest taka, że $\psi \in \mathrm{\Delta }$ lub też, że $\psi$ jest aksjomatem. W każdym z tych przypadkó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 \displaystyle \psi\arr(\varphi\arr\psi)} dostajemy formułę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} .

Założmy teraz, że ostatnim krokiem w wyprowadzeniu formuły $\psi$ jest zastosowanie reguły (MP) do formuł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vartheta\arr\psi} oraz $\vartheta$, dla pewnej formuły $\vartheta$. Z założenia indukcyjnego mamy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_H\varphi\arr (\vartheta\arr\psi)} oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_H\varphi\arr\vartheta} . Stosuj±c regułę odrywania do Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr (\vartheta\arr\psi)} oraz do aksjomatu (A2): Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr(\vartheta\arr\psi))\arr ((\varphi\arr\vartheta)\arr(\varphi\arr\psi))} dostajemy formułę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr\vartheta)\arr(\varphi\arr\psi)} . Ponownie stosuj±c regułę odrywania do tej formuły oraz do Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\vartheta} dostajemy ż±dan± formułę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} . To kończy dowód twierdzenia o dedukcji.

Twierdzenie o poprawno¶ci

Je¶li $\mathrm{\Delta }{⊢}_H\phi$, to $\mathrm{\Delta }\models \phi$. W szczególno¶ci, je¶li ${⊢}_H\phi$, to $\phi$ jest tautologi±.

Dowód

Dowód jest indukcyjny ze względu na liczbę kroków w wyprowadzeniu formuły $\phi$ w systemie hilbertowskim ze zbioru hipotez $\mathrm{\Delta }$. Je¶li dowód ten składa się tylko z jednego kroku to albo $\phi \in \mathrm{\Delta }$ albo $\phi$ jest aksjomatem. W obu przypadkach oczywi¶cie zachodzi $\mathrm{\Delta }\models \phi$.

Załóżmy teraz, że $\phi$ jest otrzymana przez zastosowanie reguły odrywania do formuł Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr\varphi} oraz $\psi$. Z założenia indukcyjnego mamy

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

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

Lemat

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

1. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi \arr(\neg\psi\arr\neg(\varphi\arr\psi))} ;
2. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \bot\arr\varphi} ;
3. Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\varphi\arr\psi)\arr((\neg\varphi\arr\psi)\arr\psi)} ;

Dowód

(1)  Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\varphi,\psi\arr\bot,\varphi\arr\psi\}} . Stosuj±c regułę odrywania do formuł $\phi$ oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} dostajemy $\psi$. Przez ponowne zastosowanie (MP) do tej formuły oraz do Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \psi\arr\bot} otrzymujemy wyprowadzenie $\mathrm{\perp }$. Tym samym pokazali¶my, że $\mathrm{\Delta }{⊢}_H\mathrm{\perp }$. Stosuj±c teraz trzy razy twierdzenie o dedukcji dostajemy

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\varphi\arr((\psi\arr\bot)\arr((\varphi\arr\psi)\arr\bot)),}

czyli

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\varphi \arr(\neg\psi\arr\neg(\varphi\arr\psi)).}

(2)  Ponieważ $\{\mathrm{\perp },\mathrm{\neg }\phi \}{⊢}_H\mathrm{\perp }$, więc z twierdzenia o dedukcji wynika $\mathrm{\perp }{⊢}_H\mathrm{\neg }\mathrm{\neg }\phi$. Stosuj±c teraz (MP) do tej formuły oraz do aksjomatu (A3) w postaci Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\varphi\arr\varphi} otrzymujemy $\mathrm{\perp }{⊢}_H\phi$. Ponowne zastosowanie twierdzenia o dedukcji daje nam Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H\bot\arr\varphi} .

(3)  Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\varphi\arr\psi,\neg\varphi\arr\psi\}} . Zaczynamy od zbioru hipotez $\mathrm{\Delta }\cup \{\phi ,\mathrm{\neg }\psi \}$. Stosuj±c (MP) do formuł $\phi$ oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\psi} dostajemy $\psi$. Ponowne zastosowanie (MP) do tej formuły oraz do $\mathrm{\neg }\psi$ daje nam $\mathrm{\perp }$. Używaj±c teraz twierdzenia o dedukcji do formuły $\mathrm{\perp }$ otrzymujemy

$\mathrm{\Delta }\cup \{\mathrm{\neg }\psi \}{⊢}_H\mathrm{\neg }\phi .$

Ponieważ mamy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\cup\{\neg\psi\}\vdash_H\neg\varphi\arr\psi} , to stosuj±c (MP) otrzymujemy $\mathrm{\Delta }\cup \{\mathrm{\neg }\psi \}{⊢}_H\psi$. Jeszcze raz używamy (MP) aby z $\mathrm{\neg }\psi$ i $\psi$ otrzymać $\mathrm{\perp }$ i mamy

$\mathrm{\Delta }\cup \{\mathrm{\neg }\psi \}{⊢}_H\mathrm{\perp }.$

Na mocy twierdzenia o dedukcji $\mathrm{\Delta }{⊢}_H\mathrm{\neg }\mathrm{\neg }\psi$. Stosuj±c (MP) do formuły $\mathrm{\neg }\mathrm{\neg }\psi$ oraz do aksjomatu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\neg\psi\arr\psi} otrzymujemy $\mathrm{\Delta }{⊢}_H\psi$. Dwukrotne zastosowanie twierdzenia o dedukcji daje nam Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_H(\varphi\arr\psi)\arr((\neg\varphi\arr\psi)\arr\psi)} . To kończy dowód lematu.

Powyższy system można łatwo rozszerzyć do systemu dla formuł opartych o pozostałe spójniki logiczne. Wystarczy w tym celu dodać aksjomaty wyrażaj±ce równoważno¶ci definiuj±ce te spójniki.

(B1)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\wedge \psi\arr\neg(\varphi\arr\neg\psi)}
(B2)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\arr\varphi\wedge \psi}
(B3)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\vee\psi\arr(\neg\varphi\arr\psi)}
(B4)  Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\neg\varphi\arr\psi)\arr\varphi\vee\psi}

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

Twierdzenie o poprawno¶ci dla ${⊢}_{H^{+}}$

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

Dowód

Wystarczy sprawdzić, że aksjomaty (B1)--(B4) s± tautologiami. Konkluzja wynika z Twierdzenia Uzupelnic tw-zda-2| o poprawno¶ci dla ${⊢}_H$.

Lemat

Dla dowolnej formuły $\phi$ istnieje formuła $\tilde{\phi }$ zbudowana przy użyciu jedynie Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} oraz $\mathrm{\perp }$, taka że Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\varphi\arr\tilde{\varphi}} {.1cm} oraz {.1cm} Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\tilde{\varphi}\arr\varphi} .

Dowód

W danej formule $\phi$, zast±pmy każd± podformułę postaci $\psi \wedge \vartheta$ formuł± Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\psi\arr\neg\vartheta)} oraz każd± podformułę postaci $\psi \vee \vartheta$ formuł± Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg\psi\arr\vartheta} . Aksjomaty (B1)--(B4) mówi±, że zast±pione formuły s± równoważne. Tak więc łatwo dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\varphi\arr\tilde{\varphi}} oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \vdash_{H^+}\tilde{\varphi}\arr\varphi} . Szczegóły dowodu pozostawimy Czytelnikowi.

System naturalnej dedukcji

System naturalnej dedukcji (wprowadzony przez S. Ja¶kowskiego i G. Gentzena) operuje wyrażeniami zwanymi sekwentami. S± to wyrażenia postaci $\mathrm{\Delta }⊢\phi$, gdzie $\mathrm{\Delta }$ jest pewnym skończonym zbiorem formuł, a $\phi$ jest formuł±. W odróżnieniu od systemu hilbertowskiego, w naturalnej dedukcji istotne s± reguły dowodzenia, a aksjomat jest bardzo prosty. Charakterystyczn± cech± naturalnej dedukcji jest to, że reguły dowodzenia (za wyj±tkiem reguły (PS) "przez sprzeczno¶ć") s± podzielone na grupy, po jednej dla każdego spójnika. W ramach jednej takiej grupy mamy dwa rodzaje reguł. Reguły wprowadzania mówi± o tym w jakiej sytuacji można wprowadzić dany spójnik na prawo od znaku $⊢$ (tj. wywnioskować formułę danego kształtu). Reguły eliminacji mówi± o tym w jakiej sytuacji można ten spójnik wyeliminować, tzn. jak można użyć formuły zbudowanej z jego pomoc± do wyprowadzenia innej formuły. Regułę dowodzenia "przez sprzeczno¶ć" można traktować jako "siln±" regułę eliminacji $\mathrm{\perp }$. Pamiętajmy, że $\mathrm{\neg }\phi$ oznacza formułę Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\bot} .

Poniżej będziemy stosować następuj±c± konwencję: Napis $\mathrm{\Delta },{\phi }_1,\dots ,{\phi }_n$ oznacza zbiór $\mathrm{\Delta }\cup \{{\phi }_1,\dots ,{\phi }_n\}$, przy czym nie zakładamy tu, że ${\phi }_i\in ̸\mathrm{\Delta }$.

Aksjomat

(A0)  $\mathrm{\Delta },\phi ⊢\phi$

Reguły dowodzenia

Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle (\arr } -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta,\varphi\vdash\psi}{\Delta\vdash\varphi\arr\psi} \hspace{1cm} (\arr } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm} \frac{\Delta\vdash\varphi\arr\psi\odstep \Delta\vdash\varphi}{\Delta\vdash\psi}} $(\wedge$ -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\odstep \Delta\vdash\psi}{\Delta\vdash\varphi\wedge\psi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\varphi} \hspace{1cm} (\wedge } -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle ) \hspace{.2cm}\frac{\Delta\vdash\varphi\wedge\psi}{\Delta\vdash\psi}} $(\vee$ -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi}{\Delta\vdash\varphi\vee\psi} \hspace{1cm} (\vee } -intro Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\psi}{\Delta\vdash\varphi\vee\psi} } $(\vee$ -elim Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta\vdash\varphi\vee\psi\odstep \Delta,\varphi\vdash\vartheta\odstep \Delta,\psi\vdash\vartheta}{\Delta\vdash\vartheta}} $($ PS Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle )\hspace{.2cm} \frac{\Delta,\neg\varphi\vdash\bot}{\Delta\vdash\varphi}}

Zauważmy, że szczególnym przypadkiem reguły (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -intro) jest następuj±ca reguła, można j± traktować jak regułę wprowadzenia negacji.

$\frac{\mathrm{\Delta },\phi ⊢\mathrm{\perp }}{\mathrm{\Delta }⊢\mathrm{\neg }\phi }$

Zauważmy też, że szczególnym przypadkiem reguły (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -elim) jest następuj±ca reguła, można j± traktować jak regułę eliminacji negacji.

$\frac{\mathrm{\Delta }⊢\mathrm{\neg }\phi \mathrm{\Delta }⊢\phi }{\mathrm{\Delta }⊢\mathrm{\perp }}$

O ile dowody w systemi hilbertowskim s± tradycyjnie definiowane jako ci±gi, a więc struktury liniowe, to w systemie naturalnej dedukcji dowody s± drzewami. Pozwala to znacznie lepiej wizualizować zależno¶ci pomiędzy przesłankami i konkluzj± stosowanych reguł. Dowodem sekwentu $\mathrm{\Delta }⊢\phi$ w systemie naturalnej dedukcji nazwiemy drzewo etykietowane sekwentami tak, że korzeń ma etykietę $\mathrm{\Delta }⊢\phi$, li¶cie s± etykietowane wyst±pieniami aksjomatu oraz każdy wewnętrzny wierzchołek jest etykietowany sekwentem otrzymanym z etykiet potomków tego wierzchołka przy zastosowaniu jednej z reguł. Piszemy $\mathrm{\Delta }{⊢}_N\phi$, gdy sekwent $\mathrm{\Delta }⊢\phi$ ma dowód w systemie naturalnej dedukcji. Gdy $\mathrm{\Delta }=\mathrm{\varnothing }$, to mówimy też, że $\phi$ jest twierdzeniem systemu naturalnej dedukcji i zapisujemy to przez ${⊢}_N\phi$. Je¶li $\mathrm{\Delta }$ jest zbiorem nieskończonym, to $\mathrm{\Delta }{⊢}_N\phi$ oznacza, że istnieje dowód sekwentu ${\mathrm{\Delta }}_0⊢\phi$, dla pewnego skończonego ${\mathrm{\Delta }}_0\subseteq \mathrm{\Delta }$.

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

Przykład

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

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{p\vdash p}{\vdash p\arr p} }

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

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{\arintro{p,q\vdash p}{p\vdash q\arr p}}{\vdash p\arr (q\arr p)} }

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

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{\ps{\arelim{\neg\neg p,\neg p\vdash\neg\neg p} {\neg\neg p,\neg p\vdash\neg p}{\neg\neg p,\neg p\vdash p}} {\neg\neg p\vdash p}}{\vdash\neg\neg p\arr p} }

Twierdzenie

Dla dowolnego sekwentu $\mathrm{\Delta }⊢\phi$ mamy następuj±c± równoważno¶ć:

Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \Delta\vdash_{N}\varphi\hspace{.2cm} } , gdy Parser nie mógł rozpoznać (błąd składni): {\displaystyle \displaystyle \hspace{.2cm} \Delta\vdash_{H^+}\varphi.}

Aby pokazać, że każdy dowód w ${⊢}_N$ daje się przerobić na dowód w ${⊢}_{H^{+}}$ wystarczy sprawdzić, że każda z reguł systemu naturalnej dedukcji jest dopuszczalna w $H^{+}$. Tzn. wystarczy sprawdzić, że je¶li mamy dowody przesłanek w ${⊢}_{H^{+}}$, to możemy udowodnić konkluzję. Zauważmy, że wyprowadzalno¶ć reguły(Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -intro) jest konsekwencj± twierdzenia o dedukcji, natomiast reguła (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr} -elim) jest reguł± (MP). Przykładowo pokażemy wyprowadzenie ($\vee$-elim) oraz (PS) w $H^{+}$, pozostawiaj±c Czytelnikowi wyprowadzenie pozostałych reguł.

Załóżmy, że mamy w $H^{+}$ dowody następuj±cych sekwentów: $\mathrm{\Delta }⊢\phi \vee \psi$, {.1cm} $\mathrm{\Delta },\phi ⊢\vartheta$ {.1cm}oraz {.1cm} $\mathrm{\Delta },\psi ⊢\vartheta$. Wówczas, stosuj±c aksjomat (B2) i regułę (MP) mamy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_{H^+}\neg\varphi\arr\psi} . Zatem $\mathrm{\Delta },\mathrm{\neg }\phi {⊢}_{H^{+}}\psi$ i ponieważ Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_{H^+}\psi\arr\vartheta} to również Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta,\neg\varphi\vdash_{H^+}\psi\arr\vartheta} . St±d $\mathrm{\Delta },\mathrm{\neg }\phi {⊢}_{H^{+}}\vartheta$. Stosuj±c twierdzenie o dedukcji dostajemy Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta\vdash_{H^+}\neg\varphi\arr\vartheta} . Skoro mamy również Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \delta\vdash_{H^+}\varphi\arr\vartheta} , to na mocy Lematu Uzupelnic le-zda-1|(3) otrzymujemy $\mathrm{\Delta }{⊢}_{H^{+}}\vartheta$.

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

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

Parser nie mógł rozpoznać (nieznana funkcja „\arelim”): {\displaystyle \displaystyle \arelim{\arelim{\se\varphi\arr(\psi\arr\vartheta)}{\se\varphi} {\se\psi\arr\vartheta}} {\arelim{\se\varphi\arr\psi}{\se\varphi}{\se\psi}}{\se\vartheta} }

Stosuj±c trzy razy (Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \arr } -intro ) do sekwentu Parser nie mógł rozpoznać (nieznana funkcja „\se”): {\displaystyle \displaystyle \se\vartheta} dostajemy wyprowadzenie aksjomatu (A2).

Następnie pokażemy dowód (B1) w ND. Zaczniemy od wyprowadzenia Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\varphi} , gdzie Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\neg(\varphi\arr\neg\psi), \neg\varphi\}} :

Parser nie mógł rozpoznać (nieznana funkcja „\ps”): {\displaystyle \displaystyle \ps{\arelim{\arintro{\arintro{\arelim{\Delta,\varphi,\psi\vdash\neg\varphi} {\Delta,\varphi,\psi\vdash\varphi}{\Delta,\varphi,\psi\vdash\bot}} {\Delta,\varphi\vdash\neg\psi}}{\se\varphi\arr\neg\psi}} {\se\neg(\varphi\arr\neg\psi)}{\se\bot}} {\neg(\varphi\arr\neg\psi)\vdash\varphi} }

Następnie wyprowadzimy sekwent Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\psi} . Niech Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \Delta=\{\neg(\varphi\arr\neg\psi), \neg\psi\}}

Parser nie mógł rozpoznać (nieznana funkcja „\ps”): {\displaystyle \displaystyle \ps{\arelim{\arintro{\Delta,\varphi\vdash\neg\psi}{\se\varphi\arr\neg\psi}} {\se\neg(\varphi\arr\neg\psi)}{\se\bot}}{\neg(\varphi\arr\neg\psi)\vdash\psi} }

Maj±c wyprowadzone sekwenty Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\varphi} oraz Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \neg(\varphi\arr\neg\psi)\vdash\psi} możemy zakończyć dowód (B1).

Parser nie mógł rozpoznać (nieznana funkcja „\arintro”): {\displaystyle \displaystyle \arintro{\wedgeintro{\neg(\varphi\arr\neg\psi)\vdash\varphi} {\neg(\varphi\arr\neg\psi)\vdash\psi} {\neg(\varphi\arr\neg\psi)\vdash\varphi\wedge\psi}} {\vdash\neg(\varphi\arr\neg\psi)\arr(\varphi\wedge\psi)} }