Three aspects of decidability

A C T A U N I V E R S I T A T I S L O D Z I E N S I S __________________ F O L IA PHILOSQPHICA 7, 1990__________________

Janusz Kaczmarek THREE ASPECTS OF DECID ABILITY

M etam athem atical problems of d e c i d a b i l i t y re c u r in lo g ic in the shape of the q u e s tio n : i s a g iv e n lo g ic a l th eory d e c id a b le or u n d e c id a b le . B a s ic r e s u l t s con cern ing d if f e r e n t m athem atical and l o g ic a l t h e o r ie s were ach ieved m ainly in the t h i r t i e s and the f o u r t ie s of our c e n tu ry . No wonder th a t the n o tio n of d e c i d a b i l i t y i s u s u a lly combined w ith the term inology o f th a t tim e . However, I would suggest th a t p e r c e iv in g a t le a s t th re e d i f f e r e n t p e rio d s in the s tu d ie s on d e c i d a b i l i t y i s f u l l y j u s t i f i e d .

The f i r s t p e rio d c o v e rs the y e a rs t i l l 1930. At th a t time the problem of d e c i d a b i l i t y a cq u ire d some im p ortan ce, m ainly on account of the s tu d ie s connected w ith H i l b e r t 's programme. The second p e rio d f a l l s on the t h i r t i e s and the f o u r t i e s . Then, on the b a s is of v a rio u s approaches, a narrow m athem atical concept of d e c i d a b i l i t y was b u i l t up, which rendered p o s s ib le an e q u a lly p r e c is e d e f i n i t i o n o f d e c i d a b i l i t y . F i n a l l y , in the t h ir d p e rio d th a t s ta r te d about the e a r ly s i x t i e s , th e re appeared p u re ly me­ c h a n ic a l p rocedures fo r s o lv in g v a rio u s problem s, thus s tim u la tin g the s tu d ie s on p r a c t i c a l d e c i d a b i l i t y . The n o tio n of d e c id a b le th e o ry in these th re e p e rio d s w i l l be the b a s ic theme of t h is

p a p e r1.

-1 There i s a g re a t v a r i e t y o f in t e r e s t i n g works concerned w ith r e c u r s iv e fu n c tio n s and tho problems of d e c i d a b i l i t y and unde­ c i d a b i l i t y . The most v a lu a b le a r e , f o r example, A. G r z e g o r ­ c z y k , Z ag ad nienia r o z s t r z y g a ln o á c i, Warszawa 1957; A. T a r- s к í , A. M o s t o w s k i , R. M. R o b i n s o n , U ndecida­ b le T h e o rie s , N o rth -H o lla n d , Amsterdam 1953; 0. V a n D a l e n, Alg o rith m u s and D e c is io n Problem s: a Crash Course in R e cu rsio n Theory, [ i n : } Handbook of P h ilo s o p h ic a l L o g ic , eds 0. M. Gabbay,

1. P e rio d I . The d e c id a b ilit y of a theory was d efin e d in terms of the in fo rm a l i n t u i t i v e n otion of an e f f e c t i v e method. What is an e f f e c t i v e method? I t s paradigm can be found in sim ple and w e ll- -known m athem atical alg o rith m s as, fo r example, E u c l i d 's alg o rith m fo r fin d in g the g re a te s t common d iv is o r of two p o s it iv e in te g e rs n o t - r e la t iv e ly prim e; e f f e c t i v e method i s a method which a llo w s to s o lv e a problem or a c la 'js of problems in a f i n i t e number of steps. A c c o rd in g ly , a g eneral problem (a c la s s of s p e c i f ic q u e s tio n s ) i s d e c id a b le i f th e re e x is ts an e f f e c t i v e method of s o lv in g every q u estio n of th a t c la s s , e .g . g eneral q u e stio n : " i s a g iven num­ ber n p rim e ?" i s d e c id a b le . C onsequently, a theory T i s d e c id a ­ b le i f i t s g e n e ral problem: " i s a form ula v a lid in i t " i s d e c id a ­ b le 2 .

