Def 4. (Teoria) Zbiór formuł X nazywamy teorią wtw X=Cn(X). Elementy zbioru X nazywamy wówczas tezami teorii.
Znaczy to, że teoria to zbiór formuł zamkniękty na operację Cn. Można udowodnić, że:
Twierdzenie 11. Zbiór Trz jest teorią, czyli Trz=Cn(Trz)
Każda formuła, która należy do teorii jest na jej gruncie dowodliwa i należy do tej teorii.
Teorię tworzą wszystkie i tylko te formuły, które są w niej dowodliwe.
Szkic dowodu:
(I) Inkluzja Trz _c Cn(Trz) jest wnioskiem z twierdzeniea o zwrotności operacji Cn.
(II) Cn(Trz) _c Trz. Czyli: jeżeli A e Cn(Trz), to A e Trz. Niech A e Cn(Trz), czyli istnieje dowód formuły A w oparciu o zbór Trz. Każda formuła w tym dowodzie jest tautologią albo powstaje z tautologii przez zastosowanie RO. Zgodnie z semantycznym twierdzeniem o odrywaniu, stosując RO do przesłanek będących tautologiami otrzymujemy wnioski będące też tautologiami KRZ co uzasadnia, że A e Trz.
Każda tautologia posiada dowód i kazda formuła, której dowodziemy w oparciu o tautologię, sama jest tautologią.
Metoda aksjomatyczna jest połowiczną procedurą rozstrzygania czy dana formuła jest tezą KRZ. Jeśli daje ona odpowiedź, to jedynie odpowiedź pozytywną, głoszącą, że rozważana formuła jest tezą. Nie może dostarczyć natomiast odpowiedzi negatywnej, ponieważ faktyczny brak dowodu nie świadczy o niedowodliwości (w ogóle).
Metoda sprowadzania do postaci normalnych:
Def. 5) Inferencyjna równoważność: formuła A jest inferencyjnie równoważna formule B wtw równoważność postaci (A ↔ B) jest tezą KRZ.
Notacja: Piszemy A ~= B (A jest inferencyjnie równoważne B) [ = złożone z dwóch ~~)
np.
Formuła p ~= ~~p gdyż równoważność p ↔ ~~p jest tezą KRZ.
Formuła ~(p → q) ~= (p /\ ~q), gdyż ~(p → q) ↔ (p /\ ~q) jest tezą KRZ.
Formuła
p → (q → r) ~= (p …
Twierdzenie 12: Dla dowolnych formul A, B i C:
(a) A ~= B [zwrotność]
(b) Jeżeli A ~= B, to B ~= A [symetryczność]
( c ) Jeżeli A ~= B i B ~= C, to A ~= C [przechodniość]
Dowody: Batóg str 71 – 87.
Twierdzenie 13:
(a) Jeżeli A ~= B oraz A jest tezą KRZ, to formuła B też jest tezą KRZ [dowód z opusczania równoważności].
(b) Jeżeli A ~= oraz A jest tautologią KRZ, to B jest też tautologią KRZ.
Def 6. (Literały). Literałami nazywamy wyrażenia postaci pi oraz ~pi gdzie p jest zmienną zdaniową (zmienna jest literałem pozytywnym, a negacja literałem negatywnym).
Przykłady: Literałami są: p, ~p, q, ~q.
Def 7: Alternatywa elementarna:
(1) Każdy literał jest alternatywą elementarną
(2) Jeżeli A jest alternatywą elementarną i L jest literałem, to wyrażenie (A v L) jest alternatywą elementarną.
(3) Nie ma innych alternatyw elementarnych poza literałami i takimi wyrażeniami, które można budować wedle reguły (2).
Np.
p, ~p, (p v ~p), ((p v q) v r), ((p v q) v ~r), (((p v ~q) v r) v ~p)
Składnikami alternatyw elementarnych są więc literały, tj zmienne zdaniowie i/lub ich negacje.
Twierdzenie 14: Jeżeli A i B są dowolnymi alternatywami elementarnymi, to formuła A v B jest inferencyjnie równoważna pewnej alternatywie elementarnej.
Notacja: W alternatywach elementarnych opuszczamy nawiasy poza najbardziej zewnętrznymi: zamiast (((p v ~q) v r) v ~p) piszemy: (p v ~q v r v ~p).
Twierdzenie 15: Alternatywa elementarna jest tautologią KRZ wtw co najmniej jedna zmienna zdaniowa występuje w niej zarówno ze znakiem negacji, jak i bez tego znaku.
Tautologie:
· (p v ~p)
· (p v ~q v r v ~p)
Nie tautologie:
· (p v p)
· (p v q v ~r)
Def 8) Koniunkcyjna postać normalna: (kpn)
(1) Każda alternatywa elementarna jest formułą o kpn
(2) Jeżeli A jest dowolną formuła o kpn, zaś B jest dowolną alternatywą elementarną, to wyrażenie o postaci A /\ B jest też formułą o kpn.
(3) Nie ma innych formuł o kpn, poza alternatywami elementarnymi i takimi formułami, które można zbudować wedle reguły (2).
Np. Formułami o kpn są: (stosujemy opuscz. Nawiasów)
· (p v ~q) [gdyż każda alternatywa elementarna jest formuła o kpn]
· (~p v q v r) /\ (~q v r) /\ (~r)
Formułami o kpn nie są:
· (~p v q v r) /\ ((~q /\ r) v r) /\ (~r) [gdyż w drugiej alternatywie występuje koniunkcja]
· (~p v q v r) /\ ~(~q v r) /\ (~r) [gdyż druga alternatywa jest zanegowana]
Twierdzenie 16: Formuła o kpn jest tautologią KRZ wtw każda z alternatyw elementarnych składających się na tę formułę jest tautologią KRZ.
Twierdzenie 17: Każda formuła języka KRZ jest inferencyjnie równoważna pewnej formule o kpn.
Twierdzenie 18: Każda tautologia KRZ jest inferencyjnie równoważna pewnej formule kpn, takiej że każda wchodząca w jej skład alternatywa elementarna zawiera co najmniej jedną zmienną zdaniową, która występuje zarówno ze znakiem negacji, jak i bez tego znaku.
Dowolną formułe można „sprowadzić” do inferencyjnie równoważnej formuły o kpn Sposób postępowania opisany jest w Batóg str 84 – 85.
1. (p ↔ q) ↔ (~p v q) /\ (~q v p)
2. (p → q) ↔ ~p v q
3. ~(p → q) ↔ p /\ ~q
4. ~(p /\ q) ↔ ~p v ~q
5. ~(p v q) ↔ ~p /\ ~q
6. ~~p ↔ p
7. p v (q /\ r) ↔ (p v q) /\ (p v r)
8. (p /\ q) v r ↔ (p v r) /\ (q v r)
1. Usuwamy znaki równoważności i implikacji zgodnie z dwoma pierwszymi prawami.
2. Znaki negacji stojące przed nawiasmi w koniunkcji i alternatywy w oparciu o dwa prawa de morgana.
3. Zlikwidować podówjne i wielokrotne negacje w oparciu o prawo podwójnego przeczenia.
(najlepiej rozpoczynać od znaków negacji najbardziej zewnętrznych! → dobra rada by dr hab. Z. Tworak)
4. Stosować prawa rozdzielności alternatywy względem koniunkcji/koniunkcji względem alternatywy – na ogół dużą liczbę razy.
Jeżeli zachodzi potrzeba zastosować prawa przemienności:
· p /\ q ↔ q /\ p
· p v q ↔ q v p
1. [p /\ q → r) ↔ ~(p /\ q) v r
↔ (~p v ~q) v r) [nie jest to tautologią]
2. (p → q) v (q → p) ↔ (~p v q v ~q v p) [jest tautologią]
3. ~((p → q) /\ (q → p)) ↔ ~(p → q) v ~(q → p)
↔ (p /\ ~q) v (q /\ ~p)↔ ((p /\ ~q) v q) /\ ((p /\ ~q) v ~p)↔ (p v q) /\ (~q v q) /\ (p v ~p) /\ (~q v ~p)
4. (p → ~p) → ~p) (jako ćwiczenie)
Pozwala ona rozstrzygnąć czy formuła jest czy nie jest tautologią.
Dygresja: oprócz kpn rozważa się też tzw alternatywną postać noermalną, pozwalającą rozstrzygnąć czy dana formuła jest kontrtautologią KRZ, czy też nie. Sz. P. dr hab. Z. Tworak temat ten pomija:(
Wcześniej odnotowaliśmy w postaci osobnego twierdzenia, ze każda teza KRZ jest jego tautologią. Było to twierdzenie o słuszności aksjomatyki KRZ. Bez odpowiedzi pozostawilismy natomiast pytanie: Czy każda tautologią KRZ jest jego teza? Pytanie to wyraża zagadanienie o pełności KRZ. Obecnie pokażemy, że odpowiedź na to pytanie jest twierdząca, tj. każda tautologia jest aksjomatem KRZ bądź daje się udowodnić w oparciu aksjomaty.
Twierdzenie 19 (O pełnośco KRZ – słabe)
Dla dowolnej formyły A:
A jest tezą KRZ wtw A jest tautologią KRZ.
Symbolicznie: A e Cn(O) wtw A e Trz [O – zbiór pusty]
Lub inaczej: Cn(O) = Trz.
W dowodzie skorzystamy z następujących twierdzeń (podr. Str ; istnieje wiele dowodów o pełności KRZ); dowód od L. Hepklina (?):
· Syntaktyczne twierdzenie o odrywaniu. Jeżeli formuły (A → B) i A są tezmaki KRZ, to formuła B też jest tezą KRZ.
· Każda tautologia KRZ jest inferencyjnie równoważna pewnej formule o kpn, takiej że każda wchodząca w jeje skład alternatywa elementarna zawiera co najmniej jedną zmienną zdaniową, która występuje zarówno ze znakiem negacji jak i bez tego znaku.
Ponadto skorzystamy z faktów że tezami KRZ są wszystkie formuły języka KRZ, reprezentowane przez schematy:
A v ~A [prawo wył. Środka]
A → A v B [prawo addycji]
A → (A → A /\ B) [prawo koniunkcji]
(A ↔ B) → (B → A) [prawo rozkładania równoważności]
Dowód:
I. każda teza krz jest tautologią krz. Zostało to już udowodnione (twierdzenie o sluszności aksjomatyki krz).
II. Każda tautologia krz jest tezą krz.Dla dowodu przypuśćmy, że A e Trz. Należy pokazać, że A jest tezą krz.
W myśl twierdzenia o kpn istnieje formuła b o kpn, taka że:
i) A jest inferencujnie równoważna B, tj formuła o postaci A ↔ B jest tezą krz:
ii) B = (C1 /\ C2 /\ … /\ Cn)
gdzie każde Ck (dla 1 _< k _< n) jest alternatywą elementarną zawierającą co najmniej jedną zmienną. pi k która występuje zarówno ze znakiem negacji jak i bez niego, tj:
Ck = (p ik v ~p ik v Dk)
Pokażmy teraz, że B jest tezą krz:
Najpierw zauważmy, że
1) pik v ~pik jest tezą krz oraz:
2) pik v ~pik -> pik v ~pik v Dk (prawo addycji)
...
jelonka72