Logika dla informatyków/Rachunek zdań

Wnioskowanie o prawdziwości rozmaitych stwierdzeń jest powszednim zajęciem matematyków i nie tylko matematyków. Dlatego filozofowie i matematycy od dawna zajmowali się systematyzacją metod wnioskowania i kryteriów ich poprawności. Oczywiście ostatecznym kryterium poprawności rozumowania pozostaje zawsze zdrowy rozsądek i przekonanie o słuszności wywodu. Logika, która narodziła się jako nauka o rozumowaniu, jest jednak ważnym i potrzebnym narzędziem, które to przekonanie ułatwia.

Szczególną rolę wśród rozmaitych działów logiki zajmuje logika matematyczna, poświęcona opisowi i analizie języka matematyki oraz poprawności wnioskowań matematycznych. Jest to dyscyplina w pewnym sensie paradoksalna: będąc sama częścią matematyki, traktuje matematykę jako swój przedmiot zainteresowania. Dla uniknięcia "błędnego koła" musimy więc tutaj zauważyć, że logika formalna nie opisuje rzeczywistych wywodów matematyka, ale ich uproszczone modele, które bez zastrzeżeń można uważać za zwykłe obiekty matematyczne. Mimo tego ograniczenia, logika matematyczna dostarcza niezwykle ważnych wniosków o charakterze filozoficznym i metamatematycznym.

Logika formalna była kiedyś ezoteryczną nauką z pogranicza filozofii i matematyki, potem stała się pełnoprawnym działem czystej matematyki.Jeszcze później, wraz z narodzinami informatyki, zaczęła być coraz bardziej postrzegana jako dziedzina matematyki stosowanej, a zwłaszcza podstaw informatyki.

Logika matematyczna stosowana jest dziś szeroko w informatyce. Semantyka i weryfikacja programów, teoria złożoności i teoria automatów, programowanie funkcyjne i programowanie w logice --- to tylko niektóre z działów informatyki, w których metody logiki formalnej stały się standardowym narzędziem zarówno badacza, jak i praktyka.

Rachunek zdań

Jak powiedzieliśmy wyżej, logika matematyczna zajmuje się badaniem rozmaitych systemów formalnych, modelujących rzeczywiste sposoby wnioskowania matematycznego. Do najprostszych takich systemów należą różne warianty logiki zdaniowej zwanej też rachunkiem zdań. Język rachunku zdań jest bardzo prosty. Nie ma w nim wyrażeń stwierdzających jakiś stan rzeczy, zajście jakichś faktów, czy też wyrażeń orzekających o własnościach obiektów. Przedmiotem naszego zainteresowania są tu tylko możliwe zależności pomiędzy stwierdzeniami (zdaniami orzekającymi) oraz to w jaki sposób prawdziwość zdań złożonych zależy od prawdziwości ich składowych. Sens samych składowych pozostaje tu całkowicie dowolny i nieistotny. Dlatego w rachunku zdań odpowiadają im po prostu zmienne zdaniowe. Zdania złożone budujemy ze zmiennych za pomocąspójników logicznych, takich jak alternatywa  $\vee$,koniunkcja  $\wedge$, negacja $\mathrm{\neg }$, czy implikacja $\to$. Wygodne są też stałe logiczne  $\mathrm{\perp }$ (fałsz) i $\mathrm{\top }$ (prawda), które można uważać za zeroargumentowe spójniki logiczne.Dlatego nasza pierwsza definicja jest taka:

Definicja 1.1

Ustalamy pewien przeliczalnie nieskończony zbiór $ZZ$ symboli, które będziemy nazywać zmiennymi zdaniowymi i zwykle oznaczać literami $p$, $q$, itp. Pojęcie formuły zdaniowej definiujemy przez indukcję:

• Zmienne zdaniowe oraz $\mathrm{\perp }$ i $\mathrm{\top }$ są formułami zdaniowymi;
• Jeśli napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą zdaniową, to także napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} jest formułą zdaniową;
• Jeśli napisy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$ są formułami zdaniowymi, to napisy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\to\psi)} , Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\vee\psi)} i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\wedge\psi)} też są formułami zdaniowymi.

Inaczej mówiąc, formuły zdaniowe to elementy najmniejszego zbioru napisów Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\F_{{\sc Z}}} , zawierającego Parser nie mógł rozpoznać (nieznana funkcja „\small”): {\displaystyle \small ZZ\cup\{\bot,\top\}} i takiego, że dla dowolnych Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} ,$\psi$ $\in$ Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\F_{{\sc Z}}} także Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi,(\var\varphi\to\psi),(\var\varphi\vee\psi), (\var\varphi\wedge\psi)} należą do Parser nie mógł rozpoznać (błąd składni): {\displaystyle \\F_{{\sc Z}}} .