M etam athem atical s tu d ie s advanced by H ilb e r t and h is school b efo re 1930 aimed at p ro vin g the c o n s is te n c y and d e c i d a b i l i t y of the main lo g ic a l and m athem atical th e o r ie s . At th a t time c l a s s i c a l mathem atics was g e n e ra lly claim ed to be not on ly c o n s is te n t but a ls o d e c id a b le . That th e s is became even more c o n v in c in g a f t e r R u s s e ll and Whitehead " P r i n c i p i a Mathema- t i c a " . Such a t t it u d e made the s tu d ie s on d e c i d a b i l i t y focus on new e f f e c t i v e methods and new d e c id a b le t h e o r ie s ; t h e ir r e s u lt s being r e fe r r e d o n ly to m athem atical th e o r ie s or t h e ir fragm ents, e . g . , L . Löwenheim3 proved the d e c i d a b i l i t y of f i r s t - o r d e r monadic p re d ic a te lo g ic (1 9 1 5 ), E . P o s t4 , the d e c i d a b i l i t y of standard t r u th - fu n c tio n a l p r o p o s itio n a l lo g ic (1 9 2 1 ), M. P resb u rg e r^ ; the

F . Guenthner, 1983, v o l. I , pp. 409-478. But a l l of them, however, d eal on ly w ith the f i r s t two p e rio d s of s tu d ie s on d e c id a b ilit y . As f a r as the author knows, some problems of p r a c t i c a l d e c id a b ilit y are d iscu ssed on ly in : M. 0. R a b i n , O e cid ab le T h e o rie s , [in :J Handbook of M athem atical lo g ic , ed. J . B a rw is e , N o rth - H o lla n d , Am­ sterdam 1977.

2

See, e .g . A. G r z e g o r c z y k , op. c i t . j A. T a r ­ s k i , A. M o s t o w s k i , R. M. R o b i - n s o n , op. c i t .

3 L . L ö w e n h e i m , Öber M ö g lic h k e ite n im R e la t iv k a lk ü l, "Mathem atische Annalen“ 1915, v o l. 76, pp. 447-470.

h

E. P o s t , In tr o d u c tio n to a G eneral Theory of Elem entary P r o p o s itio n s , "A m erica l Jo u rn a l of M athem atic" 1921, v o l. 43, pp.

163-185. ,

5 M. P r e s b u r g e r , Uber d ie V o lls t ä n d ig k e it eines gewis­ sen Systems der A rith m e tik genzer Z ahlen , in welchem d ie A d d itio n a ls e in z ig e O peration h e r v o r t r i t t ; [ i n : ] Sprawozdanie z I kongresu matematyków krajów s ło w ia ń s k ic h , Warszawa 1929, pp. 92-101,

d e c i d a b i l i t y of f i r s t - o r d e r number th e o ry w ith a d d itio n but w ith o u t m u lt ip lic a t io n (1 9 2 9 ), T. Skolem6 : the d e c i d a b i l i t y of f i r s t - o r ­ der number th eory w ith m u lt ip lic a t io n but w ith o u t a d d itio n (1 9 3 5 ). Moreover some e f f e c t i v e methods were in v e n te d a s , fo r exam ple, the re d u c tio n to c o n ju n c tiv e normal form, t r u th - t a b le method (indepen­ d e n tly - E. P o s t7 and L . W ittg e n s te in 8), and the methods of p ro ­ vin g the d e c i d a b i l i t y f o r some s p e c if ie d t h e o r ie s . Beyond the lim its of the b a s ic re s e a rc h work were, h ouever, u n d ecid ab le problems and t h e o r ie s , namely those w ith no e f f e c t i v e methods fo r s o lv in g t h e ir g e n e ral problem. At le a s t two reasons can be g ive n fo r t h a t : I ) a f t e r H ilb e r t had realized h is programme, u nd e cid ab le problems were assumed not to belong to m athem atics; 2) the f a i l u r e in the f i e l d of u nd ecid ab le th e o r ie s was to some e x ten t due to u n p re c is e d e f i ­ n it io n of d e c i d a b i l i t y of a th e o ry . As has been s ta te d above, th a t d e f i n i t i o n based on the i n t u i t i v e concept of e f f e c t i v e method. In the second p e rio d the e f f e c t i v e method was more p r e c is e ly d e fin e d , which was connected w ith the in tr o d u c tio n of i t s m athem atical coun­ t e r p a r t : the concept of re c u rs iv e n e s s .

