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.