Konwencje notacyjne: Dla pełnej jednoznaczności składni nasze formuły są w pełni nawiasowane. W praktyce wiele nawiasów pomijamy, stosując przy tym następujące priorytety:

1. Negacja;

1. Koniunkcja i alternatywa;

1. Implikacja.

Zatem na przykład wyrażenie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi\vee\psi\to\vartheta} oznacza Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle ((\neg\var\varphi\vee\psi)\to\vartheta)} , ale napis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\vee\psi\wedge \vartheta} jest niepoprawny.

Znaczenie formuł

W logice klasycznej interpretacja formuły jest wartość logiczna tj. "prawda" (1) lub "fałsz" (0). Aby określić wartość formuły zdaniowej, trzeba jednak najpierw ustalić wartości zmiennych.

Definicja 1.2

Przez wartościowanie zdaniowe rozumiemy dowolną funkcję $\varrho$, która zmiennym zdaniowym przypisuje wartości logiczne 0 lub 1. Wartość formuły zdaniowej Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} przy wartościowaniu $\varrho$ oznaczamy przez Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz\var[[\varphi]]\varrho} i określamy przez indukcję:

• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz[[\bot]]\varrho=0} oraz Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz[[\top]]\varrho=1} ;
• $[[p]]\varrho =\varrho (p)$, gdy $p$ jest symbolem zdaniowym;
• Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz[[{\neg\var\varphi}]]\varrho=1-\wfz{[[\var\varphi]]}\varrho} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\vee\psi]]\varrho=\max\{\wf[[\var\varphi]]\varrho,\[[\psi]] \varrho\}} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\wedge\psi]]\varrho=\min\{\wf[[\var\varphi]]\varrho,\[[\psi]] \varrho\}} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\to\psi]]\varrho =0} , gdy Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz\var[[\varphi]]\varrho=1} i Parser nie mógł rozpoznać (nieznana funkcja „\wfz”): {\displaystyle \wfz[[\psi]]\varrho=0} ;
• Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\to\psi]]\varrho =1} , w przeciwnym wypadku

Łatwo zauważyć, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\to\psi]]\varrho = \max\{\wfz[[\psi]]\varrho,1-\wfz\var[[\varphi]]\varrho\}} , czyli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\to\psi]]\varrho=[[\neg\var\varphi\vee\psi]]\varrho} dla dowolnego $\varrho$. A zatem zamiast formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\to\psi} moglibyśmy z równym powodzeniem używać wyrażenia Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi\vee\psi} , lub też odwrotnie: zamiast alternatywy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\vee\psi} pisać Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi\to\psi} . Nasz wybór spójników nie jest więc "najoszczędniejszy", w istocie w logice klasycznej wystarczy używać np. implikacji i fałszu (ćwiczenie 6). Czasem i my będziemy korzystać z tego wygodnego uproszczenia, przyjmując, że "oficjalnymi" spójnikami są tylko implikacja i fałsz, a pozostałe to skróty notacyjne, tj. że napisy

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi}	oznaczają odpowiednio	Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\to\bot} ;
$\mathrm{\top }$		$\mathrm{\neg }\mathrm{\perp }$;
Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\vee\psi}		Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi\to\psi} ;
Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi\wedge\psi}		Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg(\var\varphi\to\neg\psi)} .

Będziemy też czasem pisać Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi \leftrightarrow\psi} zamiast Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle (\var\varphi\to\psi)\wedge(\psi\to\var\varphi)} . Zauważmy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\leftrightarrow\psi]]\varrho=1} wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi\to\psi]]\varrho=[[\psi\to\var\varphi]]\varrho} .

Często stosowanym skrótem jest notacja Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \bigvee_{i\in I}\var\varphi_i} , oznaczająca alternatywę wszystkich formuł Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi_i} , gdzie $i$ przebiega skończony zbiór $I.$ Analogicznie stosuje się zapis Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \bigwedge_{i\in I}\var\varphi_i} .