2. P e rio d I I . The second p e rio d belongs to the most p r o l i f i c in the h is t o r y of d e c i d a b i l i t y s tu d ie s , and thus i t can be

a

tre a te d as a w hole. When G o d e l's work was p u b lish e d in 1931, i t became e v id e n t th a t the d e d u c tiv e power of fo rm a liz e d systems i s lim it e d and, c o n s e q u e n tly , not alw ays the r ig h t procedure ( i . e . the one th a t s o lv e s the problem in e v e ry s i t u a t i o n ) , f o r a g ive n problem of a th e o ry can be s e t t le d . Based, on the one hand, on the i n t u i t i v e n o tio n of what i s c a lc u la b le , and, on the o th e r hand, on the e x is t in g a lg o rith m s , s e v e r a l d i f f e r e n t m athem atical d e fin itio n s of re c u rs iv e n e s s were form u lated ( t h a t i s , d e f i n i t i o n s o f r e c u r ­ s iv e f u n c tio n , Gödel in [a] fo r the f i r s t tim e , and of r e c u r s iv e s e t ) , which in consequence made p r e c is e d e f i n i t i o n of d e c i d a b i l i t y

6 T. S k o l e m , Uber e in ig e S a tz fu n k tio n e n in der A rith m e­ t i k , S k r i f t e r U t g i t t av Det Norske Videnskaps-akademi i O slo , I . M a t.- N a tu rv . K la s s e 1930, No. 7, Oslo 1931.

7 E. P o s t , op. c i t .

8 L . W i t t g e n s t e i n , T ra c ta tu s lo g ic o - p h ilo so p h ic u s , Routledge and Kegan P a u l, London 1922.

9 ».

K. G ö d e l , Uber form al u n e n tsch e id b are S ä tz e der P r i n ­ c i p i a M athem atica und verw an d ter Systeme I , "M o n a tsch ri f t f ü r Mat­ hem atik und P h y s ik " 1931, Bd. 38, pp. 173-198.

p o s s ib le . The most n o tab le r e s u l t s o r ig in a te d w ith A. Church, K. G ödel, S . C. K le e n e , J . B. R o sse r, E. P o s t, A. T u rin g , and l a t e r A,H arkov, The must persp icu ou s d e f in it io n of r e c u r s iv e fu n c tio n s (w h ich a t the same time c h a r a c te r iz e s t h e ir c o n s tr u c tio n ) i s foun­ ded on the n o tio n s of e f f e c t i v e minimum, p r im it iv e re c u rs io n * ^ and com position o p e r a tio n s * 1, Namely, i f we c o n s id e r e a s i l y c a lc u la b le fu n c tio n s :

<*) Z (x ) = 0, S (x ) « x ♦ I , Un i ( x j ... xn ) = xx fo r i < n, n = 1, 2...

