System aksjomatyczny

Co to jest i o co chodzi

W poprzedniej sekcji mówiliśmy o pojęciach interpretacji, modelu, spełniania formuł w modelu, zdaniach logicznie prawdziwych, wynikaniu semantycznym oraz o niezawodnych regułach wnioskowań. Zauważmy, że wszystkie te pojęcia są definiowane w oparciu o pojęcie "znaczenia", które jest pojęciem semantycznym (pamiętamy, że znaczeniem zdań prostych jest któraś z wartości logicznych (prawda czy fałsz) i to znaczenie ustalamy poprzez przypisanie zmiennym wartości, czyli poprzez interpretację). 

Wyobraźmy sobie, że nie mamy pojęcia znaczenia: umawiamy się w tym oraz następnym rozdziale nie mówić o znaczeniu zdań (pojęcia prawda / fałsz są przez następne dwa rozdziały niedostępne). Czy bez pojęcia znaczenia (bez pojęcia prawdy i fałszu) będziemy w stanie uzyskać "odpowiedniki" modelu, spełniania formuł, zdań logicznie prawdziwych oraz czy potrafimy sprawdzić poprawność wnioskowań (czy są oparte o regułę niezawodną)?

Otóż to, co zrobiliśmy drogą semantyczną, spróbujemy zrobić drogą syntaktyczną, czyli bez odwołania do znaczenia, lecz do składni, czyli badając związki syntaktyczne między formułami. Wstępnie: idea jest taka, by określić reguły, który pozwoliłby w sposób pewny wyprowadzać jedne formuły z drugich (wyłącznie na podstawie schematów tych formuł). W oparciu o te reguły dostaniemy wszystkie "odpowiedniki" pojęć semantycznych.

Rozważmy rozumowanie: "Jeśli jest sztorm, a na łajbie nie ma bosmana Jima Beama, to łajba roztrzaska się o skały. Ale nie roztrzaskała się. A sztorm był. Zatem: na łajbie był bosman Jim Beam". Intuicyjnie wnioskowanie jest poprawne (a już potrafimy sprawdzić, że jest oparte o regułę niezawodną). Rozważmy jeszcze jedno wnioskowanie: "Jeśli pada, a majtek Jaś Wędrowniczek nie ma gumiaków, to przemoczy nogi. Ale Jaś nie przemoczył nóg. A padało. Zatem: Jaś miał gumiaki". W tym wnioskowaniu również jest tak, że z przesłanek wynika wniosek. Jeśli przypatrzymy się uważnie obu tym wnioskowaniom, to zauważymy, że mają one ten sam schemat:

(α∧¬β)→γ

¬γ

α

––––––

β

Schemat ten jest oparty o regułę niezawodną, czyli czy jest tak, że ze zbioru przesłanek {(α∧¬β)→γ, ¬γ, α} wynika β. Teraz wynikanie będziemy chcieli zastąpić wyprowadzaniem, czyli regułami, w oparciu o które będziemy mogli powiedzieć, że ze zbioru przesłanek {(α∧¬β)→γ, ¬γ, α} jest wyprowadzalny wniosek β.

System aksjomatyczny

Przypomnijmy sobie geometrię Euklidesa i dowody twierdzeń, które robiliśmy w szkole. Otóż geometria Euklidesa jest systemem aksjomatycznym - wszystkie twierdzenia tego systemu wynikają z aksjomatów - twierdzeń uznanych za pierwotne oraz pewne (czyli nie wymagające dowodu, takie jak "dowolne dwa punkty można połączyć odcinkiem").

W Klasycznym Rachunku Zdań jest podobnie. System aksjomatyczny KRZ składa się z (pełna definicja):

• zbioru formuł nazywanych aksjomatami;

• reguł wnioskowania (pierwotnych), które pozwalają przechodzić od przesłanek do wniosku w sposób uznany za niezawodny.

Istnieje bardzo dużo różnych układów aksjomatów KRZ równoważnych między sobą (zobacz przykłady innych systemów). Przyjmiemy układ aksjomatów Hilberta-Bernaysa.

Aksjomaty KRZ

Formuły KRZ, które możemy wygenerować poprzez podstawienie dowolnych formuł KRZ w poniższe schematy, są aksjomatami KRZ (w miejsce greckich liter możemy podstawić dowolne formuły KRZ i otrzymać formuły):

1. (α→β)→((β→γ)→(α→γ))

2. α→(β→α)

3. (α→(α→β))→(α→β)

4. α→¬¬α

5. ¬¬α→α

6. (α→β)→(¬β→¬α)

7. (α∧β)→α

8. (α∧β)→β

9. (α→β)→((α→γ)→(α→(β∨γ))) 

10. α→(α∨β)

11. β→(α∨β)

12.  (α→γ)→((β→γ)→((α∨β)→γ))) 

13. (α↔β)→(α→β)

14. (α↔β)→(β→α)

15. (α→β)→((β→α)→(α↔β))

Reguły wnioskowania

RO (reguła odrywania, modus ponens)

α, α→β

–---------

β

W oparciu o pojęcie aksjomatów oraz reguł wnioskowania systemu aksjomatycznego możemy zdefiniować pojęcia wyprowadzalności (wynikania syntaktycznego) oraz dowodu w obrębie systemu aksjomatycznego.

Dowód

Syntaktyczne odpowiedniki semantycznych pojęć