Notacja i terminologia: Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle [[\var\varphi]]\varrho=1} , to piszemy też Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \varrho\models\var\varphi} lub Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi[\varrho]} i mówimy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełniona przez wartościowanie $\varrho$. Jeśli $\mathrm{\Gamma }$ jest zbiorem formuł zdaniowych oraz $\varrho \models \gamma$ dla wszystkich $\gamma \in \mathrm{\Gamma }$, to piszemy $\varrho \models \mathrm{\Gamma }$. Wreszcie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\models\var\varphi} oznacza, że każde wartościowanie spełniające wszystkie formuły z $\mathrm{\Gamma }$ spełnia także formułę Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Mówimy wtedy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest semantyczną konsekwencją zbioru $\mathrm{\Gamma }$. Jeśli $\mathrm{\Gamma }=\mathrm{\varnothing }$, to zamiast Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\models\var\varphi} piszemy po prostu Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi} . Oznacza to, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełniona przez każde wartościowanie. Na koniec powiedzmy jeszcze, że formułami równoważnymi nazywamy takie formuły Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} i $\psi$, których wartości przy każdym wartościowaniu są takie same (tj. takie, że równoważność Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi \leftrightarrow\psi} jest tautologią --- patrz niżej).

Definicja 1.3

Formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest spełnialna, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \varrho\models\var\varphi} zachodzi dla pewnego wartościowania $\rho$. Jeśli zaś Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \models\var\varphi} , to mówimy, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jesttautologią (klasycznego) rachunku zdań. Oczywiście Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \neg\var\varphi} jest spełnialna wtedy i tylko wtedy, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} nie jest tautologią.

Tautologie rachunku zdań

Niech $S$ będzie funkcją przypisujacą symbolom zdaniowym pewne formuły. Jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest formułą zdaniową, to przez Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle S(\var\varphi)} oznaczymy formułę otrzymaną z Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} przez jednoczesną zamianę każdego wystąpienia zmiennej zdaniowej $p$ na formułę $S(p)$. Mówimy, że formuła Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle S(\var\varphi)} jest instancją schematu zdaniowego Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} . Używamy oznaczenia $S(\mathrm{\Gamma })=\{S(\psi )|\psi \in \mathrm{\Gamma }\}$.

Fakt 1.4

Jeżeli $\mathrm{\Gamma }$ jest zbiorem formuł rachunku zdań i Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \Gamma\models\var\varphi} , to także Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle S(\Gamma)\models S(\var\varphi)} . W szczególności, jeśli Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest tautologią to Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle S(\var\varphi)} jest też tautologią.

Dowód

Ćwiczenie.

Przykład 1.5

Następujące formuły (i wszystkie ich instancje) są tautologiami rachunku zdań:

1. $\mathrm{\perp }\to p$;
2. $p\to (q\to p)$;
3. $(p\to (q\to r))\to ((p\to q)\to (p\to r))$;
4. $((p\to q)\to p)\to p$;
5. $p\vee \mathrm{\neg }p$;
6. $p\to \mathrm{\neg }\mathrm{\neg }p$ oraz $\mathrm{\neg }\mathrm{\neg }p\to p$;
7. $(p\to q)\to (\mathrm{\neg }q\to \mathrm{\neg }p)$ oraz $(\mathrm{\neg }q\to \mathrm{\neg }p)\to (p\to q)$;
8. $p\to (p\vee q)$, $q\to (p\vee q)$ oraz $(p\to r)\to ((q\to r)\to (p\vee q\to r))$;
9. $(p\wedge q)\to p$, $(p\wedge q)\to q$ oraz $(r\to p)\to ((r\to q)\to (r\to (p\wedge q)))$;
10. $((p\wedge q)\to r)\leftrightarrow (p\to (q\to r))$;
11. $\mathrm{\neg }(p\vee q)\leftrightarrow (\mathrm{\neg }p\wedge \mathrm{\neg }q)$;
12. $\mathrm{\neg }(p\wedge q)\leftrightarrow (\mathrm{\neg }p\vee \mathrm{\neg }q)$;
13. $(p\to q)\leftrightarrow (\mathrm{\neg }p\vee q)$;
14. $((p\leftrightarrow q)\leftrightarrow r)\leftrightarrow (p\leftrightarrow (q\leftrightarrow r))$;
15. $p\vee \mathrm{\perp }\leftrightarrow p$ oraz $p\wedge \mathrm{\top }\leftrightarrow p$.

Dowód

Łatwy.

Niektóre z powyższych formuł wskazują na analogię pomiędzy implikacją i uporządkowaniem (np. zawieraniem zbiorów). Implikację $p\to q$ można odczytać tak: "warunek $p$ jest silniejszy (mniejszy lub równy) od $q$". Formułę (1) czytamy wtedy: "fałsz jest najsilniejszym warunkiem (najmniejszym elementem)". Formuły (8) stwierdzają, że alternatywa $p\vee q$ jest najsilniejszym warunkiem, który wynika zarówno z $p$ jak i z $q$ (czyli jest kresem górnym pary $\{p,q\}$, jak suma zbiorów). Formuły (9) wyrażają dualną własność koniunkcji: to jest kres dolny, czyli najsłabszy warunek implikujący oba argumenty.Prawa de Morgana (11,12) wskazują też na analogie koniunkcja -- iloczyn, alternatywa -- suma, negacja -- dopełnienie. Ta ostatnia widoczna jest też w prawach wyłączonego środka (5), podwójnej negacji (6) i kontrapozycji (7).