then a c la s s of re c u rs iv e fu n c tio n s can be d efin ed as the minimal c la s s of fu n c tio n s c o n ta in in g (# ) and clo se d under the o p e ra tio n s of com position, p r im it iv e re c u rs io n and e f f e c t iv e minimum. Making use of t h is o b s e rv a tio n , r e c u rs iv e s e t was d efin ed as a set fo r which th e re e x is ts a re c u rs iv e fu n ctio n c h a r a c t e r is t ic fo r t b is s e t; and d e cid a b le theory - as a theory w ith r e c u rs iv e set of theorems.

12

In 1936 Turing proposed to d e fin e computable fu n c tio n in terms of computing machines he had in ve n te d . Fu n ctio n f is compu­ ta b le i f there can be designed Turing machine fo r i t , such th a t i t may be capable of p r in t in g succeeding valu es of th a t fu n c tio n on the tap e. In d e p e n d e n tly, E. Post made a s im ila r a n a ly s is . Next p ro p o s itio n concerning A - d e fin a b le fu n c tio n s was in trod u ced by Church and K leene; i t was based on C h u rch 's A - c a l c u l i 1 } , where

The o p e ra tio n of e f f e c t iv e minimum. The o p e ra tio n of m in i­ mum lead s from a fu n c tio n g (y , x., . . . . x „ ) of n ♦ I arguments to a ru n c tio n f ( x 1t xn) of n arguments, whose valu e f o r given x. •••• *n 1S the le a s t va lu e pf y , i f one such e x is t s , fo r which

* i > •••i ~ 0 and which is undefined i f no such у e x is t s . I f fo r given x. , xn th e re alw ays e x is ts the le a s t valu e of y, then the o p e ra tio n of minimum is c a lle d e f f e c t i v e . The op era­ tio n of p r im it iv e re c u rs io n . This o p e ra tio n a s s o c ia te s w ith the rtľ n n h ? t a l ,u n c tlo n i\ f ( *1> xn) and g ( x , ... xn<2) the fun-F ÍČ on t*(x l ... where: h (0, x ,, . , , , x „ ) = f ( x . . . . Xn),

( +n l - *1» *n) = 9 (k , h (k , x ,, . ! . , xn ) ... xn ) l ^e e * e -9- A. G r z e g o r c z y k , op. c i t ,

A. T u r i n g , On Computable Numbers, w ith an a p p lic a tio n to the Entscheidungsproblero, "Pro c ee d in g s London M athem atical So­ ciety 1936/1937, s e r . 2, v o l. 42, pp. 230-265.

к A ' .,C h u r c h, An tln so lva b le Problem of Elem entary Number Theory, "Am erican Jo u rn a l of M athem atic" 1936, v o l. 50, pp!

due to л - o p erato r producing f u n c tio n a l sym bols, the consequent no­ t a t io n is u n i f i e d 14. Also o th er d i f f e r e n t aproaches were t r i e d l a ­ t e r , b rin g in g a lto g e th e r v a rio u s , more p r e c is e d e f in it io n s of the i n t u i t i v e n o tio n of c a l c u l a b i l i t y . The im p ortan t f a c t , however, is th a t in a l l those aproaches the same c la s s of r e c u r s iv e fu n c tio n s was d e fin e d s in c e :

1) The c la s s of r e c u r s iv e fu n c tio n s i s e q u iv a le n t to the c la s s of A - d e fin a b le f u n c t io n s 15.

2) The c la s s of computable fu n c tio n s i s e q u iv a le n t to the class of А - d e fin a b le fu n c tio n s 16.

T h is f a c t made Church and Turing put forw ard a h y p o th e sis that the i n t u i t i v e n o tio n of what i s c a lc u la b le has i t s p r e c is e mathe­ m a tic a l c o u n te rp a rt. That h yp o th e sis c a lle d C h u rch 's T h e s is , Tu­ r i n g 's H y p o th e s is, or the most r i g h t l y , Church-Turing Hypothesis, can have m an ifo ld form es. L e t us p re se n t two of them:

H I) E ve ry r e c u r s iv e fu n c tio n i s e f f e c t i v e l y c a lc u la b le .

H2) A lg o rith m ic p ro cesses in the i n t u i t i v e sense can be r e a liz e d by means of Turing m achines.

Church-Turing H yp o th e sis i s not proved. V a rio u s approaches to what i s c a lc u la b le , however, make us b o liv e i t i s p la u s ib le ; when i t s v a l i d i t y i s assumed, the u n d e c id a b ilit y o f , fo r in s ta n c e , p r e d ic a te c a l c u l i or of the h a lt in g problem can be showed.

