R O Z P R A W Y
R O C Z N IK I FIL O Z O F IC Z N E T o m X X IX , zesz y t 1 — 1981
LU D W IK BORKOW SKI
C H A R A K T E R Y S T Y K A KW AN T YFIKA T O R O W W A K SJO M A TYCZN EJ TEORII KONSEKW ENCJI
Wsrod aksjomatow teorii konsekwencji mozna odroznic dwa rodzaje:
1 . aksjom aty dotycz^ce m ocy zbioru S i ogolnych wlasnosci konsekwen
cji, 2. aksjom aty charakteryzuj%ce funktory rachunku zdan.
Nie form ulowano w niej aksjomatow charakteryzujqcych kw antyfi- katory. Zapewne, istnieje takie specjalne uj^cie aksjomatyczne rachunku predykatow, przy ktorym nie ma zadnych swoistych regul pierwotnych dla kwantyfikatorow, a jako jedyna regula pierwotna 'wystarcza regula odrywania. Jednakze przy zw yklych uj^ciach tego systemu wyst^puje przynajm niej jedna regula pierwotna dotyczqca kwantyfikatorow, np.
regula dolqczania kw antyfikatora ogolnego do tez. W aksjomatycznej teorii konsekwencji odpowiadaj^cej takiemu uj^ciu nie wystarcza w y- szczegolnienie w yrazen nalez^cych do zbioru tez logicznych, ale trzeiba wprowadzic aksjom aty stwierdzaj^ce dla wyrazen zawierajqcych kwan- tyfikatory, ze wyrazenia o pewnej postaci sq konsekwencjami wyrazen 0 okreslonej postaci lub tez, ze jesli pewne wyrazenia sg tezami logicz- nymi, to okreslone inne wyrazenia sq tezami logicznymi.
W artykule tym wskazuj^, jak aksjomatycznq teori^ konsekwencji mozna rozszerzyc przez dol^czenie aksjomatow charakteryzujqcych kwan- tyfikatory.
Znane sq rozne rownowazne aksjom atyki teorii konsekwencji, aksjo- m atyka o terminach pierwotnych „S ” i „ L ” oraz aksjomatyka o termi- nach pierwotnych „ S ” i „Cn” .
Rownowazna z aksjom atyka Tarskiego o terminach pierwotnych „S ” 1 „C n ” jest aksjom atyka nawiqzujqca do pewnego ukladu regul zaloze- niowych. Wyst^pujqce w niej aksjom aty charakteryzuj^ce funktory ra
chunku zdan stanowi^ trawestacj^ regul systemu zalozeniowego dotycz^- cych tych funktorow (reguly tworzenia dowodow zalozeniowych i regul dol^czania nowych w ierszy do dowodu)1. Jest to zrozumiale, gdyz reguly
1 W w y k o n a n y ch pod m oim k ieru n k iem na U n iw er sy te cie W roclaw skim pra- ca ch m agistersk ich : M. S z a t a n. A k s jo m a ty c z n a teo ria system & w d e d u k c y jn y c h o p a r ty c h na irv tu ic jo m sty c zn y m ra ch u n k u zd a n . 1966; Z. S z a t a n. A k sjo m a ty c zn a te o r ia s y s te m d w d e d u k c y jn y c h o p a rty ch na p ozytyw n ym i im p lik acyjn ym rach u n -
6
L U D W IK B O R K O W S K Ipierwotne systemu zalozeniowego mozna traktowac jako reguty okresla- jqce poj^cie konsekwencji.
Podobnie jak dla funktorow rachunku zdan mozna w aksjomatycznej teorii konsekwencji wprowadzic aksjomaty charakteryzuj^ce kw antyfi- katory stanowiqce trawestacjQ regul pierwotnych dla kwantyfikatorow w systemie zalozeniowym, mianowicie regul opuszczania i dolqczania kwantyfikatorow.
Oprocz poj^cia wyrazenia sensownego (zdaniowego) wprowadzamy jeszcze poj^cie zmiennej wolnej w wyrazeniu sensownym oraz wyrazenia zdaniowego uzyskanego przez prawidlowe podstawienie wyrazenia £ za zmienn^ a w wyrazeniu qp, ktore b^dzie oznaczane przez <p(a/|).-
Jako aksjomaty charakteryzujqce kwantyfikator ogolny przyjm ujem y:
VI p(a/{)eCn({V<p})
a
V 2 p e C n X a a n i e j e s t w o l n e w X V ^ e C n X a
Na podstawie tych aksjomatow oraz tez teorii konsekwencji mozna udowodnic m. i. nast^pujqce twierdzenia:
T 1 peCn 0 -*l~Vp~leCn 0
a
Jesli cp jest tez^ logicznq, to ^ V p- * jest tezq logiczng.
a
T 2 ^ Y v - * i p ( a l i p e C n 0 a
T 3 J e s l i a n i e j e s t w o l n e w <p, t o C n 0 1 a n i e j e s t w o l n e w <f> Z.
2 e C n ( { V f a - H P ) } )
a V I
3 y j e C n ( { p , V ( p - » ^ ) } )
a 2
4 a n i e j e s t w o l n e w {<p, V ( f » - n / ) } 1
5 r V ^ e C n {{<p, V ( ^ - > ^ ) } )
a d V 2 ,
6 r e C n ( { V ( ^ -> ((/)})
a a
5
r V (tp -> y /)-> (< p -+ W < j/)1 e C n 0
a a 6
k u zda.ii. 1966 — zo sta ly podane m. in. szczegolow e dow ody row now aznoSci zw y - klej aksjom atyki te o rii k on sek w en cji o term in ie p ierw otn ym „Cn” z aksjom atykq stan ow iqcq traw estacjq regu l system u zalozen iow ego dla teorii k on sek w en cji w y - znaczonej prze t in tu icjon istyczn y rach unek zdan i przez p o zytyw n y rach unek zdan.
Por. tez: S. S u r m a . U proszczon a a k s jo m a ty k a teo rii k o n s e k w e n c ji T arskiego.
„Z eszyty N au k ow e W yzszej S zk oly P ed agogiczn ej w Opolu. M atem atyk a” 6 :1969 s. 77 - 8 4 .
2 N ie zaznaczam stosow an ia w ty m dow odzie dobrze znanych tez teo rii kon
sek w en cji.
C H A R A K T E R Y S T Y1K A K W A N T Y F1K A T O R0W
7
T 2 i T 3 odpowiadajq dwom a'ksjomatom rachunku predykatow, a T 1 regule pierwotnej doigczania kwantyfikatora ogolnego do tez.
K w antyfikator szczegolowy mozna scharakteryzowac za pomoc^
definicji lub za pomoc^ dwoch nast^pujqcych aksjomatow odpowiada- jqcych regulom jego dolqczania i opuszczania3:
31 r3p_leC n ({<o(a/0})
a
32
x// e Cn(A\j{^}) aa nie jest wolne w X<o{(p) -* \// e Cn (Zu{ 3 ^})
Mowigc dotychczas o aksjomatach teorii konsekwencji mielismy na m ysli teori^ konsekwencji wyznaczonej przez klasyczny rachunek zdan.
ta tw o jednak zauwazyc, ze aksjom aty V l, V2 oraz 31 » 32 mozna do- iqczyc rowndez do aksjomatow teorii konsekwencji wyznaczonej przez nieklasyczne rachunki zdan. Zw ykle bowiem rozne nieklasyczne rachun- k i logiczne otrzym uje si§ z odpowiednich nieklasycznych rachunkow zdan przez dolqczenie tego samego ukladu aksjomatow i regut pierwot- nych dotyczqcych kwantyfikatorow.
* M am y tu na m y sli gentzen ow sk ^ regul^ opuszczania k w an ty fik a to ra szczeg6- lo w e g o Opor. np. E. N i e z n a n s k i . D efin icje i d o w d d in d u k c y jn y a re la cje a n c e - str a ln e . „Studia P h ilo so p h ia e C h ristian ae” 2 :1973 s. 103 - '121).