O ile (9) wskazuje na analogię pomiędzy koniunkcją i iloczynem mnogościowym, o tyle warto zauważyć, że koniunkcja ma też własności podobne do iloczynu kartezjańskiego. Jeśli zbiór funkcjiz $A$ do $B$ oznaczymy przez $[A\to B]$, to mamy (bardzo naturalną) równoliczność $[A\times B\to C]\sim [A\to [B\to C]]$. Podobieństwo tego związku do formuły (10) nie jest wcale przypadkowe. Wrócimy do tego w Rozdziale 11.

Formuła (12) wyraża implikację z pomocą negacji i alternatywy i jest często bardzo przydatna, gdy np. chcemy przekształcić jakąś formułę do prostszej postaci.

Formuła (2) mówi, że dodatkowe założenie można zawsze zignorować. Formuła (3) (prawo Frege) wyraża dystrybutywność implikacji względem siebie samej i może być odczytywana tak: jeśli $r$ wynika z $q$ w kontekście $p$, to ten kontekst może być włączony do założenia i konkluzji. Formuła (4) (prawo Peirce'a) wyraża przy pomocy samej implikacji zasadniczą własność logiki klasycznej: możliwość rozumowania przez zaprzeczenie. Sens prawa Peirce'a widać najlepiej, gdy $q$ jest fałszem, otrzymujemy wtedy prawo Claviusa: $(\mathrm{\neg }p\to p)\to p$.

Warto zauważyć, że formuły w parach (6) i (7) nie są wcale tak symetryczne jak się wydaje na pierwszy rzut oka. Na przykład, pierwsza z formuł (6) to w istocie $p\to ((p\to \mathrm{\perp })\to \mathrm{\perp })$.Wiedząc, że $p$ i $p\to \mathrm{\perp }$, natychmiast zgadzamy się na $\mathrm{\perp }$. Intuicyjne uzasadnienie drugiej formuły jest zaś w istocie związane z prawem  (5).

Własnością, która często uchodzi naszej uwadze, jest łączność równoważności (13). W zwiazku z tym, wyrażenie Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi \leftrightarrow \psi \leftrightarrow \vartheta} można z czystym sumieniem pisać bez nawiasów. Zwróćmy jednak uwagę na to, że oznacza ono zupełnie co innego niż stwierdzenie, że Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} , $\psi$ i $\vartheta$ są sobie nawzajem równoważne!

Ostatnie na liście są dwie równoważności wyrażające taką myśl: fałsz jest "elementem neutralnym" dla alternatywy, a prawda dla koniunkcji. Dlatego $\mathrm{\perp }$ możemy uważać za "pustą alternatywę" a $\mathrm{\top }$ za "pustą koniunkcję". Powyżej pominięto dobrze znane prawa: łączność i przemienność koniunkcji i alternatywy, ich wzajemną dystrybutywność, przechodniość,zwrotność implikacji itp.

Postać normalna formuł

Definicja 1.6

Każdą zmienną zdaniową i negację zmiennej zdaniowej nazwijmy literałem. Mówimy, że formuła zdaniowa Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest w koniunkcyjnej postaci normalnej, gdy Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi} jest koniunkcją alternatyw literałów, tj.

Parser nie mógł rozpoznać (nieznana funkcja „\var”): {\displaystyle \var\varphi = (p^1_1\vee\cdots\vee p^{k_1}_1)\wedge\cdots\wedge(p^1_r\vee\cdots\vee p^{k_r}_r)} ,              (*)

gdzie $r\ge 0$, $k_i\ge 0$, dla $i=0,\dots r$, a wszystkie $p_j^i$ są literałami. Przy tym pustą koniunkcję ($r=0$) utożsamiamy w myśl Przykładu 1.5 ze stałą $\mathrm{\top }$, a stała $\mathrm{\perp }$ to tyle co koniunkcja z jednym pustym składnikiem.

Fakt 1.7

Dla każdej formuły zdaniowej istnieje równoważna jej formuła w koniunkcyjnej postaci normalnej.

Dowód

{{{3}}}

Przypisy

<references/>