Po stronie syntaktycznej odpowiednikami zdań logicznie prawdziwych są twierdzenia. W poprzednich rozdziałach pojęcie tautologia zastępowało de facto pojęcie zdania logicznie prawdziwego. Od tego rozdziału będziemy pamiętać o tym, że tautologia (bądź zdanie logicznie prawdziwe) jest pojęciem semantycznym, a twierdzenie jest pojęciem syntaktycznym.

Twierdzenie

Zauważmy, że zgodnie z tą definicją, wszystkie twierdzenia są wnioskami ze zbioru aksjomatów (czyli da się je wyprowadzić ze zbioru aksjomatów za pomocą reguły odrywania). Rozważmy przykład wyprowadzania schematu p→p (o którym wiemy, że jest to schemat zdania logicznie prawdziwego) z aksjomatów. Czyli, by udowodnić, że p→p jest twierdzeniem, musimy podać skończony ciąg formuł, którego: 1. każdym elementem jest albo aksjomat, albo formuła, która powstała z poprzednich formuł w wyniku zastosowania reguły odrywania oraz 2. końcową formułą jest p→p:

1. (p→¬¬p)→((¬¬p→p)→(p→p)) (A1)

2. p→¬¬p (A4)

3. (¬¬p→p)→(p→p) (RO, 1,2)

4. ¬¬p→p (A5)

5. p→p (RO, 3,4)

Ciąg formuł 1-5 jest dowodem: formuła 1 jest aksjomatem (powstała poprzez podstawienie w A1 formuły ¬¬p za β, formuły p za α oraz formuły p za γ); formuła 2 jest aksjomatem (powstała poprzez podstawienie w A4 formuły p za α); formuła 3 powstała z poprzednich formuł (czyli 1 i 2) za pomocą reguły odrywania; formuła 4 jest aksjomatem (powstała poprzez podstawienie w A5 formuły p za α); formuła p→p jest ostatnią formułą i powstała z wcześniejszych formuł (3 i 4) w wyniku zastosowania reguły odrywania. 

Twierdzenia (bądź tezy) systemu aksjomatycznego są wyprowadzalne z aksjomatów za pomocą reguły odrywania.

Zauważmy, że twierdzenia są wyprowadzalne (wynikają syntaktycznie) z dowolnego zbioru formuł (w tym z pustego, ∅ ⊢ α), ponieważ by je wyprowadzić, potrzebujemy jedynie aksjomatów i reguły odrywania. Jeśli jakaś formuła α wynika syntaktycznie ze zbioru formuł Γ, to mówimy, że α  jest konsekwencją zbioru formuł Γ. Zbiór aksjomatów oraz wyprowadzalnych z nich twierdzeń stanowi teorię. 

W tym miejscu wprowadźmy (bez dowodu) twierdzenie o dedukcji.

Potoczne intuicje wspierające prawdziwość tego twierdzenia mieliśmy przy okazji sprawdzania poprawności rozumowań z Morskich Opowieści, takich jak "Majtek Jaś Wędrowniczek uważa, że Jim Beam dostał mandat. No, bo: Jim Beam szwędał się po mieście, a ma chorobę filipińską. Skoro Jim Beam ma chorobę filipińśką, to ma obowiązek kwarantanny. No a jeżeli ma obowiązek kwarantanny a równocześnie szwędał się po mieście, to dostał mandat." Czy wnioskiem w tym rozumowaniu jest "Jeżeli ma obowiązek kwarantanny a równocześnie szwędał się po mieście, to dostał mandat" czy samo "Jim Beam dostał mandat", a "ma obowiązek kwarantanny a równocześnie szwędał się po mieście" jest przesłanką? - Okazuje się, że na mocy twierdzenia o dedukcji obie odpowiedzi są poprawne! 

Po stronie semantycznej twierdzenie o dedukcji ma swój odpowiednik (znak wyprowadzalności ⊢ zamień na znak wynikania ⊨).

Rozważmy zbiór wszystkich tautologii oraz zbiór wszystkich twierdzeń. Pierwszy zbiór jest zdefiniowany semantycznie (poprzez pojęcie prawdy), a drugi syntaktycznie (poprzez pojęcie dowodu). Jaka między nimi zachodzi relacja? - Otóż jednym z najważniejszych twierdzeń w KRZ jest twierdzenie o pełności, które mówi, że te dwa zbiory są identyczne.

Możemy wybrać podzbiór zmiennych zdaniowych z alfabetu KRZ i ten wybrany podzbiór będzie służył odpowiednikiem modelu. Nazwijmy ten podzbiór ℳ . Zauważmy, że ℳ  jest arbitralnie wybranym podzbiorem zmiennych zdaniowych (ale dokładnie tak samo jest w przypadku modelu, który zależy od wybranej interpretacji).

Następnie musimy mieć syntaktyczny "odpowiednik" spełniania formuł w modelu. Jest nim wyprowadzalność ze zbioru formuł ℳ. Gwarantuje to twierdzenie, które głosi, że relacja wyprowadzalności w KRZ trafnie i w sposób pełny odowiada relacji wynikania semantycznego w KRZ:

Dla dowolnego zbioru formuł ℳ oraz formuły α jest tak że ℳ ⊢ α wtedy i tylko wtedy, gdy ℳ ⊨ α.

Wyobraź sobie, że istnieje super doskonała istota, która mówi zawsze prawdę, oraz super-komputer, który w ogóle nie ma pojęcia, co zdania znaczą, lecz potrafi wyprowadzać jedne zdania z drugich w sposób doskonały. Gdybyś rozmawiał z nimi przez czat, to nie byłbyś w stanie odróżnić je od siebie....