D:\User\sbornik_38_pdf\39.DVI Mathematical Problems of Computer Science 38, 91{92, 2012. On the For malization of Scienti¯c T heor ies Ig o r D . Za s la vs ky Institute for Informatics and Automation Problems of NAS of RA e-mail: zaslav@ipia.sci.am Th e g e n e r a l c o n c e p t o f t h e fo r m a liz a t io n is c o n s id e r e d . Five le ve ls o f t h e fo r m a liz a t io n o f s c ie n t i¯ c t h e o r ie s a r e n o t e d a n d d e s c r ib e d . Th e g e n e r a l c o n c e p t o f t h e fo r m a liz a t io n is c o n n e c t e d wit h t h e s ys t e m a t iz a t io n a n d t h e s p e c i¯ c a t io n o f h u m a n kn o wle d g e . Th e fo r m a liz a t io n o f s o m e b r a n c h o f kn o wle d g e is d e ¯ n e d a s a r e p r e s e n t a t io n o f kn o wle d g e in t h is b r a n c h b y m e a n s o f a n o t h e r b r a n c h wh e n t h is r e p - r e s e n t a t io n is c o n n e c t e d wit h s ys t e m a t iz a t io n a n d s p e c i¯ c a t io n o f kn o wle d g e ; a s a r u le s u c h a r e p r e s e n t a t io n is a p p r o xim a t ive a n d e s t r a n g e d fr o m t h e in it ia l b r a n c h . Th e fo r m a liz a t io n o f d i®e r e n t b r a n c h e s o f s c ie n c e is t yp ic a l fo r s u c h s c ie n c e s a s , fo r e xa m p le , m a t h e m a t ic s a n d p h ys ic s , b u t it t a ke s p la c e a ls o in t h e h u m a n it ie s . Fo r e xa m p le , t h e c r im in a l a n d t h e c ivil la w m a y b e c o n s id e r e d a s a fo r m a liz a t io n o f t h e h u m a n m o r a ls . Th e wr it t e n n a t u r a l la n g u a g e m a y b e c o n s id e r e d a s a fo r m a liz a t io n o f t h e o r a l o n e . W e s h a ll s t u d y s o m e le ve ls in t h e fo r m a liz a t io n o f s c ie n t i¯ c t h e o r ie s . B e lo w ¯ ve le ve ls o f s u c h kin d will b e d e s c r ib e d . Th e ¯ r s t o f t h e m is t h e \descriptional" le ve l. Th e c r e a t io n o f a n y s c ie n t ī c t h e o r y b e - g in s fr o m t h e o b s e r va t io n o f fa c t s . A c o lle c t io n o f t h e o b s e r ve d fa c t s is t h e c o n t e n t o f t h e d e s c r ip t io n a l le ve l. It g ive s a b a s is fo r t h e d e ve lo p m e n t o f t h e t h e o r y in fu t u r e . On t h is le ve l o n ly t h e c o lle c t io n o f fa c t s is p r e s e n t ; t h e t h e o r y ( in t h e o wn s e n s e o f t h is t e r m ) ye t d o e s n o t e xis t . Th e s e c o n d le ve l m a y b e c h a r a c t e r iz e d a s a \linguistic" o n e . It is p e r fo r m e d wh e n t h e o b s e r ve d fa c t s a r e n u m e r o u s a n d m u lt ifo r m , a n d it is n e c e s s a r y t o s ys t e m a t iz e t h e m a n d t o in t r o d u c e s o m e s ys t e m o f n o t io n s g ivin g a c la s s ī c a t io n o f t h e o b s e r ve d fa c t s a n d o f t h e r e la t io n s b e t we e n t h e m . On t h is le ve l t h e language o f t h e t h e o r y is c r e a t e d . Th e t h ir d le ve l m a y b e c h a r a c t e r iz e d a s a n \intuitive logical" o n e . It is p e r fo r m e d wh e n it is n e c e s s a r y t o s p e c ify a n d s ys t e m a t iz e t h e s t a t e m e n t s o f t h e t h e o r y a n d t o e s t a b lis h r e la t io n s b e t we e n t h e m . On t h e h ig h e s t s t a g e o f t h is le ve l s o m e c e n t r a l s t a t e m e n t s o f t h e t h e o r y s o m e t im e s a r e fo r m u la t e d s u c h t h a t a ll t h e s t a t e m e n t s in t h e c o n s id e r e d t h e o r y c a n b e d e d u c e d fr o m t h e m . S u c h c e n t r a l s t a t e m e n t s b e a r d i®e r e n t n a m e s in d i®e r e n t s c ie n c e s . Th e y a r e , fo r e xa m p le , axioms a n d postulates in t h e g e o m e t r y, la ws ( fo r e xa m p le , N e wt o n 's la ws ) in t h e p h ys ic s . S o m e t im e s s u c h c e n t r a l s t a t e m e n t s a r e equations ( fo r e xa m p le , Ma xwe ll's e qu a t io n s in t h e e le c t r o d yn a m ic s , S c h r yd in g e r 's e qu a t io n in t h e qu a n t u m m e c h a n ic s ) . B u t t h e m e t h o d s o f lo g ic a l d e d u c t io n o n t h is le ve l a r e t yp ic a l o n ly fo r a c o n s id e r e d t h e o r y; we h a ve , fo r e xa m p le , t h e \ g e o m e t r ic a l t h in kin g " in t h e g e o m e t r y, t h e \ m e c h a n ic a l t h in kin g " in t h e m e c h a n ic s . Th e fo u r t h le ve l o f t h e fo r m a liz a t io n m a y b e c h a r a c t e r iz e d a s a \formal logical" o n e . It is p e r fo r m e d wh e n t h e m e t h o d s o f t h e in t u it ive lo g ic a l t h in kin g u s e d o n t h e p r e vio u s le ve l 9 1 9 2 On the Formalization of Scienti¯c Theories b e c o m e n o t s a t is fa c t o r y fr o m t h e p o in t o f vie w o f t h e e xa c t n e s s a n d t h e r e lia b ilit y o f t h e s t a t e m e n t s o b t a in e d b y t h e d e d u c t io n . Th e in t u it ive lo g ic a l d e d u c t io n is r e p la c e d o n t h is le ve l b y t h e fo r m a l lo g ic a l o n e . Fo r e xa m p le , t h e p a s s in g o f t h e g e o m e t r y t o t h e fo r t h le ve l wa s p e r fo r m e d in 1 9 -t h c e n t u r y [1 ]. Th e ¯ ft h le ve l o f t h e fo r m a liz a t io n m a y b e c h a r a c t e r iz e d a s a \syntactical" o n e . It is p e r fo r m e d wh e n t h e fo r m a l lo g ic a l d e d u c t io n is r e d u c e d t o t r a n s fo r m a t io n s o f c o m b in a t io n s o f fo r m a l s ym b o ls ( d e ¯ n e d o n ly b y t h e ir fo r m a l s t r u c t u r e ) . S u c h a le ve l is e s s e n t ia l fr o m t h e p o in t o f vie w o f s o m e d ir e c t io n s in t h e m a t h e m a t ic s ( fo r e xa m p le , fo r m a lis m [2 ]) ; it is e s s e n t ia l a ls o fo r a p p lic a t io n s o f t h e c o m p u t e r s c ie n c e t o t h e in ve s t ig a t io n s o f p e c u lia r it ie s o f t h e h u m a n t h in kin g . Th e p r e d ic a t e c a lc u lu s [3 ] g ive s a g e n e r a l m e t h o d fo r p a s s in g t o t h e ¯ ft h le ve l fr o m t h e fo u r t h o n e . S o m e h ig h e r le ve ls o f t h e fo r m a liz a t io n m a y a ls o b e c o n s id e r e d , b u t t h e y a r e ye t n o t im p le m e n t e d , a n d we d o n o t c o n s id e r t h e m h e r e . R eferences 1 . D a vid H ilb e r t . Gr u n d la g e n d e r Ge o m e t r ie , S ie b e n t e A u ° a g e , L e ip z ig u n d B e r lin , 1 9 3 0 . 2 . D . H ilb e r t u n d P . B e r n a ys . Gr u n d la g e n d e r Ma t h e m a t ik I, Zwe it e A u ° a g e , S p r in g e r - V e r la g , B e r lin -H e id e lb e r g -N e w Y o r k, 1 9 6 8 . 3 . H . E n d e r t o n . A Ma t h e m a t ic a l In t r o d u c t io n t o L o g ic , 2 n d e d ., S a n D ie g o , H a r c o u r t , A c a d e m ic P r e s s , 2 0 0 1 .