Not o n ly d e fin in g d e c i d a b i l i t y in terms of m athem atics but a ls o the f a c t o f surmounting the d i f f i c u l t i e s connected w ith the pos­ s i b l e r e a liz a t io n of H ilb e r t programme r e s u lte d in v a rio u s c o n c lu ­ s io n s con cern ing the u n d e c id a b ilit y of the main m athem atical and lo g ic a l t h e o r ie s . The b est known r e s u l t s (p roved in 1936) are as fo llo w s :

14 "

л - d e fin a b le fu n c tio n can be d e te rm in e d 'a s fo llo w s : fu n c tio n F i s c a lle d A - d e fm a b le i f th e re e x is t s a form ula £ such t h a t , i f F(m ) * r and jd end _£ the form ulas corresp on d in g in t h is c a l c u l i to the p o s it iv e in te g e rs m and r , then F(m ) conv r , where "c o n v ” i s a r e l a t i o n between form ulas F(m ) and r i f f the form ula r can be d e riv e d from £(m ) by m eans.of a p p ro p ria te op era­ t io n s in tro d u ced in x - c a l c u l i and c a lle d c o n v e rs io n (most e x a c t ly : any f i n i t e sequence of these o p e ra tio n s i s c a lle d a con­ v e r s io n ) .

15 A. C h u r c h , o p . c i t . *6 A. T u r i n g , o p . c i t .

3) F ir s t - o r d e r p r e d ic a te lo g ic i s u n d e c id a b le 17. 18

4) Peano's a r ith m e tic i s u ndecidable

and so are f ir s t - o r d e r th e o r ie s of groups, r in g s , f i e l d s and la t - 19

t i c e s . Each of those cases employs th a t th e re i s no e f f e c t i v e method to decide whether any given form ula of a th eory i s v a lid or n o t. In terms of d e c id a b ilit y the s e t of theorems of a given th e o ry i s s a id t.o be r e c u r s iv e . I t becomes e v id e n t th a t i f we a d d it io n a lly in tro d u c e the n o tio n of r e c u r s iv e ly enumerable s e t as a s e t of v a lu es of a r e c u r s iv e fu n c tio n , then G ö d e l's F i r s t Theorem can be form u lated as fo llo w s :

5) The s e t of Gödel numbers of a r it h m e t ic a l theorems i s r e c u r ­ s i v e l y enumerable but is not r e c u r s iv e .

The thorough s tu d ie s on the d e c i d a b i l i t y problems based on the n o tio n of r e c u rs iv e n e s s ( t h i s b r i e f p re s e n ta tio n does not even mention a l l the s i g n i f i c a n t r e s u l t s ) d is c lo s e t h e ir s i m i l a r i t y to computer p r a c t ic e . On the one hand, the models of m athem atical machines c re a te d by Turing and Post (T u rin g machine and Post ma­ c h in e are e q u iv a le n t) are not in f a c t mechanisms but m athem atical con cep ts. Speaking p r e c is e ly , they are d e d u ctive system s: by means of form al tra n sfo rm a tio n made in accordance w ith the r u le s given in advance, they form new sequences of symbols out of the symbol sequences g iven in the in p u t. On the o th e r hand, however, i t is e v id e n t th a t today every r e a l l y e x is t in g computer can be reduced to Turing machine. From the t h e o r e t ic a l p o in t of vie w , Turing ma­ c h in e , and hence a ls o e v e ry computer can s o lv e any computable problem. C onsequently, the problems of d e c id a b le th e o r ie s can be reduced to some a p p ro p ria te computer p ro ced u res. Are the procedures th a t s o lv e the problems of d e c id a b le th e o r ie s f e a s ib le fo r compu­ t e r ? Th is q u estio n was of s p e c ia l a tt e n t io n in the t h ir d p e rio d .

3. P e rio d I I I . From what has been s ta te d above too h asty a co n c lu sio n can be in fe r r e d t h a t , as regard s the d e c id a b le th e o ry ,

A. C h u r c h , A Note on the Entscheidungsproblem , "The Jo u rn a l of Sym bolic L o g ic " 1936, v o l. I , pp. 40-41; C o r r e c tio n , ib i­ dem, pp. 101-102.

I Q

