Logika dla informatyków/Paradygmaty dowodzenia
Paradygmaty dowodzenia
Sprawdzenie, czy dana formuła rachunku zdań jest tautologią, polega zwykle na obliczeniu jej wartości dla (Twierdzenie 3.8). W obu przypadkach istnieją jednak metody dowodzenia pozwalające na wyprowadzanie prawdziwych formuł za pomocą ustalonych procedur syntaktycznych.
różnych wartościowań, gdzie 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ą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
, stałej oraz zmiennych zdaniowych. Przypomnijmy, że dla dowolnej formuły , napis jest skrótem zapisu Parser nie mógł rozpoznać (nieznana funkcja „\arr”): {\displaystyle \displaystyle \varphi\arr\bot} . Symbole w poniższym systemie oznaczają dowolne formuły.Aksjomaty
Reguła dowodzenia
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
ma dowód lub jest twierdzeniem systemu hilbertowskiego, co zapiszemy , gdy istnieje dowód zawierający . Powyższą definicję możemy nieco uogólnić. Niech będzie dowolnym zbiorem formuł. Powiemy, że formuła ma dowód ze zbioru hipotez (notacja ), gdy jest twierdzeniem systemu, w którym zbiór aksjomatów został poszerzony o formuły ze zbioru .Przykład 5.1
Niech
będzie zmienną zdaniową. Pokażemy, że formuła 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.Zauważmy, że w powyższym przykładzie możemy wszędzie zastąpić zmienną
przez dowolną formułę dostając dowód formuły .Następujące twierdzenie jest bardzo użyteczne, gdy trzeba uzasadnić, że jakaś formuła jest twierdzeniem.
Twierdzenie 5.2 (o dedukcji)
Dla dowolnego zbioru formuł
oraz dowolnych formuł , jeśli , to .Dowód
Dowód jest indukcyjny ze względu na liczbę kroków w dowodzie formuły 5.1 dostajemy dowód formuły . Możemy oczywiście przyjąć, że formuła ta jest wyprowadzona ze zbioru hipotez . Druga możliwość jest taka, że lub też, że jest aksjomatem. W każdym z tych przypadków mamy . Wówczas stosując regułę odrywania do oraz aksjomatu , dostajemy formułę .
ze zbioru hipotez . Przypuśćmy najpierw, że dowód ten składa się tylko z jednego kroku. Jeśli , to stosując wyprowadzenie z PrzykładuZałożmy teraz, że ostatnim krokiem w wyprowadzeniu formuły
jest zastosowanie reguły (MP) do formuł oraz , dla pewnej formuły . Z założenia indukcyjnego mamy oraz . Stosując regułę odrywania do oraz do aksjomatu (A2): dostajemy formułę . Ponownie stosując regułę odrywania do tej formuły oraz do dostajemy żądaną formułę . To kończy dowód twierdzenia o dedukcji.
Twierdzenie 5.3 (o poprawności)
Jeśli
, to . W szczególności, jeśli , to jest tautologią.Dowód
Dowód jest indukcyjny ze względu na liczbę kroków w wyprowadzeniu formuły
w systemie hilbertowskim ze zbioru hipotez . Jeśli dowód ten składa się tylko z jednego kroku, to albo , albo jest aksjomatem. W obu przypadkach oczywiście zachodzi .Załóżmy teraz, że
jest otrzymana przez zastosowanie reguły odrywania do formuł oraz . Z założenia indukcyjnego mamyNiech
będzie dowolnym wartościowaniem spełniającym wszystkie formuły z . Na mocy (1), wartościowanie spełnia oraz spełnia . Wynika stąd, że spełnia . Tym samym udowodniliśmy, że . To kończy dowód.
Lemat 5.4
Dla dowolnych formuł
zbudowanych przy użyciu oraz , następujące formuły są twierdzeniami systemu hilbertowskiego.- ;
- ;
- ;
Dowód
(1) Niech
. Stosując regułę odrywania do formuł oraz dostajemy . Przez ponowne zastosowanie (MP) do tej formuły oraz do otrzymujemy wyprowadzenie . Tym samym pokazaliśmy, że . Stosując teraz trzy razy twierdzenie o dedukcji dostajemyczyli
(2) Ponieważ
, więc z twierdzenia o dedukcji wynika . Stosując teraz (MP) do tej formuły oraz do aksjomatu (A3) w postaci otrzymujemy . Ponowne zastosowanie twierdzenia o dedukcji daje nam .(3) Niech
. Zaczynamy od zbioru hipotez . Stosując (MP) do formuł oraz dostajemy . Ponowne zastosowanie (MP) do tej formuły oraz do daje nam . Używając teraz twierdzenia o dedukcji do formuły otrzymujemyPonieważ mamy
, to stosując (MP) otrzymujemy . Jeszcze raz używamy (MP) aby z i otrzymać i mamyNa mocy twierdzenia o dedukcji
. Stosując (MP) do formuły oraz do aksjomatu otrzymujemy . Dwukrotne zastosowanie twierdzenia o dedukcji daje nam . 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.
Tak otrzymany system oznaczymy przez
.Twierdzenie 5.5 (o poprawności dla )
Dla dowolnego zbioru formuł
i dla dowolnej formuły 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 .Dowód
Wystarczy sprawdzić, że aksjomaty (B1)-(B4) są tautologiami. Konkluzja wynika z Twierdzenia 5.3 o poprawności dla .

