Elementy metalogiki rachunku zdań
1
Pojęcie dowodu
DEF.1 (Dowód – wersja dla humanistów). Dowodem (formalnym) formuły A w oparciu o zbiór
formuł X na gruncie KRZ nazywamy każdy skończony ciąg formuł:
(D)
D 1, D 2, …, Dn,
taki że:
(1) formuła ostatnia Dn jest identyczna z formułą dowodzoną A,
(2) formuła pierwsza D 1 jest aksjomatem KRZ bądź elementem zbioru X
(3) każda formuła w ciągu (D) nie będąca ani aksjomatem KRZ, ani elementem zbioru X
powstaje z poprzedzających ją formuł w tym ciągu przez zastosowanie do nich reguły
odrywania (RO).
Notacja: Przez Arz będziemy oznaczać zbiór aksjomatów KRZ.
X ├─ KRZ A czytamy:
istnieje co najmniej jeden dowód formuły A w oparciu o zbiór X (na gruncie KRZ). ■
2
Dygresje: (1) W podanej definicji odwołałem się tylko do reguły odrywania, gdyż w przyjętej tu
wersji aksjomatycznego systemu KRZ jest ona jedyną pierwotną regułą inferencyjną. Gdy
rozważamy system o innych regułach pierwotnych, np. taki, w którym obowiązuje jeszcze
reguła podstawiania, należy w definicji dowodu odwołać się do tych reguł.
(2) Niekiedy wprowadza się węższe pojęcie dowodu: dowodu formuły A w oparciu o jedynie
zbiór aksjomatów. Natomiast wyprowadzenie w sensie podanej tu definicji nazywa się
derywacją. Różnicę między jednym a drugim można scharakteryzować następująco: w ciągu,
który jest dowodem w oparciu o (jedynie) aksjomaty, każda formuła jest tezą KRZ, natomiast w
ciągu, który jest derywacją, mogą występować formuły nie będące tezami KRZ (mianowicie
formuły ze zbioru X). Każdy dowód formuły w oparciu o aksjomaty jest jej derywacją ze zbioru
pustego. ■
Precyzyjna definicja dowodu brzmi następująco:
3
Pojęcie konsekwencji inferencyjnej
DEF. 1a (Dowód – wersja dla purystów). Dowodem (formalnym) formuły A w oparciu o zbiór X
na gruncie KRZ nazywamy każdy skończony ciąg formuł D 1, …, Dn, taki że Dn = A oraz dla każdego wskaźnika k ≤ n spełniony jest przynajmniej jeden z następujących warunków:
(1) Dk ∈ Arz ∪ X,
(2) istnieją takie i, j, że i < k, j < k oraz Dj ma postać Di → Dk.
Pojęcie dowodu służy do zdefiniowania pojęcia konsekwencji inferencyjnej (wynikania
syntaktycznego):
DEF. 2 (Konsekwencja inferencyjna). Formuła A jest konsekwencją inferencyjną zbioru formuł
X wtw istnieje co najmniej jeden dowód formuły A w oparciu o zbiór X (na gruncie KRZ).
Notacja: Cn( X) = zbiór wszystkich konsekwencji inferencyjnych zbioru formuł X;
A ∈ Cn( X) czytamy: formuła A jest (jedną z) konsekwencją inferencyjną zbioru formuł X.
Podaną definicję można symbolicznie zapisać następująco: A ∈ Cn( X) wtw X ├─KRZ A. ■
4
Pojęcie konsekwencji inferencyjnej
Dygresja: Pojecie konsekwencji w sensie tu używanym wprowadził A. Tarski. Biorąc rzecz
ściśle, Cn jest funkcją przyporządkowującą podzbiorom zbioru For (tj. formuł języka KRZ)
podzbiory zbioru For, czyli jest funkcją typu:
Cn: 2For → 2For,
gdzie 2For oznacza zbiór wszystkich podzbiorów zbioru For (= zbiór potęgowy zbioru For). ■
DEF. 3 (Teza KRZ). Formuła A jest tezą KRZ wtw jest ona aksjomatem KRZ bądź posiada co
najmniej jeden dowód w oparciu o aksjomaty KRZ.
Dygresja: Ciąg jednowyrazowy 〈 A〉, gdzie A jest aksjomatem, ma wszelkie znamiona dowodu
formuły A w oparciu o aksjomaty. Tak więc, w definicji tezy wystarczyłoby sformułowanie „ma
co najmniej jeden dowód w oparciu o aksjomaty”. ■
Notacja: Piszemy A ∈ Cn(∅), gdy A jest tezą KRZ. Symbol ∅ oznacza zbiór pusty. ■
5
Pojęcie konsekwencji inferencyjnej
Twierdzenie 1 (O słuszności aksjomatyki KRZ). Każda teza KRZ jest tautologią KRZ.
Symbolicznie: Cn(∅) ⊆ Trz .
Szkic dowodu. Aksjomaty zostały tak dobrane, że każdy z nich jest tautologią KRZ. Zgodnie z
semantycznym twierdzeniem o odrywaniu, stosując RO do przesłanek będących tautologiami
KRZ otrzymujemy wnioski będące też tautologiami KRZ. ■
Później udowodnimy, że prawdziwa jest także inkluzja odwrotna. Zajmiemy się teraz
własnościami operacji Cn.
Twierdzenie 2 (O zwrotności). X ⊆ Cn( X).
Dowód: Znaczy to, że dla dowolnej formuły A, jeżeli A ∈ X, to A ∈ Cn( X). Niech więc A będzie jakąkolwiek formuła należącą do zbioru X. Ciąg 〈 A〉 , którego jedynym wyrazem jest A, jest
dowodem ze zbioru X (na podstawie definicji dowodu). Stąd A ∈ Cn( X). ■
6
Pojęcie konsekwencji inferencyjnej
Twierdzenie 3 (O idempotencji). Cn(Cn( X)) = Cn( X).
Szkic dowodu.
(I) Cn( X) ⊆ Cn(Cn( X)); jest to wniosek z twierdzenia poprzedniego.
(II) Cn(Cn( X)) ⊆ Cn( X).
Znaczy to, że dla dowolnej formuły A, jeżeli A ∈ Cn(Cn( X)), to A ∈ Cn( X). Czyli: jeżeli A posiada dowód w oparciu o twierdzenia, które wcześniej zostały udowodnione w oparciu o
pewien wyjściowy zbiór przesłanek X, to A posiada też dowód w oparciu o jedynie ów zbiór X.
Niech więc ciąg D 1, … Dn będzie dowodem formuły A w oparciu o zbiór Cn( X). Na bazie tego
ciągu konstruujemy nowy ciąg w ten sposób, że występujące w ciągu D 1, … Dn twierdzenia
wcześniej udowodnione zastępujemy ich dowodami ze zbioru X. Ów nowy ciąg jest
poszukiwanym dowodem. Dowód precyzyjniejszy znajduje się w: Batóg 1994, s. 67-68. ■
7
Pojęcie konsekwencji inferencyjnej
Twierdzenie 4 (O monotoniczności). Jeżeli X ⊆ Y, to Cn( X) ⊆ Cn( Y).
Dowód: Zakładamy, że X ⊆ Y i A ∈ Cn( X). Wykażemy, że A ∈ Cn( Y), czyli że A ma dowód (na gruncie KRZ) w oparciu o zbiór Y. Niech D 1, … Dn będzie dowodem A w oparciu o zbiór X.
Ciąg ten jest również dowodem A w oparciu o zbiór Y, bo X ⊆ Y. ■
Dygresja: Własność ta odzwierciedla przekonanie, że powiększenie zbioru przesłanek nie
zmniejsza, a jedynie może zwiększyć zakres naszej wiedzy, rozumianej jako zbiór zdań, które są
uzasadnione na podstawie tych przesłanek. Innymi słowy, jeżeli A jest uzasadnione na podstawie
przesłanek X, to żaden dodatkowy argument nie może podważyć zasadności zdania A (o ile nie
kwestionuje, któreś z przesłanek z X). Operację, która nie spełnia tego warunku nazywa się
niemonotoniczną. Logiki z operacją niemonotoniczną są wykorzystywane w computer science.
Niektóre nasze wnioskowania nie cechuje monotoniczność. Powiększenie zbioru przesłanek
może prowadzić do rewizji pewnych wcześniejszych przekonań.
8
Pojęcie konsekwencji inferencyjnej
Często podawanym przykładem wnioskowania niemonotonicznego jest wyprowadzenie
konkluzji, że Ćwirek lata na podstawie przesłanki, że jest on ptakiem (jeśli bowiem coś jest
ptakiem, to możemy oczekiwać, że będzie latało), oraz odrzucenie tej konkluzji po dodaniu
nowej przesłanki, że Ćwirek jest strusiem; sytuacja przedstawia się więc następująco (symbol Ca
oznacza operację konsekwencji niemonotonicznej):
X = {Ptaki zwykle latają, Strusie nie latają, Ćwirek jest ptakiem},
Ćwirek lata ∈ Ca( X), ale
Ćwirek lata ∉ Ca( X ∪ {Ćwirek jest strusiem}). ■
9
Pojęcie konsekwencji inferencyjnej
Twierdzenie 5 (O finitystyczności).
A ∈ Cn( X) wtw istnieje zbiór Y ⊆ X taki, że Y jest skończony i A ∈ Cn( Y).
Szkic dowodu: Powód jest prosty: każdy dowód jest skończonym ciągiem formuł, a zatem
korzystamy w nim ze skończonej ilości elementów zbioru X – to właśnie będzie zbiór Y. Z
drugiej strony, na mocy twierdzenia o monotoniczności (tj. twierdzenia 4), skoro Y ⊆ X oraz
A ∈ Cn( Y), to A ∈ Cn( X). Precyzyjny dowód znajduje się w: Batóg 1994, s. 69. ■
10
Pojęcie konsekwencji inferencyjnej
Twierdzenie 6 (Syntaktyczne twierdzenie o odrywaniu).
Jeżeli ( A → B) ∈ Cn( X) oraz A ∈ Cn( X), to B ∈ Cn( X).
Dowód: Załóżmy, że ( A → B) ∈ Cn( X) oraz A ∈ Cn( X). Wykażemy, że B ∈ Cn( X).
Z założeń wnosimy, że formuły ( A → B) oraz A posiadają dowody w oparciu o zbiór X. Niech
tymi dowodami będą – odpowiednio – następujące ciągi:
D 1, … Dn oraz
E 1, … En.
Wówczas ciąg będący ich połączeniem i zakończony formułą B
D 1, … Dn , E 1, … En, B
jest dowodem formuły B w oparciu o zbiór X. A zatem, B ∈ Cn( X). ■
11
Pojęcie konsekwencji inferencyjnej
Twierdzenie 7 (Eksplozyjność). Cn({ A, ~ A}) = For.
Twierdzenie to można zapisać też następująco: B ∈ Cn({ A, ~ A}) wtw B ∈ For.
O operacji Cn spełniającej ten warunek mówimy, że jest eksplozyjna. Głosi on bowiem, że z
dwóch formuł wzajemnie sprzecznych wyprowadzalna jest dowolna formuła zdaniowa. Mówiąc
metaforyczne, sprzeczność eksploduje, czyniąc tezami wszystkie formuły danego języka – znika
różnica pomiędzy tezą a formułą sensowną, przez co system staje się przepełniony.
Inkluzja Cn({ A, ~ A}) ⊆ For jest oczywista. Inkluzja odwrotna For ⊆ Cn({ A, ~ A}) wynika stąd,
że tezą KRZ jest prawo Dunsa Szkota, na którym możemy oprzeć regułę Dunsa Szkota:
A, ~ A
.
B
12
Pojęcie konsekwencji inferencyjnej
Dygresja: Na gruncie KRZ poprawne formalnie jest więc następujące wnioskowanie:
Skoro
Sokrates jest filozofem,
i zarazem
Sokrates nie jest filozofem,
a zatem:
Osioł fruwa.
Możliwe jest zmodyfikowanie operacji Cn, które blokuje wymienioną tu własność (a tego typu
wnioskowania dyskryminuje). Uzyskana w ten sposób operacja konsekwencji umożliwia
konstruowanie systemów dedukcyjnych, które tolerują (w ograniczonym zakresie) sprzeczność.
Mimo, że występują w nich dwie formuły wzajemnie sprzeczne, A i ~ A, nie są przepełnione, tj.
nie wszystkie formuły są ich tezami. Systemy takie określa się mianem parakonsystentnych. ■
13