Ibidem . Church ob tain ed t h is r e s u l t having assumed C hurchi -Turing h yp o th e sis and c o n s is te n c y of a r it h m e t ic a l system .

19

the q u estio n whether a form ula is v a l i d c r e a te s a t r i v i a l problem. However, t h is i s not the case s io c e d e c id a b le proced ures m a n ifest e v id e n t com putational com p lex ity as, fo r example, d e c id a b le theory of a r ith m e tic s w ith a d d itio n but w ith o u t m u lt ip lic a t io n . In 1974 F is c h e r and R a b in20 showed th a t in the case of elem entary th eory of a d d itio n , fo r every d e ciU a b le p roced ure, _' th e re can be s in g le d_{л П} out a sentence of a le n g th n fo r which g iven procedure needs 2 step s in order to p ro v id e the answer. L e t us n o tic e th a t computa­ tio n in more than 22 step s is im p o ssib le ( i . e . , we sa y: i t is not p r a c t i c a l d e c i d a b i l i t y ) . S im ila r r e s u lt s were ach ieved in the theory o f lin e a r - o r d e r and the second-order weak theory w ith one s u c c e s o r21. Thus, what should be in e v it a b ly d e fin e d a t t h is mo­ ment, i s such a n o tio n of p r a c t i c a l d e c i d a b i l i t y , th a t would em­ brace the com putational com p lex ity of the p ro ce d u re s. T h e re fo re , i t is accepted th a t i f a fu n c tio n i s p r a c t i c a l l y c a lc u la b le then i t s com p u tation al com p lex ity is determ ined by the f a c t th a t the number of step s n ece ssa ry fo r producing the answer grows p o lin o m ia lly depending on to the le n g th of a in p u t word. C le a r y , i f t h is r e l a ­ tio n is ex p o n e n tia l the due fu n c tio n i s not com putable.

The s tu d ie s of the t h ir d p e rio d are not com pleted, t h e r e f o r e , i t is d i f f i c u l t to f o r e t e l l what r e s u l t s w i l l be o b ta in e d . However, i t is p o s s ib le to s p e c ify i t s o b je c t iv e : to c o n s tru c t new, i n t e r ­ e s t in g , p r a c t i c a l l y d e c id a b le t h e o r ie s .

4. C o n c lu s io n s . Each of the th re e p e rio d s has e s s e n tia lly the same n o tio n of d e c id a b le th e o ry : a theory is d e c id a b le i f a method which i s claimed tu be e f f e c t i v e s e t t l e s whether a form ula is v a l i d . Whereas what makes them vary i s caused by the f a c t , th a t they c o n c e n tra te on d i f f e r e n t problems con cern ing d e c i d a b i l i t y ; in the f i r s t , " i n t u i t i v e " p e rio d the s t r e s s was put on the d e c id a ­ b i l i t y of v a rio u s t h e o r ie s : the second m athem atical one managed to prove many elem entary th e o rie s to be u nd e cid ab le and b u i l t up a h ie r a rc h y of degrees of u n d e c id a b ilit y ; the t h ir d p e rio d , on the oth er hand, was marked by computable p r a c t ic e s and re s to re d d e c id a ­ b le th e o r ie s but from the p o in t of view of p r a c t i c a l l y r e a liz e d p ro c e d u re s .

20

J . M. F i s c h e r , M. 0. R a b i n , Super E x p o n e n tia l Com plexity of P r e s b u r g e r's A r it h m e tic , "SIAM AMS P ro c e e d in g s " 1974, No. 7, pp. 27-41.

In s p it e of the f a c t th a t the s tu d ie s on d e c id a b le th e o rie s are s t i l l making p ro g re s s , I th in k two t a c ts are worth m entioning:

1 °. The range of the problems connected w ith d e c i d a b i l i t y was s u c c e s s iv e ly reduced by every next p e rio d . I f the d e n o ta tio n of the concept of d e c id a b le theory (problem ) i s r e fe r e d to us D j, О ц , °j i i > fo llo w in g in c lu s io n is tru e :