Lemat 5.6
Dla dowolnej formuły
istnieje formuła zbudowana przy użyciu jedynie oraz , taka że oraz .Dowód
W danej formule
, zastąpmy każdą podformułę postaci formułą oraz każdą podformułę postaci formułą . Aksjomaty (B1)-(B4) mówią, że zastąpione formuły są równoważne. Tak więc łatwo dostajemy oraz . 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
, gdzie jest pewnym skończonym zbiorem formuł, a 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 . Pamiętajmy, że oznacza formułę .Poniżej będziemy stosować następującą konwencję: Napis
oznacza zbiór , przy czym nie zakładamy tu, że .Aksjomat
Reguły dowodzenia
Zauważmy, że szczególnym przypadkiem reguły ( -intro) jest
następująca reguła, można ją traktować jak regułę wprowadzenia negacji.
Zauważmy też, że szczególnym przypadkiem reguły (
-elim) jest następująca reguła, można ją traktować jak regułę eliminacji negacji.O ile dowody w systemie 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
w systemie naturalnej dedukcji nazwiemy drzewo etykietowane sekwentami tak, że korzeń ma etykietę , 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 , gdy sekwent ma dowód w systemie naturalnej dedukcji. Gdy , to mówimy też, że jest twierdzeniem systemu naturalnej dedukcji i zapisujemy to przez . Jeśli jest zbiorem nieskończonym, to oznacza, że istnieje dowód sekwentu , dla pewnego skończonego .Poniżej podajemy kilka przykładów dowodów w systemie naturalnej dedukcji.
Przykład 5.7
- Pokażemy .
- Pokażemy .
- Pokażemy .
Twierdzenie 5.8
Dla dowolnego sekwentu
mamy następującą równoważność:Aby pokazać, że każdy dowód w
daje się przerobić na dowód w wystarczy sprawdzić, że każda z reguł systemu naturalnej dedukcji jest dopuszczalna w . Tzn. wystarczy sprawdzić, że jeśli mamy dowody przesłanek w , to możemy udowodnić konkluzję. Zauważmy, że wyprowadzalność reguły( intro) jest konsekwencją twierdzenia o dedukcji, natomiast reguła ( elim) jest regułą (MP). Przykładowo pokażemy wyprowadzenie ( elim) oraz (PS) w , pozostawiając Czytelnikowi wyprowadzenie pozostałych reguł.Załóżmy, że mamy w Lematu 5.4 (3) otrzymujemy .
dowody następujących sekwentów: , {.1cm} {.1cm}oraz {.1cm} . Wówczas, stosując aksjomat (B2) i regułę (MP) mamy . Zatem i ponieważ to również . Stąd . Stosując twierdzenie o dedukcji dostajemy . Skoro mamy również , to na mocyDla wyprowadzenia (PS) załóżmy, że
. Z twierdzenia o dedukcji dostajemy . Tak więc z (A3) i (MP) dostajemy .Dla pokazania implikacji odwrotnej wystarczy pokazać, że wszystkie aksjomaty systemu Przykładzie 5.7. Przykładowo pokażemy wyprowadzenia (A2) i (B1). Zaczniemy od wyprowadzenia (A2). Niech . Mamy następujący dowód:
są twierdzeniami systemu naturalnej dedukcji. Wyprowadzenia (A1) i (A3) w ND zostały podane w
Stosując trzy razy ( -intro ) do sekwentu dostajemy wyprowadzenie aksjomatu (A2).
Następnie pokażemy dowód (B1) w ND. Zaczniemy od wyprowadzenia
, gdzie :
Następnie wyprowadzimy sekwent . Niech
Mając wyprowadzone sekwenty
oraz , możemy zakończyć dowód (B1).
Rachunek sekwentów
Dla przedstawienia rachunku sekwentów rozszerzymy nieco pojęcie sekwentu. Przez sekwent będziemy teraz rozumieć napis
, gdzie oraz są skończonymi zbiorami formuł. Intuicyjnie, wyprowadzalność sekwentu w rachunku sekwentów będzie oznaczać, że alternatywa formuł z wynika z hipotez .Podobnie jak w poprzedniej części, rozważamy formuły, zbudowane w oparciu o spójniki
oraz stałą zdaniową . Negację traktujemy jako spójnik zdefiniowany przez i .Charakterystyczną cechą rachunku sekwentów jest specyficzna postać reguł. Reguły w tym systemie naturalnie dzielą się na dwie grupy: jedna grupa reguł opisuje sytuacje kiedy możemy wprowadzić dany spójnik na lewo od znaku
, a druga grupa jest odpowiedzialna za wprowadzanie spójnika na prawo od . Dla każdego spójnika mamy odpowiadającą parę reguł. Aksjomat (A ) można traktować jako regułę (bez przesłanek) wprowadzenia z lewej strony znaku .Przypomnijmy, że napis
oznacza zbiór .Aksjomaty
Reguły dowodzenia
Dowodem sekwentu , tak jak poprzednio,
nazywamy drzewo etykietowane sekwentami tak, że korzeń jest
etykietowany przez , liście są etykietowane
aksjomatami oraz wierzchołki wewnętrzne
są etykietowane sekwentami otrzymanymi poprawnie przez zastosowanie
reguł dowodzenia. Jeśli istnieje dowód sekwentu
w rachunku sekwentów to zapisujemy to tak:
. (Litera G pochodzi od nazwiska twórcy tego
systemu, G. Gentzena.) Piszemy też , gdy
jest nieskończony, ale
dla pewnego skończonego .
Zauważmy, że jeśli mamy sekwent
to stosując aksjomat ( ), a następnie ( -lewa) dostajemy sekwent . Zatem natępująca reguła jest dopuszczalna w systemie (tj. jeśli dodamy ją do systemu, to zbiór wyprowadzalnych sekwentów nie ulegnie zmianie):Ponadto zauważmy, że jeśli mamy dowód sekwentu
Ćwiczenie 12).
W szczególności, jeśli mamy udowodniony sekwent , to możemy też
udowodnić sekwent .
Stosując do niego regułę ( -prawa) otrzymujemy sekwent
. Tym samym pokazaliśmy, że
następująca reguła jest dopuszczalna w systemie :
Twierdzenie 5.9
Dla każdych
i mamy następującą równoważnośćPowyższe twierdzenie pozostawimy bez dowodu. Łatwo jest "przetłumaczyć" każde wyprowadzenie w systemie
na dowód w stylu Hilberta. Dla dowodu implikacji odwrotnej rozszerza się system przez dodanie nowej reguły zwanej cięciem.Niech Twierdzenia 5.9 polega na udowodnieniu następującego twierdzenia o eliminacji cięcia. Twierdzenie to podajemy bez dowodu.
oznacza system gentzenowski z cięciem. Bez trudu można pokazać, że reguła odrywania jest dopuszczalna w . Zatem, korzystając z twierdzenia o pełności dla systemu hilbertowskiego, łatwo pokazujemy, że każda tautologia jest twierdzeniem systemu . Główna trudność w dowodzieTwierdzenie 5.10 (o eliminacji cięcia)
Jeśli
, to .Główna zaleta dowodów w rachunku sekwentów (bez cięcia) wynika z następującej własności podformuł: wszystkie formuły występujące w przesłance dowolnej reguły są podformułami formuł występujących w konkluzji. Zatem np. w dowodzie sekwentu
mamy do czynienia tylko z podformułami formuły . Dla danej formuły , łatwiej więc znaleźć dowód w sensie Gentzena niż np. dowód w sensie Hilberta. Dlatego systemy zbliżone do rachunku sekwentów znajdują zastosowanie w automatycznym dowodzeniu twierdzeń. Pokażemy to na przykładzie.Przykład 5.11
- Poszukamy dowodu sekwentu w
. Ponieważ najbardziej zewnętrznym spójnikiem w rozważanej formule jest , to ostatnią regułą w poszukiwanym dowodzie musiała być reguła ( -prawa). Zatem wystarczy znaleźć dowód sekwentu . Najbardziej zewnętrznym spójnikiem formuły po lewej stronie jest , a zatem na mocy reguły ( -lewa) wystarczy udowodnić sekwent . Podobnie, na mocy reguły ( -prawa), wystarczy udowodnić sekwent , a on przecież jest aksjomatem.
- Jeśli zastosujemy powyższą procedurę do formuły, która
nie jest tautologią, to dostaniemy wskazówkę na to gdzie należy szukać wartościowania falsyfikującego tę formułę. (Wartościowanie falsyfikujące sekwent
to takie, które spełnia wszystkie formuły z oraz falsyfikuje wszystkie formuły z .) Dla zilustrowania tej tezy weźmy bardzo prosty sekwent . Postępując podobnie jak poprzednio, dochodzimy do sekwentu , który nie jest aksjomatem, i którego nie możemy już dalej rozłożyć. Jako wartościowanie falsyfikujące wystarczy wziąć wartościowanie spełniające i falsyfikujące .Z własności podformuł 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 wyprowadzenie nie wymaga reguł związanych z tym spójnikiem.