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 β.
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.
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):
(α→β)→((β→γ)→(α→γ))
α→(β→α)
(α→(α→β))→(α→β)
α→¬¬α
¬¬α→α
(α→β)→(¬β→¬α)
(α∧β)→α
(α∧β)→β
(α→β)→((α→γ)→(α→(β∨γ)))
α→(α∨β)
β→(α∨β)
(α→γ)→((β→γ)→((α∨β)→γ)))
(α↔β)→(α→β)
(α↔β)→(β→α)
(α→β)→((β→α)→(α↔β))
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 w systemie aksjomatycznym
Dowodem w systemie aksjomatycznym jest dowolny skończony ciąg formuł δ1, δ2, ..., δn taki, że każda formuła δi jest bądź aksjomatem, bądź została otrzymana na mocy reguły odrywania z przesłanek występujących wcześniej w tym ciągu.
Mając pojęcie dowodu, możemy zdefiniować syntaktyczny odpowiednik zdań logicznie prawdziwych. Przypomnijmy definicję (ponieważ w tym rozdziale nie posługujemy się pojęciem prawdziwości, to definicja została ukryta pod strzałką po prawej).
Zdanie logicznie prawdziwe, ⊨ α
Zdanie α jest logicznie prawdziwe, ⊨ α, wtedy i tylko wtedy, gdy dla dowolnego modelu ℳ jest tak, że ℳ ⊨ α.
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, ⊢ α
Zdanie α jest twierdzeniem wtedy i tylko wtedy, gdy istnieje dowód w systemie aksjomatycznym, którego ostatnim elementem jest α.
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:
(p→¬¬p)→((¬¬p→p)→(p→p)) (A1)
p→¬¬p (A4)
(¬¬p→p)→(p→p) (RO, 1,2)
¬¬p→p (A5)
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.
Teraz przejdźmy do wyprowadzalności (syntaktyczny odpowiednik wynikania semantycznego; jeśli zapomniałeś, jaka jest definicja wynikania semantycznego, kliknij na strzałkę po prawej stronie). Zdefiniujemy, co to znaczy, że ze zbioru formuł Γ jest wyprowadzalna (albo wynika syntaktycznie) formuła α.
Wynikanie semantyczne, Γ ⊨ α
Formuła α wynika semantycznie ze zbioru formuł Γ wtedy i tylko wtedy, gdy dla każdego modelu ℳ ⊨ Γ jest tak, że ℳ ⊨ α.
Wyprowadzalność, Γ ⊢ α
Ze zbioru formuł Γ jest wyprowadzalna (wynika syntaktycznie) formuła α wtedy i tylko wtedy, gdy istnieje skończony ciąg formuł δ1, δ2, ..., δn, którego ostatnim elementem jest α (α = δn) taki, że każda formuła δi jest bądź aksjomatem, bądź elementem zbioru Γ, bądź została otrzymana na mocy reguły odrywania z przesłanek występujących wcześniej w tym ciągu.
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.
Twierdzenie o dedukcji
Γ ∪ {α} ⊢ β wtedy i tylko wtedy, gdy Γ ⊢ α→β.
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.
Twierdzenie o pełności, ⊢ α wtw ⊨ α
Dla dowolnej formuły α: α jest twierdzeniem KRZ wtedy tylko wtedy, gdy α jest tautologią KRZ.
A co z syntaktycznym odpowiednikiem modelu ℳ (przypomnijmy jego definicję - kliknij na strzałkę)?
Zbiór wszystkich zmiennych zdaniowych, którym została przyporządkowana wartość prawda, nazywa się modelem ℳ .
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....