° I 3 D1I 3 D1 I I

Les us, however, s tr e s s the p e c u la r it y of th a t in c lu s io n : Church-Turing Thesis s ta t e s the e q u iva le n ce between i n t u i t i v e c a l c u l a b i l i t y and m athem atical r e c u rs iv e n e s s , which cannot be en­ t i r e l y proved (alth o u g h i t i s obvious th a t every r e c u r s iv e fun c­ tio n is i n t u i t i v e l y C a lc u la b le ). In order to r e je c t the t h e s is , th e re must be p ointed out an i n t u i t i v e l y c a lc u la b le fu n c tio n which is a t the same time not r e c u r s iv e . The above reasoning d e a ls n atu ­ r a l l y w ith the concept of d e c id a b ilit y , and t h is f a c t is the source of an unexpected problem: we are not able to s in g le out such an element a, th a t a e Dj and a ť U j j , which would prove th a t Dj is in f a c t a g re a te r c la s s (a cc o rd in g to Church-Turing Th esis no such an element should be form ed). C la ss Dj j, on the o th er hand,

is e s s e n t ia lly g re a te r then c la s s O j j j i which is obviuus s in ce the s tu d ie s were lim ite d o n ly to p r a c t i c a l l y d e c id a b le th e o r ie s . H ere, however, a s e n s ib le p r a c t i c a l l y d e cid a b le theory can be h a rd ly appointed.

2 °. The problems of d e c id a b ilit y and the p r a c tic e are (e n ­ t i r e l y ) analogous; the former stem from the s tu d ie s on c a lc u la ­ tin g a lg o rith m s: they were combined w ith computer p r a c tic e in the second p e rio d , and d e a lt w ith the co n crete d e cid a b le th e o rie s and s o lv in g procedures in P e rio d I I I . The q u estio n can be put i f th ia analogy is r e a l l y c lo s e ? For the time being the answer is n e g a ti­ ve. The r e s u lt s of the s tu d ie s on p r a c t ic a l d e c id a b ilit y show th a t a lg o rith m s can be h a rd ly expected to be p r a c t i c a l l y r e a liz e d s in c e s o lv in g procedures are of too high com putational co m p lex ity. However, some alg o rith m s fo r d ata,fro m a f i n i t e s e t can be r e a l i ­ zed in p r a c t ic e . Th is i s an im portant f a c t in the s tu d ie s of au­ tom atic theorem p rovin g s in c e the p o s s i b i l i t i e s to form theorem,

p ro vin g procedures ( f o r a form ula of U n i t e d le n g th ) are not ex­ clu d ed .

U n iv e r s it y of Łódź Poland

Janusz Kaczmarek

TRZY POJĘCIA ROZSTRZYGALNOŚCI

W a r ty k u le dokonano k r ó t k i e j a n a liz y p o ję c ia r o z s trz y g a ln o ś c i w trz e c h k o le jn y c h okresach j e j rozw oju.

P ie rw sz y okres obejmuje la t a przed rokiem 1930, w k tó ry c h p ro ­ blemy ro z s trz y g a ln o ś c i u z y sk a ły w ła ściw e znaczen ie głów nie za s p ra ­ wą badaó związanych z programem H ilb e r t a . Okres d rug i obejmuje l a ­ ta t r z y d z ie s t e 1 c z t e r d z ie s t e . W yk o rzystu jąc rozm aite p o d e jś c ia , wypracowano wówczas ś c i s ł e , matematyczne p o ję c ie o b l i c z a l n o ś c i , co u m o ż liw iło p r z y ję c ie równie p r e c y z y jn e j d e f i n i c j i r o z s t r z y g a ln o ś c i. Z k o le i okres t r z e c i rozpoczyna s ię m niej w ię c e j od początku l a t s z e ś ć d z ie s ią ty c h , k ied y to w związku z procedurami możliwymi do realn eg o u rz e c z y w is tn ie n ia p o ja w iła s ię r e f l e k s j a nad p rak tycz n ą r o z s t r z y g a ln o ś c ią .