D:\User\sbornik_38_pdf\27.DVI


Mathematical Problems of Computer Science 38, 68{69, 2012.

Distr ibutivity in Symmetr ic Constr uctive

Full Lambek Calculus

Mic h a Ãl K o z a k

Pozna¶n Supercomputing and Networking Center
Polish Academy of Sciences, Pozna¶n, Poland

mkozak@man.poznan.pl

In [4 ] we h a ve d e ve lo p e d a n a lg e b r a ic s e m a n t ic s fo r s ym m e t r ic c o n s t r u c t ive lo g ic o f P r o -
fe s s o r Ig o r D . Za s la vs ky [9 ] d e vo id o f s t r u c t u r a l r u le s a n d h a ve s h o wn h o w it is r e la t e d t o
c yc lic in vo lu t ive FL { a lg e b r a s a n d N e ls o n FL ew { a lg e b r a s . B e c a u s e o f t h is a n a lo g y we c a lle d
t h e o b t a in e d c a lc u lu s symmetric constructive full L ambek calculus ( SymConFL ) a n d it s
a lg e b r a ic m o d e ls symmetric constructive F L {algebras.

W e p r o ve d t h a t t h e c la s s o f c yc lic in vo lu t ive FL { a lg e b r a s ( CyIn FL) is m u t u a lly in t e r -
p r e t a b le wit h t h e c la s s o f s ym m e t r ic c o n s t r u c t ive FL { a lg e b r a s ( S ym Co n FL) . Mo r e o ve r , c o n -
s id e r in g SymConFL wit h t h e b a s ic s t r u c t u r a l r u le s exchange ( e) , weakening ( w ) a n d con-
traction ( c) , we h a ve d e ve lo p e d a n a lo g o u s s e m a n t ic s fo r a ll va r ia n t s o f SymConFLS, wh e r e
S is a n y s u b s e t o f fe; w; cg. In p a r t ic u la r , s in c e SymConFL e wc is e xa c t ly s ym m e t r ic c o n -
s t r u c t ive lo g ic , t h e c la s s S ym Co n FLew c is it s a lg e b r a ic s e m a n t ic s .

1

L ike wis e , we ve r ī e d t h a t t h e m u t u a l in t e r p r e t a b ilit y h o ld s b e t we e n t h e c o m m u t a t ive
s u b c la s s e s CyIn FLe a n d S ym Co n FLe, a n d t h e in t e g r a l s u b c la s s e s CyIn FLw a n d S ym Co n FLw .
Fo r t h e c o n t r a c t ive s u b c la s s e s CyIn FLc a n d S ym Co n FLc a s im ila r c o r r e s p o n d e n c e d o e s n o t
h o ld . N e ve r t h e le s s , we p r o ve d t h e t e r m e qu iva le n c e b e t we e n t h e c la s s S ym Co n FLew c ( wh ic h
we a ls o c a lle d t h e c la s s o f Za s la vs ky FL ew c { a lg e b r a s ) a n d t h e c la s s o f N e ls o n FL ew { a lg e b r a s .
A c c o r d in g t o t h e r e s u lt o f M. S p in ks a n d R . V e r o ® [7 , 8 ], wh o h a ve in t r o d u c e d t h e va r ie t y o f
N e ls o n FL ew { a lg e b r a s a s t h e t e r m wis e e qu iva le n t d e ¯ n it io n o f N e ls o n a lg e b r a s [6 ], Za s la vs ky
FL ew c { a lg e b r a s a r e t e r m e qu iva le n t t o N e ls o n a lg e b r a s a s we ll.

In t h is t a lk we a d d it io n a lly c o n s id e r va r ia n t s o f SymConFL t h a t a llo ws o n e t o p r o ve
t h e la w o f d is t r ib u t ivit y o f c o n ju n c t io n o ve r d is ju n c t io n . In s ym m e t r ic c o n s t r u c t ive lo g ic
( SymConFL e wc ) t h is la w is p r o va b le , b u t it is b e yo n d t h e r a n g e o f t h a t s ys t e m wit h o u t
we a ke n in g o r c o n t r a c t io n . W e u s e t h e m e t h o d in d e p e n d e n t ly e la b o r a t e d b y J.M. D u n n [1 ]
a n d G. Min t s [5 ], t h a t c o n s is t s in a llo win g a n a n t e c e d e n t o f a s e qu e n t t o b e a s t r u c t u r e b u ilt
fr o m t wo kin d s o f s t r u c t u r e s in d u c t ive ly.

W e h a ve d e ve lo p e d s u c h s ys t e m s fo r c yc lic in vo lu t ive d is t r ib u t ive FL { a lg e b r a s ( CyIn DFL )
a n d t h e ir c o m m u t a t ive a n d in t e g r a l va r ia n t s [3 ]. U s in g t h e d e ¯ n it io n o f s ym m e t r ic c o n s t r u c -
t ive FL { a lg e b r a s a n d e xt e n d in g it wit h t h e la w o f d is t r ib u t ivit y we c a n a ls o e xp a n d t h e
c o m p le t e n e s s t h e o r e m t o s ys t e m s wit h c o n t r a c t io n .

1We use the naming convention adopted for variants of full Lambek calculus and their algebraic models,
where subscripts stand for structural rules determining properties of fusion [2].

6 8



M. Kozak 6 9

R e fe r e n c e s

[1 ] D u n n , J.M., A Ge n t z e n S ys t e m fo r P o s it ive R e le va n t Im p lic a t io n . Jo u r n a l o f S ym b o lic
L o g ic 3 8 , 3 5 6 -3 5 7 ( 1 9 7 3 ) . A b s t r a c t .

[2 ] Ga la t o s , N ., K o wa ls ki, T., Jip s e n , P ., On o , H .: R e s id u a t e d L a t t ic e s : A n A lg e b r a ic
Glim p s e a t S u b s t r u c t u r a l L o g ic s . E ls e vie r ( 2 0 0 7 )

[3 ] K o z a k, M.: Cyc lic In vo lu t ive D is t r ib u t ive Fu ll L a m b e k Ca lc u lu s Is D e c id a b le . Jo u r n a l
o f L o g ic a n d Co m p u t a t io n 2 1 , 2 3 1 { 2 5 2 ( 2 0 1 1 )

[4 ] K o z a k, M.: S t r o n g N e g a t io n in In t u it io n is t ic S t yle S e qu e n t S ys t e m s fo r R e s id u a t e d L a t -
t ic e s . Ma n u s c r ip t ( 2 0 1 2 )

[5 ] Min t s , G.: Cu t E lim in a t io n Th e o r e m fo r R e le va n t L o g ic s . Jo u r n a l o f Ma t h e m a t ic a l S c i-
e n c e s 6 , 4 2 2 { 4 2 8 ( 1 9 7 6 ) . Tr a n s la t e d fr o m Issledovanija po konstructivnoj mathematike i
matematiceskoj logike V, Izdatelstvo Nauka, 1972.

[6 ] R a s io wa , H .: N { L a t t ic e s a n d Co n s t r u c t ive L o g ic wit h S t r o n g N e g a t io n . Fu n d a m e n t a
Ma t h e m a t ic a e 4 6 , 6 1 { 8 0 ( 1 9 5 8 )

[7 ] S p in ks , M., V e r o ®, R .: Co n s t r u c t ive L o g ic wit h S t r o n g N e g a t io n Is a S u b s t r u c t u r a l L o g ic .
I. S t u d ia L o g ic a 8 8 , 3 2 5 { 3 4 8 ( 2 0 0 8 )

[8 ] S p in ks , M., V e r o ®, R .: Co n s t r u c t ive L o g ic wit h S t r o n g N e g a t io n Is a S u b s t r u c t u r a l L o g ic .
II. S t u d ia L o g ic a 8 9 , 4 0 1 { 4 2 5 ( 2 0 0 8 )

[9 ] Za s la vs ky, I.D .: S ym m e t r ic Co n s t r u c t ive L o g ic ( in R u s s ia n ) . P u b lis h in g H o u s e o f
A c a d e m y o f S c ie n c e s o f A r m e n ia S S R ( 1 9 7 8 )