Założeniowe systemy normalnych logik
modalnych
Marcin Tkaczyk
W niniejszym tekście jest zaprezentowany system logiki modalnej K zbu-
dowany metodą założeniową, czyli metodą dedukcji naturalnej opracowaną
przez J. Słupeckiego i L. Borkowskiego, a także dowody odpowiednich twier-
dzeń o równoważności prezentowanego systemu oraz aksjomatycznego ujęcia
logiki modalnej K. Ponadto pokazana jest metoda budowania metodą założe-
niową wielu mocniejszych od K normalnych systemów modalnych w oparciu
o rezultaty uzyskane dla systemu K.
Dotychczasowe próby budowania systemów modalnych metodą założe-
niową pochodzą od jednego z twórców tej metody, Borkowskiego.1 Wyniki
Borkowskiego podlegajÄ… jednak pewnym ograniczeniom.
Przede wszystkim Borkowski uzyskał jedynie założeniowe systemy S4 i
S5, należące do najmocniejszych systemów modalnych. Nie wiadomo, jak z
tych systemów uzyskać systemy słabsze. Ponadto Borkowski odwołuje się
w sposób istotny bądz
do pojęcia implikacji ścisłej z", bądz
do indeksowa-
nia zmiennych zdaniowych. Część reguł przyjętych przez Borkowskiego ma
wreszcie faktycznie charakter definicji w postaci dwóch odwrotnych schema-
tów wnioskowania, gwarantowanych przez dwie implikacje, składające się na
definicyjną równoważność. Tymczasem do specyfiki założeniowego systemu
logiki klasycznej należy niezawieranie pierwotnych reguł zastępowania defi-
nicyjnego.
W zwiÄ…zku z zarysowanymi uwagami zachodzi potrzeba kontynuowania
dzieła Słupeckiego i Borkowskiego przez rozbudowę metody założeniowej.
Jest to cel niniejszego tekstu.
1
Por. L. Borkowski, O terminach modalnych, w: Tenże, Studia logiczne. Wybór, TN
KUL, Lublin 1990, s. 138 173. Tenże, O pewnym systemie logicznym opartym na regułach
i jego zastosowaniu przy nauczaniu logiki matematycznej. R. III. Nieklasyczne rachunki
logiczne, tamże, s. 174 183.
1
1 Aksjomatyzacja systemu K
Doniosłość systemu logiki modalnej K bierze się stąd, że  używając
terminologii E. J. Lemmona  jest to najsłabsza normalna logika modalna.
Wszelkie normalne systemy logiki modalnej (a są to systemy najczęściej przez
logików badane) zawierają system K. Standardowa (aczkolwiek niejedyna)
aksjomatyzacja systemu K przedstawia się następująco.2
System K jest nadbudowany nad klasycznym rachunkiem zdań i zawiera
oprócz podstawień jego tez jeden aksjomat osobliwy, zwany często wzorem
(K):
(p q) ( p q) (1)
definicjÄ™
( Ć) = (Ź ŹĆ) (2)
oraz  oprócz reguł podstawiania i odrywania  regułę procedury dowodo-
wej
Ć
(3)
( Ć)
Sławny system T  przykładowo  powstaje z systemu K przez dołączenie
wzoru ( p p), a system D  przez dołączenie wzoru ( p p).
2 Założeniowy system klasycznego rachunku
zdań
Założeniowy system klasycznego rachunku zdań J. Słupeckiego i L. Bor-
kowskiego opiera się na następujących założeniach: siedem pierwotnych reguł
dołączania nowych wierszy do dowodu o dziesięciu schematach oraz jedna
pierwotna reguła tworzenia dowodu, mianowicie reguła tworzenia założenio-
wego dowodu nie wprost.3 Reguły dołączania nowych wierszy do dowodu
2
Por. G. E. Hughes, M. J. Cresswell, A New Introduction to Modal Logic, Routledge,
London and New York 1996, s. 25.
3
Por. L. Borkowski, Wprowadzenie do logiki i teorii mnogości, TN KUL, Lublin 1991,
s. 31 38.
2
pozwalają na wnioskowanie odpowiednio według następujących schematów:
RO (Ć È), Ć È
DK Ć, È (Ć '" È)
OK (Ć '" È) Ć
(Ć '" È) È
DA Ć (Ć (" È)
(4)
È (Ć (" È)
OA (Ć (" È), (ŹĆ) È
DE (Ć È), (È Ć) (Ć a" È)
OE (Ć a" È) (Ć È)
(Ć a" È) (È Ć)
Natomiast reguła tworzenia założeniowego dowodu nie wprost stwierdza, że
za tezę wolno uznać wszystkie i tylko takie wyrażenia o postaci
Ć1 (Ć2 (Ć3 · · · (Ćn-1 Ćn) . . .)) (n 1) (5)
dla których istnieje założeniowy dowód nie wprost, to znaczy taki skończony
ciąg wyrażeń, że
" w n - 1 jego wierszach występują wyrażenia Ć1, Ć2, Ć3, . . . , Ćn-1 jako
założenia twierdzenia,
" w n wierszu (ŹĆn) jako założenie dowodu nie wprost,
" wszystkie pozostałe wiersze są uprzednio dowiedzionymi tezami lub
zostają uzyskane z wierszy wcześniejszych za pomocą reguł dołączania
nowych wierszy do dowodu (4), oraz
" w dowodzie występują dwa wiersze sprzeczne.
Wtórna w systemie jest reguła tworzenia założeniowego dowodu wprost, róż-
niąca się od reguły tworzenia dowodu nie wprost tym, że z założeń twierdze-
nia, bez założenia dowodu nie wprost, należy w analogiczny sposób wypro-
wadzić wyrażenie Ćn zamiast dwóch wyrażeń sprzecznych.
J. Słupecki i L. Borkowski udowodnili, że tak określony system jest równo-
ważny klasycznemu rachunkowi zdań, to znaczy istnieje założeniowy dowód
nie wprost dla wszystkich i tylko tych wyrażeń klasycznego rachunku zdań,
że wyrażenia te sprawdzają się w klasycznej matrycy dwuwartościowej czyli
są tezami aksjomatycznych systemów klasycznego rachunku zdań.
3
3 Określenie założeniowego systemu K
Konstruowany założeniowy system logiki modalnej K oprzemy na przed-
stawionym w paragrafie 2 założeniowym systemie klasycznego rachunku zdań.
Ponieważ, jak wspomniano w paragrafie 2 istnieje dowód, że system Słu-
peckiego i Borkowskiego jest równoważny innym systemom klasycznego ra-
chunku zdań, wolno nam uznać, że jest on też równoważny systemowi aksjo-
matycznemu klasycznego rachunku zdań, na którym opiera się przedstawiony
w paragrafie 1 aksjomatyczny system logiki modalnej K.
Pokażemy dwa sposoby, na jakie można uzyskać założeniowy system logiki
modalnej K z założeniowego systemu klasycznego rachunku zdań. Pierwszy
sposób jest bardziej intuicyjny, drugi sposób jest mniej intuicyjny, ale dosko-
nalszy formalnie. Pokażemy, że oba sposoby są inferencyjnie równoważne, tj.
dają ten sam zbiór tez, oraz że są równoważne systemowi aksjomatycznemu.
Przy pierwszym sposobie wprowadzamy jedną pierwotną regułę dołącza-
nia nowych wierszy do dowodu, uzupełniając listę (4). Nowa reguła zezwala
na dołączanie nowych wierszy do dowodu zgodnie ze schematem
( Ć1), ( Ć2), . . . , ( Ćn-1)
(6)
( Ćn)
jeżeli wyrażenie (Ć1 (Ć2 (Ć3 · · · (Ćn-1 Ćn) . . .))) jest uprzednio
dowiedzionÄ… tezÄ….
Reguła (6) jest, jak pokażemy, równoważna aksjomatowi (1) oraz regule
(3). Pozostaje jednak definicja (2), którą trzeba przyjąć jako odrębne zało-
żenie. Tutaj tkwi główny mankament techniczny omawianego rozwiązania.
Do specyfiki systemu założeniowego należało bowiem dotąd, że nie wystę-
powały w nim pierwotne reguły zastępowania definicyjnego. Wprowadzenie
takiej reguły nie jest żadną katastrofą, zwłaszcza że odpowiednie reguły de-
finicyjne są wtórne w założeniowym systemie klasycznego rachunku zdań.
Ponadto większość reguł przyjmowanych dla uzyskania systemu modalnego
w pracach Borkowskiego ma również faktycznie charakter definicji przyjętych
w postaci dwóch odwrotnych schematów wnioskowania. Jednakże wprowa-
dzenie definicji stanowi odejście od pewnej specyfiki systemu założeniowego.
Powstaje zatem pytanie, czy nie można by zbudować założeniowego sys-
temu logiki modalnej K w taki sposób, by uniknąć wskazanej niedogodności.
Rzeczywiście, jest taka możliwość, którą obecnie przedstawimy jako drugie
rozwiÄ…zanie zadanego problemu.
Założeniowy system logiki modalnej K można uzyskać z założeniowego
systemu klasycznego rachunku zdań przez przyjęcie dwóch pierwotnych reguł
dołączania nowych wierszy do dowodu (względnie jednej reguły o dwóch
4
schematach). Reguły te pozwalają na dołączanie nowych wierszy do dowodu
według schematu
( Ć1), ( Ć2), . . . , ( Ćn-1)
(7)
(Ź ŹĆn)
oraz według schematu
(Ź ŹĆ1), (Ź ŹĆ2), . . . , (Ź ŹĆn-1)
(8)
( Ćn)
w obu wypadkach pod tym warunkiem, że wyrażenie
(Ć1 (Ć2 (Ć3 · · · (Ćn-1 Ćn) . . .)))
jest uprzednio dowiedzioną tezą. W takim ujęciu uzyskuje się system K bez
potrzeby przyjmowania reguł definicyjnych.
Podsumowując, założeniowy system logiki modalnej K można uzyskać z
założeniowego systemu klasycznego rachunku zdań na dwa sposoby: przyjmu-
jąc dodatkową regułę (6) i zarazem przyjmując z systemu aksjomatycznego
logiki modalnej K regułę zastępowania definicyjnego (2) lub też przyjmując
obok założeń klasycznego rachunku zdań reguły (7) i (8) bez konieczności
akceptowania jakichkolwiek innych założeń.
4 Równoważność systemów założeniowych K
Dowiedziemy, że obydwa sposoby budowania założeniowego systemu lo-
giki modalnej K przedstawione w paragrafie 3 są równoważne.
Lemat 1 Reguły (7) i (8) są wtórne względem reguły (6) i definicji (2) na
gruncie założeniowego systemu klasycznego rachunku zdań.
Dowód: Załóżmy, że pewne wyrażenie (Ź ŹĆ) zostało wprowadzone do do-
wodu na mocy reguły (7). Wówczas na mocy reguły (6) wolno do dowodu
dołączyć wyrażenie ( Ć), z którego przez zastosowanie definicji (2) otrzymu-
jemy wyrażenie (Ź ŹĆ).
Załóżmy teraz, że pewne ( Ć) zostało dołączone do dowodu na mocy
reguły (8). Wówczas do dowodu należą odpowiednie wyrażenia
(Ź ŹĆ1), (Ź ŹĆ2), . . . , (Ź ŹĆm),
z których przez zastosowanie definicji (2) otrzymujemy wyrażenia
( Ć1), ( Ć2), . . . , ( Ćm),
które wolno dołączyć do dowodu, w oparciu zaś o te wyrażenia, na mocy
reguły (6), wolno włączyć do dowodu wyrażenie ( Ć). To kończy dowód.
5
Lemat 2 Reguła (6) jest wtórna względem reguł (7) i (8) na gruncie zało-
żeniowego systemu klasycznego rachunku zdań.
Dowód: Załóżmy, że pewne wyrażenie ( Ć) zostało dołączone do dowodu
zgodnie z regułą (6). Wówczas do dowodu należą odpowiednie wyrażenia
( Ć1), ( Ć2), . . . , ( Ćm).
Z uwagi na te wyrażenia oraz regułę (7) do dowodu wolno dołączyć wyrażenie
(Ź ŹĆ).
Ponadto do dowodu zawsze wolno dołączyć tezę klasycznego rachunku
zdań (Ć Ć). Stąd zaś i z (Ź ŹĆ) z uwagi na regułę (8) do dowodu wolno
dołączyć wyrażenie ( Ć), co kończy dowód.
Lemat 3 Definicja (2) jest wyprowadzalna z reguł (7) i (8) na gruncie za-
łożeniowego systemu klasycznego rachunku zdań.
Dowód: Ponieważ w założeniowym systemie klasycznego rachunku zdań wtórna
jest reguła zastępowania członów równoważności (dowodzona w zwykły spo-
sób, przez indukcję po długości wyrażenia), wystarczy udowodnić, że tezą
założeniowego systemu K uzyskanego przez dołączenie do założeniowego sys-
temu klasycznego rachunku zdań reguł (7) oraz (8) jest wyrażenie
( p a" Ź Źp)
odpowiadajÄ…ce definicji (2).
Dowodzimy implikacji w prawą stronę. Załóżmy, że ( p). Z uwagi na tezę
(p p) do dowodu wolno dołączyć na mocy reguły (7) (Ź Źp).
Dowodzimy implikacji w lewą stronę. Załóżmy, że (Ź Źp). Z uwagi na
tezę (p p) na mocy reguły reguły (8) do dowodu wolno dołączyć ( p). To
kończy dowód.
Twierdzenie 1 Założeniowe systemy logiki modalnej K uzyskane przez do-
łączenie do założeniowego systemu klasycznego rachunku zdań reguły (6) i
definicji (2) lub też reguł (7) oraz (8) są inferencyjnie równoważne.
Twierdzenie to wynika z lematów 1, 2 oraz 3.
5 Równoważność systemów założeniowych z
systemem aksjomatycznym
Z uwagi na twierdzenie 1 wystarczy udowodnić równoważność jednego
z systemów założeniowych z systemem aksjomatycznym modalnej logiki K,
6
by automatycznie uzyskać rezultat dotyczący obu tych systemów. Przepro-
wadzimy dowód dla systemu uzyskanego przez dołączenie do założeniowego
systemu klasycznego rachunku zdań reguły (6) i definicji (2). W tym celu
dowiedziemy następujących lematów.
Lemat 4 Wzór (1) jest tezą założeniowego systemu logiki modalnej K.
Dowód: Załóżmy ( (p q)) oraz ( p). Tezą jest wyrażenie
(p q) (p q).
Stąd na mocy reguły (6) wyprowadzamy ( q), co kończy dowód.
Lemat 5 Reguła procedury dowodowej (3) jest wtórna w założeniowym sys-
temie logiki modalnej K.
Dowód: Załóżmy, że Ć jest tezą. Na mocy reguły (6), przy n = 1, do bezzało-
żeniowego dowodu wolno dołączyć ( Ć), zatem ( Ć) też jest tezą, co kończy
dowód.
Lemat 6 Reguła wnioskowania (6) jest wtórna w aksjomatycznym systemie
logiki modalnej K.
Dowód: Załóżmy, że pewne wyrażenie o postaci
Ć1 (Ć2 (Ć3 · · · (Ćn-1 Ćn) . . .))
jest tezą. Stąd na mocy reguły (3) tezą jest
(Ć1 (Ć2 (Ć3 · · · (Ćn-1 Ćn) . . .)))
Stąd przez (n - 1)-krotne stosowanie aksjomatu (1) wykazujemy, że tezą jest
wyrażenie
Ć1 ( Ć2 ( Ć3 · · · ( Ćn-1 Ćn) . . .)),
które jest gwarantem niezawodności schematu wnioskowania odpowiadają-
cego regule (6), co kończy dowód.
Twierdzenie 2 Założeniowe systemy logiki modalnej K są inferencyjnie rów-
noważne aksjomatycznemu systemowi logiki modalnej K.
Dowód: Z lematów 4, 5, 6 wynika równoważność systemu aksjomatycznego
i systemu założeniowego opartego na regule (6) i definicji (2), należącej do
tego systemu, jak też do systemu aksjomatycznego. Z twierdzenia 1 wynika
równoważność obu przedstawionych ujęć założeniowych. To wystarczy dla
dowodu.
7
6 Założeniowe systemy innych normalnych lo-
gik modalnych
Najczęściej badane systemy normalnych logik modalnych powstają z sys-
temu K przez dołączenie odpowiednich osobliwych aksjomatów, których głów-
nym funktorem jest często funktor implikacji. Można wymienić następujące
aksjomaty:
p p (9)
p p (10)
p p (11)
p p (12)
p p (13)
System D powstaje przez dołączenie do systemu K wzoru (9). System T
 przez dołączenie wzoru (10). System B  przez dołączenie do systemu K
wzorów (10) i (11). System S4 powstaje z K przez dołączenie wzorów (10) i
(12), a system S5 przez dołączenie (10) oraz (13).
A
atwo udowodnić  przy pomocy twierdzenia o dedukcji oraz naszych
twierdzeń (1) oraz (2)  następujące twierdzenie
Twierdzenie 3 Jeżeli pewien aksjomatyczny system normalnej logiki mo-
dalnej L powstaje z aksjomatycznego systemu K przez dołączenie do K oso-
bliwych aksjomatów o postaci (Ć1 È1), (Ć2 È2), . . . , (Ćn Èn), to zaÅ‚o-
żeniowy system L, inferencyjnie równoważny odpowiedniemu systemowi ak-
sjomatycznemu, powstaje przez dołączenie do założeniowego systemu logiki
modalnej K przez dołączenie osobliwych pierwotnych reguł dołączania no-
wych wierszy do dowodu o schematach
Ć1 È1
Ć2 È2
. . .
Ćn Èn
8
Na przykład założeniowy system T uzyskujemy przez dołączenie do założe-
niowego systemu K reguły o schemacie ( Ć) Ć, a system S5 przez dołącze-
nie do K reguł o schematach ( Ć) Ć oraz ( Ć) ( Ć). Nie ma przy tym
znaczenia, którą z zaprezentowanych metod budowy założeniowego systemu
K wybierzemy.
Streszczenie
Most normal modal logics have been constructed as axiomatic sys-
tems rather than natural deduction. However, a lot of them have
Gentzen-style or Kalish-Montague-style counterparts. Unfortunately,
very few systems have SÅ‚upecki-Borkowski-style natural deduxtion co-
unterparts. To fill in the gap is an aim ot the present paper.
The system K is developed as a Leśniewski-Borkowski-style natural
deduction system in two ways. Equivalence of the systems is proved.
A way is described to develop other normal systams begining with the
given system K.
SÅ‚owa kluczowe: logika modalna, normalna logika modalna, deduk-
cja naturalna, system założeniowy
Key words: modal logic, normal modal logic, natural deduction
9