Aksjomatyka Klasycznego Rachunku Zdań

Podobnie jak nie wszystkie zdania języka naturalnego mają sens, nie wszystkie formuły opisują prawdziwe schematy wnioskowania lub zdania, które bylibyśmy skłonni uznać za prawdziwe. W tym rozdziale skupimy się na tym, które spośród wszystkich formuł zdaniowych wyróżnić jako prawdziwe.

Aksjomaty

Wielu matematyków zgadza się dzisiaj co do tego, że zdania pasujące do poniższych schematów powinny być uznane za prawdziwe:

Definicja 3.1 Aksjomaty klasycznego rachunku zdań

\( (\phi \Rightarrow (\psi \Rightarrow \phi)) \) (formuła ta jest nazywana aksjomatem K),
\( (\phi \Rightarrow (\nu \Rightarrow \psi)) \Rightarrow ((\phi \Rightarrow \nu) \Rightarrow (\phi \Rightarrow \psi) ) \) (formuła ta jest nazywana aksjomatem S),
\( (\neg \phi \Rightarrow \psi) \Rightarrow ((\neg \phi \Rightarrow \neg \psi) \Rightarrow \phi) \) (tzw. schemat dowodu niewprost)

Zdania pasujące do powyższych schematów to wszystkie zdania, które można otrzymać, podstawiając w miejsce \( \phi, \nu, \psi \) dowolne formuły.

Reguła dowodzenia

Przyglądnijmy się teraz jak posługujemy się implikacją we wnioskowaniu. W przykładzie z początku wykładu implikacja odpowiadała konstrukcji językowej:
jeśli \( {\phi} \) to \( {\psi} \).
W takim przypadku, jeśli akceptujemy powyższą implikacjię jako zdanie prawdziwe oraz jeśli zdanie \( {\phi} \) jako prawdziwe, to powinniśmy także zaakceptować \( {\psi} \). Przedstawiony sposób wnioskowania nosi nazwę reguły Modus Ponens (nazywana też regułą odrywania, często będziemy używać skrótu MP) i jest skrótowo notowany w poniższy sposób
\( \frac{\phi \Rightarrow \psi, \phi} {\psi}. \)
Reguła modus ponens posłuży nam do uzupełniania zbioru aksjomatów o ich konsekwencje logiczne, które również uznamy za prawdziwe. Aby precyzyjnie zdefiniować zbiór wszystkich konsekwencji logicznych aksjomatów, definiujemy poniżej pojęcie dowodu.

Definicja 3.2

Ciąg formuł \( \phi_0, \dots ,\phi_n \) jest dowodem formuły \( {\psi} \) wtedy i tylko wtedy, gdy:

\( \phi_n \) jest formułą \( {\psi} \),
dla każdego \( i\leq n \) formuła \( \phi_i \) jest aksjomatem lub istnieją \( j,k < i \) takie, że formuła \( \phi_i \) jest wynikiem zastosowania reguły modus ponens do formuł \( \phi_j, \phi_k \).

W drugim punkcie powyższej definicji, jeśli formuła \( \phi_i \) nie jest aksjomatem (a więc powstaje przez zastosowanie MP), to formuły \( \phi_j,\phi_k \) muszą pasować do przesłanek reguły MP, a więc \( \phi_j \) musi być postaci \( \phi_k \Rightarrow \phi_i \) lub \( \phi_k \) postaci \( \phi_j \Rightarrow \phi_i \).
Definicja 3.3
Formułę nazywamy twierdzeniem klasycznego rachunku zdań jeśli istnieje jej dowód z aksjomatów klasycznego rachunku zdań 3.1

Przykład

Zastanówmy się na formułą postaci \( \phi \Rightarrow \phi \). Intuicja podpowiada, że taką formułę powinniśmy uznać za prawdziwą. Nie pasuje ona jednak do żadnego ze schematów aksjomatów 3.1. Formuła ta jest jednak twierdzeniem klasycznego rachunku zdań. Poniżej przedstawiamy jej dowód. Aby łatwiej dopasować formuły do schematów aksjomatów, użyliśmy nawiasów kwadratowych dla nawiasów, które pochodzą ze schematów.

\( [\phi \Rightarrow [(q \Rightarrow \phi) \Rightarrow \phi)]\Rightarrow [[\phi \Rightarrow (q \Rightarrow \phi)] \Rightarrow [\phi \Rightarrow\phi]] \) formuła ta jest aksjomatem zgodnym ze schematem S,
\( \phi \Rightarrow [(q \Rightarrow \phi) \Rightarrow \phi] \) aksjomat zgodny ze schematem K,
\( (\phi \Rightarrow (q \Rightarrow \phi)) \Rightarrow (\phi \Rightarrow \phi) \) z modus ponens z formuł 1 i 2,
\( \phi \Rightarrow [q \Rightarrow \phi] \) aksjomat zgodny ze schematem K,
\( (\phi \Rightarrow \phi) \) z modus ponens z formuł 3 i 4.

Podsumowanie

Klasyczny rachunek zdań, czyli zbiór formuł które uznajemy za prawdziwe, zdefiniowaliśmy, wyróżniając pewne formuły jako aksjomaty 3.1 i dorzucając do nich wszystkie formuły, które dają się z nich wywnioskować przy pomocy reguły Modus Ponens. Warto zwrócić uwagę, że pomimo tego, iż w doborze aksjomatów i reguł wnioskowania kierowaliśmy się intuicyjnym pojęciem implikacji i konsekwencji, klasyczny rachunek zdań jest teorią syntaktyczną, zbiorem pewnych napisów o których znaczeniu nie musimy nic mówić.

Uwaga 3.4

Warto przyglądnąć się przyjętym aksjomatom i zastanowić się jakim zdaniom odpowiadają i czy rzeczywiście bylibyśmy skłonni uznać je za prawdziwe. Pomocne może być interpretowanie formuł postaci \( \phi \Rightarrow (\nu \Rightarrow \psi) \) jako „jeśli prawdziwe jest \( {\phi} \) i prawdziwe jest \( \nu \) to prawdziwe jest \( {\psi} \)”. W kolejnych rozdziałach przekonamy się, że taka interpretacja jest uzasadniona.

Informatyka MIMUW