ANOTHER NOTION OF RECURSIVENESS BY STELLA MEI-YEE YEUNG B. A., Mills College, California, U. S. A., 1971 A THESIS SUBMITTED IN PARTIAL FULFILLMENT OF THE REQUIREMENTS FOR THE DEGREE OF MASTER OF ARTS in the Department of MATHEMATICS We accept this thesis as conforming to the required standard THE UNIVERSITY OF BRITISH COLUMBIA September, 1973 I n p r e s e n t i n g t h i s t h e s i s i n p a r t i a l f u l f i l m e n t o f t h e r e q u i r e m e n t s f o r a n a d v a n c e d d e g r e e a t t h e U n i v e r s i t y o f B r i t i s h C o l u m b i a , I a g r e e t h a t t h e L i b r a r y s h a l l make i t f r e e l y a v a i l a b l e f o r r e f e r e n c e a n d s t u d y . I f u r t h e r a g r e e t h a t p e r m i s s i o n f o r e x t e n s i v e c o p y i n g o f t h i s t h e s i s f o r s c h o l a r l y p u r p o s e s may b e g r a n t e d b y t h e H e a d o f my D e p a r t m e n t o r b y h i s r e p r e s e n t a t i v e s . I t i s u n d e r s t o o d t h a t c o p y i n g o r p u b l i c a t i o n o f t h i s t h e s i s f o r f i n a n c i a l g a i n s h a l l n o t b e a l l o w e d w i t h o u t my w r i t t e n p e r m i s s i o n . D e p a r t m e n t The U n i v e r s i t y o f B r i t i s h C o l u m b i a V a n c o u v e r 8, C a n a d a D a t e i i Abstract The notion of recursiveness is treated in a model-theoretical way by using a particular instance of Kreisel's definition of 'invariant definability' . Naming the chosen notion 'finite describability', a number of basic definitions and properties are defined and proved. As one would expect, these properties coincide with the ones for recursion theory The equivalences of finite describability and recursiveness bring model theory and recursion theory slighty together. i i i Table of Contents Page Chapter I Finitely Describable Sets and Functions 3 1.1 Definitions • .. 3 1.2 Basic Properties 7 Chapter II Finitely Enumerable Sets 11 II. 1 Definition 11 II.2 Properties 11 Chapter III Some Non-Finitely Describable Sets 19 Chapter IV The Relation between Finite Describability and Recursiveness 30 Bibliography 39 iv Acknowledgement First of a l l , I would like to thank my supervisor Dr. Andrew Adler for his suggestion of the topic of this thesis and also for his constant guidance and help throughout the work. I would also like to thank Dr. Timothy Cramer for taking interest in reading the thesis. The financial support from the University of British Columbia is greatly appreciated. Introduction The important notions of 'recursive function' and 'recursive predicate' have been defined in many different ways. Among the more impor-tant ones are Herbrand-GSdel recursiveness, u-recursiveness, computability by turing machine, and computability by Markov algorithm. A l l these notions have so far turned out to be equivalent. None of the definitions are, however, natural, from a model-theoretic point of view. In order to help in bringing recursion theory and model theory together, Kreisel [2] in 1963 defined a class of concepts of 'Invariant definability' and pointed out that this notion, at least for the natural numbers, could be traced back to Godel's result of 1931. Since 1963, a few papers have been written exploring some notions of Invariant definability . Lambert, Lacombe, Moschavakis and Fraisse- have obtained some results that appear to show that the notions of 'Invariant definability' can be useful tools in recursive theory and its generalizations. D. Lacombe in [3] defined various notions of recursiveness and relative recursiveness on algebraic structures, and some of the more interes-ting notions are singled out and various equivalences are given. W. H. Lambert Jr. in [4] defined a notion of 'Schematic definability' and proved a number of results. He showed for instance that the set of 'schematic definable1 functions has the properties that one might reasonably expect, and that certain devices for ordinary recursion theory, like defini-tion by cases, carry over. Y. N. Moschavakis in [5] looked at invariant - 2 -definability over arbitrary structures. One loses a number of the results of ordinary recursion theory in his process of generalization. In this thesis, we define a particular instance of 'Invariant definability' which we call 'finite describability'., and we examine closely the elementary properties of this notion. Chapter I consists of the basic definitions and proofs that the notion of finite describability has the expected elementary properties. In Chapter II, the notion of 'finite enumerability' is studied. This notion is intended to be a formulation in our setting of the ordinary notion of recursive enumerability. The main result of Chapter II is that i f a set and its complement are finitely enumerable, the set is finitely describable. The most interesting result of Chapter III is an analogue of Godel's result on the undecidability of number theory. It is proved in this chapter that the set of theorems of the predicate calculus is not finitely describable. A long construction shows that this set i s , however, finitely enumerable. Finally, Chapter IV examines the relation between 'finite describability' and ' recursiveness'. It is proved here that on reasonably well-behaved structures, the two concepts coincide . The notion of finite describability, like other versions of invariant definability, provides a model-theoretic setting for recursion theory. Also, one can avoid almost completely such devices as arithmetiza-tion of syntax (Gbdel numbering). For most of the elementary results, i t is clear how to proceed toward a proof, though some technical difficulties do at times arise. - 3 CHAPTER I FINITELY DESCRIBABLE SETS AND FUNCTIONS I.I Definitions I.1.1 Small Structures Let Ly be a first-order language with equality. We will suppose that L^ has only a finite number of constant symbols, function symbols, or predicates symbols. Let W be an I^-structure. Let |w| be the underlying set of the structure W. For any variable-free term a of 1^ , let a^ be the interpretation of a in W. W is said to be small i f every element of |w| is of the form a^ for some term a of L^ . In what follows, the letter W always denotes a small structure. The word 'term' always means 'variable-free term' . 1.1.2 The Theory T y Let be the theory with the following axioms : (i) a = b, for a l l pairs (a,b) of terms for which the sentence a = b is true in W . (ii) ~] (a = b) , for a l l pairs (a,b) of terms for which the sentence a = b is false in W . (i i i ) P(a^,...,an), for a l l predicate symbols P of L^ and a l l tuples (a^,...,an) of terms for which P(a^,...,an) is true in W. _ 4 -(iv) 1 P(a^,...,a n), for a l l predicate symbols P of and a l l tuples (a^,...,an) of terms for which P(a^,...,an) is false in W. 1.1.3 Let T be a consistent extension of T^, and let M be a model of T. For any term a of L^, let a^ be the interpretation of a in M. Let |w^| be the set of a l l a^ as a ranges over the terms of L^ . For any term a of L^ , let " K ^ ) = • First we show that is well-defined, that is we show that i f a^ = b^ , -then a^ = b^ , But i f a^ = by , a = b is true in W . Hence a = b is an axiom of and so a^ = b^ . Since every element of |w| is of the form a^ for some a , (J) maps |w| onto |w"M| . Let f be a function symbol of Iv. , and let a 1 ,...,a be elements of |w| . Since f (a ,---,a ) = [f (a.. ,... ,a ) ] >fM(a, >->*>a ) T l . T I "TI T t belongs to JW^ I . So the set |W^| inherits a natural L^ structure WM by restriction from M . We have then : Lemma : $ is an L^-isomorphism of W onto W^ . Proof : With the above, i t remains only to verify that is one-to-one and is an L^-morphism. To show that is one-to-one, let a^ and b^ be distinct elements of |w| . Then a = b is false in W , and so 1 (a = b) is an axiom of T^ . Hence we have a^ £ b^ . Let f be a function symbol of 1^ , > and let a^ = (a.. ,...,a ) \j "w be a tuple of elements of W . Then (fT7(a„)) = d>(f(a))tT = (f(a))„ = - 5 -= = ^ M ^ ^ - ^ W ^ ' ^ e t ^ be a predicate symbol of L^ , and let a^ be a tuple from W . Then P^(a^ ) holds in W i f f P(a) is an axiom of T^ i f f ^(^ J J) holds in . Since a^ = (a^ ), so this completes the proof that is an L^-morphism • So i f M is a model of an extension of T , M has an w L^-substructure which is in a natural way L^-isomorphic to W . So we may, without loss of generality, assume that every model M of an extension of T^ has W as an L^-substructure. 1.1.4 Finitely describable subsets of Wn, n > 1 . Let SCW 1 1. S is finitely describable i f there exists a finite extension T of T , with an n-ary predicate symbol R such that : w (i) For any model M of T, 0 Wn•= S . (ii) For any sentence Y of L^ , i f Y is true in a l l models of T, then Y is true in W . If the situation described above holds, we say that T with predicate symbol R describes S . Using the completeness theorem for the predicate calculus, one can give an equivalent proof-theoretic definition of finitely describable set. Before doing so, we make a simplifying convention. Let R(x) be a formula, and let. t_ be in Wn . Since _t is not an n-tuple of terms, the expression T I— R(t) does not make sense. So let a be an n-tuple of terms of L^ such that _t = a^ . Let T I — R(t) be an abbreviation for - 6 -T I— R(a) . If jt = a^ - h^ . , then a = b_ is an axiom of , hence a theorem of T . So T I— R(a) i f f T|—R(b_), and so our abbreviation is permissible . s e w 1 1 is finitely describable i f there exists a finite extension T of , with an n-ary predicate symbol R, such that (i) 1 For any Jt in Wn, either T|—R(t) or T h- "| R(t), and . ft e Wn | T |— R(t)} = S . (ii) ' For any sentence Y of 1^ , i f T |— Y, then Y is true in W. 1.1.5 Finitely Describable total function from W to n, m >_ i A total function f : W11 —> W™ is finitely describable if there exists a finite extension T of T^, with an n-ary function symbol F such that : (i) For any model M of T, | w" = f. (ii) For any sentence Y of , i f Y is true in a l l models of T, then Y is true in W . By the completeness theorem, conditions (i) and (ii) can be replaced by : (i)' For any t in «" , T|—F(_t) = f(t). Here again F(_t) = f(t) is not a sentence, since for jt in Wn, jt and so f(t) are not terms. Let a be a tuple of terms of L^ such that = jt . Let jb be a tuple of terms of L such that K = f(t) • - 7 -Then T I — F(t) = f(t) is an abbreviation for T I— F(a) = b . By an argument essentially identical with the one in 1.1.4, this abbreviation is permissable. ( i i ) 1 For any sentence Y of , i f T I— Y, then Y is true in W. 1.2 Basic Properties 1.2.1 Theorem. If SCW" is finitely describable, then S = S' is also finitely describable ". Proof : Since S C is finitely describable, there exists a finite extension T of T »' with an n-ary predicate symbol R such that (i) For any _t in W11 , either T |— R(t) or T |— ~] R(t) , and {_t e W11 | T|—• R(t)} = S . (ii) For any sentence Y of , i f Th- Y, then Y is true in W . Let T' be T . together with the additional axiom (R1 (X) <—>~]R(x)), where R' is a new n-ary predicate symbol. (i) For any t_ in either T |— R(t) or T I IR(t). The additional axiom of T' implies that either T' I "1 R' (t_) or T'( R' (_t) . Futhermore, {it e W11 | T*h— R ' ( 0 ) = '{t e w" | T| 1 R(t_) }• = S' . (ii) Let Y be a sentence of . If T'J— Y, then T f— Y which implies that Y is true in W . Hence S'cZ Wn is finitely describable. 1.2.2 Lemma : Let T^ , T2 be theories such that L^ , 0 L^ = 1^ . Suppose for any sentence Y of L , T, |— Y or T„| Y implies that - 8 -Y is true in W. Then U T |-—Y implies that Y is true in W . Proof : Let T be the set of a l l sentences of L^ which are true in W. Let r i = T u r and I"- = T 2 \J V . Then 1^ U T2 = r U U r U T 2 = T U T 2 U r . Rob We want to show that U is consistent. By the Craig-inson Joint-Consistency Lemma ([7], p. 79), i f (J is inconsistent, then there exists a sentence Y of L^ such that T^ U r I — Y and T 2 U T |— ~|Y. By the definition of T and the assumed properties of T^ and T 2, this implies that Y is true in W and 1Y is true in W which is impossible. Hence U T 2 is consistent. For any sentence Y of 1^, i f T 1 U T 2 f — Y» t h e n U T 2 V r I— Y. Since U U T is consistent and every true formula of is a consequence of T^ U T 2 U T , Y is true in W . 1.2.3 Theorem. If S^ S 2C W11 are finitely describable, then S 1 H S 2 is also finitely describable. Proof : Since S^ , S 2 C W11 are finitely describable, there exist finite extensions T^, T 2 of T w > with n-ary predicate symbol R.^, R2 respectively such that : (i) for any jt in W11, either T 1 l — R^t) or 1^—IR^t), and either T 2J R 2(t) or T21 l ^ ^ ' Furthermore, { t e Wn | T 1j R1(jt) } = S 1 and { t/e Wn | T 2 |— R 2(t) } = S^ (ii) For any sentence Y of 1^, i f T^|— Y or T 2 f — Y, then Y is true in W . T^ and T 2 can be chosen in such a way that L^ , ' H L^ , = L^. - 9 -Let T be U T 2 together with the additional axiom (R(x) <—> R^(x) A R 2(x)), where R is a new n-ary predicate symbol . (i) For any Jt in Wn , by the additional axiom in T and the properties of T and T 2, Tj R(t) or T| 1 R(t). Also ( t e w " | T h—R(t)} = { t. e W*1 | T . J— R^jt) A T 2 J R 2(t) } = S± fl S 2 < (ii) For any sentence Y of L^, i f T I—- Y, then by Lemma 1.2.2, Y is true in W . Hence fi S^C W11 is finitely describable. From theorems 1.2.1 and 1.2.3, i t follows that any Boolean combination of finitely describable sets is finitely describable. 1.2.4 Theorem (Substitution). Let P(x^, x^) be a finitely descri-bable n-ary predicate, and f^, f • be k-ary finitely describable functions. Then the predicate Q(y^» •••> y^) which holds i f f P(f^(y^, y^), ^n(y^» •••> y^)) holds is a finitely describable k-ary predicate. Proof : Let Tp be a finite extension of T^, with an n-ary predicate symbol Rp that describes P. Let T^ , ..., T^ be finite extensions of 1 n TtT, with function symbols F, , F that describe f.. , ...» f W 1 n 1 n respectively. Theories T^, T^ can be chosen in such a way that 1 n their languages have only L^ in common. Let T be T p U T f U U T f together with the additional 1 n - 10 -axiom (R(y_) <—> RpC^^Cx) > •••> F (y_))) where R is a new k-ary predicate symbol. k It is tri v i a l to see that for any t_ in W , either T |— R(t) or T| ~lR(t). Furthermore, T|—R(t) i f f P(f_),..., f (t)) holds — — I n — i f f Q(t) holds. T p U T u . • • • U T U T , where T is the set of 1 n a l l true sentences of is consistent by lemma 1.2.2. So for any model M of I p U T f U ... u T f U T , a model. M* of T U r can be 1 n constructed such that M' is M except for the additional interpretation R^ (t) <—> Rp (F, (t) , . . . , F (t)) for a l l k tuples. Therefore T M M °M is consistent and hence for a l l sentences Y of L^, i f T 1— Y, then Y is true in W. So Q(y1, y.) is finitely describable. This chapter included the most obvious basic properties of 'finite describability' that one would expect to have in connection with the notion of recursiveness. - 11 -CHAPTER II FINITELY ENUMERABLE SETS 11.1 Definition S C Wn is finitely enumerable i f f there exists a finitely describable predicate P(x^, x^ > y^, y^) such that (Y;L> • • • » Y N ) is in S i f f 3 x^ x ^ P ^ , ..., x^ ., y ^ yn>)« 11.2 Properties : II.2.1 Theorem. If S C Wn is finitely describable, then S is finitely enumerable. Proof : Since S is finitely describable, there exists a finite extension T of T , with an n-ary predicate symbol R such that (i) For any _t w in Wn, either T|— R(0 or T f — lR(t) and {_t e Wn | T| R(t)} - S. (ii) For any sentence Y of 1^ , i f T |—- Y , then Y is true in W . Let P be an (1 + n)-ary predicate such that P(x, y^, y ) holds i f f (y^, y^) , is in S . Let T^ be T together with the additional axiom (R^(x, y ^ y^) <—> R(y^, Y N ) ) > where Rp is a new (1 + n)-ary predicate symbol. ' (i) For ary (u,Jt) in W1+n , either T| R(t) or T| ~]R(t) . The additional axiom of T implies that T I R (u,t) or T I 1 R (u,t). P p' P ~ Pl P -Also, the set {(u,t) e W1+n | T |—• R (u,t)} = {t e Wn | T|—R(t)} = S, - 12 -i.e. P(u,t) holds i f f T |— R (u,t). (ii) For any model M of T u P , where r is the set of a l l sentences of which are true in W, a corresponding model M' can be constructed such that M' is M except for the additional interpretation R (u,_t) <—> R^OO for a l l (l+n)-tuples. Then T u r is consistent P M i M P and hence i f T I Y, then Y is true in W . So P is finitely P describable. By the definition of P, P(x, y^, ..., y R) holds i f f (y^, . .., is in S. This implies that (y^ » •••» Yn) is i - n S i f f 3 X P(x> ••• Since P has proved to be finitely describable, therefore S is finitely enumerable. For the next result, we need to extend the notion of finitely describable function a l i t t l e bit. Let W . Then f can be uniquely expressed as f_ = (f^, ...» f r) , where each f^ , 1 <_ i <_ n is a function from to W . f_ is said to be finitely describable i f each of the f. i s . 1 II. 2.2 Theorem. If SCw" and S ^ , then S is finitely enumerable i f f i t is the range of a finitely describable function. Proof : -> If SCW 1 1 is finitely enumerable, then there exists a finitely describable (k+n)-ary predicate P(x,y_) such that y_ in S i f f 3 x . P(jx,y_) . Since S ^ <|> , choose a fixed w in S . Let f be a function of Wk+n into Wn defined as jf(x,y_) = w i f ~| P(x,jy_) and f_(x,x) = X i f P(x,jy_) . Therefore S is the range of f_ . - 13 -To show that f_ is finitely describable, we are going to build up a theory T^ which finitely describes f_ . Let the theory T^ with the predicate symbol R describes P . Let T,, be T together with P I P the following additional axioms : (lR p(x , x ) —> F±(x,_) = w±) , l < i < n ' and (Rp(x»Z) —> F±(*>l) = y ±) » 1 1 1 1 n where F^, F r are new n-ary function symbols, and the w^ are the components of w . Express _F = •••> ^ n) • k+n (i) For ary (jt,u) in W , either Tp|—• R (_>Ji) o r T -| 1R (t,u) . The additional axioms of T f imply that Tf| ;F(jL>2i)=w_ or T^ | Z(JL»_i) = IL • BY t n e definition and the finitely describability of P , i t turns out that T f|— _(t.,u) = f.(jt,u) . (ii) For any model M of T U T , where T is the set of a l l P true sentences of 1^ , a model . M' of U T can be constructed such that M 1 is M except for R (t,u) —> F w, (t) = u.. and 1 R (t,u) P M - - ~~ P M ~ ~ — > I M ' ^ = f o r a 1 1 ( k + n ) - t u P l e s (t,»u.) • S o T f U T is consistent and hence T^ \— Y implies Y is true in W . Therefore f_ is finitely describable . k <= If S = f^ W ) for some finitely describable function _f of into W . Let T^ be a theory with function symbol F^, F^ that describes f_ . Let P be a (k+n)-ary predicate such that P(x,y_) holds i f f f/x) = y_ • So y_ in S i f f 3xp0i>y_) . To show that P - 14 -is finitely describable, let be together with, the additional axioms ; (Rp(2L>i) < — > F(x) = y_) , where is a new (k+n)-ary predicate symbol. k+n (i) It is t r i v i a l to see that for ary (_t,u) in W , either T I R (t,u) or T | ~1R (t,u) and I | R (t,u) i f f f(t) = u i f f p1 p —'— p' p —'— p p — — — P(_t,u) holds. (ii) For any model M of T^ U P , where r is the set of a l l sentences of true in W , a model M1 of U T can be constructed such that M' is M except for R (t,u) <—> F..(t) = ir, . So T \J T • PM. - -^M p is consistent and hence for any sentence Y of , T |— Y implies Y is true in W . Hence P is finitely describable. Therefore y_ in S i f f 3 jx(f_(jx) = y_) i f f 32£ P(2i»Z) > s o S is finitely enumerable. II. 2.3 Theorem. If S CW™ and W^ N^ S = S' are both finitely enumerable, then S is finitely describable. Proof : Since S is finitely enumerable, there exists a finitely describable (k+n)-ary predicate A such that x e S i f f 3 2. A(2i>y_) • Let the theory T with predicate symbol P finitely describe A . Similary, S' = Wn\ S is finitely enumerable, so there exists a finitely describable (q+n)-ary predicate B such that x £ S' i f f 3 i B(x,z) . Let T with predicate symbol Q finitely describes B . - 15 -Construct the theory T* with new predicate symbol P* by adding to T the following axioms : A (a) P * ( r ^ , . .., r m ) <—> P ( r ^ , r^) for a l l m-tuples (r^, r^) where r^ = a j ^ ) a n ^ J (1) .£ J (2) Ji ••• 5. J (m) > an a n a r e the constant symbols of L^ . • (b) (P*(u , ..., u ) <-> P ( U l , u )) —> (P*(Fu , ... .,Tfu ) <-> ± m l m 1 m P(TTU.., .... iru )) for a l l m! permutations of 1. .... m . 1 m (c) (P*(x , u,, .. . , u ) <-> P(x , u , . .. , u ) A -.-A 1 /. m 1 JL m P*(x k, u 2, u m) < _> F(-\> u 2 » u m ) ) — > ( p * ( f i ( x 1 , ••• , x ^ , u 2, ..., u m) <—> P(f^(x^, . . . , x j t ^ > u 2, ..., u )) for a l l the function symbols ^ of The axioms (a), (b), (c) force P* to behave very much like P JL k*fn in the following sense . Let M be a model of T^ . If _t in W , then P M ( 0 holds i f f P^(t) holds. This is clear, for axioms (a), (b) and (c) force P^ and P * to agree at tuples of the form a^ where ja is a term, and since W i s small, each tuple from W i % of this form. Similarly, construct the theory T* with the predicate symbol Q* B by adding to T_ axioms (a), (b) and (c) with P replaced by Q and P * Ji replaced by Q* . Now l e t T be T* U T* together with the following axioms : A 15 (1) P(x) <-» P ( X ) A P*(X) (2) Q(x) <-> Q ( x ) A Q*(x) - 16 -(3) R(x) <-> g y_ P(x,_) . (4) axioms (a), (b), (c) with P replaced by R and P* replaced by R* . Denote these axioms by T* . R (5) R(x) <-> R(x) v R*(x) (6) R(x) <-> 1 3 z Q (x, z) . Here P, Q, R, R*, R are new predicate symbols of the appropriate arities. We want to show that this theory T with predicate symbol R finitely describes S . Since had only a finite number of constant symbols or function symbols, T is certainly a finite extension of . For any Jt in Wn , either jt in S or _t in S1 . If _t in S, then 3 U A(t,u) . Let u in W be such that A(t,u ) . Since — — — o —o A(_t,u ) i f f T j — P(t,u ) , therefore T 1 P(_t,u ) . By the axioms of the theory T* , PCt,^) <—> P*^,^) for any ( t ^ ) from Wk+n so T*|— (P(jt,u ) A P*(^,u )) and by axiom (1) of T, T | 3uP(t,u) . By axiom (3) and then axiom (5) of T, T|— R(t) . Using essentially the same argument, one can show that i f _t in S' , then T\ lR(_t) . We s t i l l have to show that i f T|—R(t) , then t in S, which will complete the requirement that T | R(t) i f f J; in S . However, this will follow from the consistency of the theory T which we are going to prove next. For i f T|—R(t) and _ t ^ S , teW 1 1 S, so T | ~|R(t) and T is inconsistent. Let M be a model of T. U T U T , where T is the set of A B a l l true sentences of L^ . We want to construct a model for T U T From M. - 17 -II.2.3.1 Lemma. Let ^(n) <~ > ' ^ j ^ — ^ for u_ , a sequence from W, and P*(_u) <—> (P^ .CJLI) otherwise. Define Q* , similarly. Then axioms of T* , T* and T* hold. A B R Proof : Consider a l l the.axioms of theory T* . Axiom (a) certainly holds. A A l l the other ones are in the form U —> V . Take _u not from W, then p M ( u ) <—> ~] CjJ.) • So the antecedents U of axioms (b) and (c) of T* are always false. The implications U —> V are true then. If _u is from W, both the antecedents and the consequents are true, so again the implications are true. Hence a l l the axioms of T* A hold» With similar proofs, a l l axioms of T* and T^ hold. B R Let P M(u) <—> p M(u;) A P^Cli) f o r a 1 1 l i • Similarly, QM(H) <-> Q M(_) A QJ(U). Let R^u) <-> R^u) V _) • So axioms (1), (2) and (5) of theory T hold. These definitions lead to the following lemma : — k+n — II. 2.3.2 Lemma. (i) PM(u) <-> PM(u) for a l l u from W , PM(u) is always false otherwise. (ii) QM(u) <-> QM(u) for a l l u from Wq+n, i s always false otherwise. — k+n — (i i i ) Bj^ Cu) <—> ^ ( u ) for a l l u from W . R^Cu) is always true otherwise. Proof : Trivial. - 18 -Let R^Ct) be true of 3 u PM(_t ,u) . By the definition of PM, vi is from w since P^ (t_»u) doesn't hold otherwise. So R^ (^jt^ ) is fals i f t. is not from W . Then axiom (3) of T is now satisfied. The only axiom that is left to be checked is axiom ( 6 ) . To show that axiom (6) R(x) <—> ~j 3 JZ Q(x,_z) is true in this constructed model, first suppose that _ is not from W . Then by Lemma II. 2 . 3 . 2 ( i i i ) P^Ct) is true . Q^t^u) is false by II. 2 . 3 . 2 (ii) for a l l u, and hence ~] ^ _u Q^(t,_) is true. Secondly, suppose Jt is from W . If Rjj(j_) is true, then R^Ct) is true by Lemma II. 2 . 3 . 2 ( i i i ) . But then fo some u.,PM(_t,u) ± s t r u e a n c j hence PM Ct,u) is true by II. 2 . 3 . 2 (i) . Therefore t is in S • If ^ ( t ) is false, then ^ _u QM(_t,u) . Since Jt i s from W , R^ .(jt^ ) is false and so Jb is not in S which implies that ^ H Qj^-tju) * s true and "| ^ u Q^ (t'.H.) false. So T U r is consistent and hence for any sentence Y of L^ if T I— Y , then Y is true in W . Hence S is finitely describable. - 19 -CHAPTER III SOME NON-FINITELY DESCRIBABLE SETS As an analogue to Gbdel's undeciability results, we are going to show that the set of theorems of the predicate calculus is not finitely describable. However, i t is finitely enumerable. We will start by letting W be a small structure for the language L^ which has constant symbols a^, a^, function symbols f^, f^ and predicate symbols P^ , P^ . Let Liog y be t n e first order language which has a^, a^, f^, f^, P^ , P m together with the letters x, a, |, F, P> 3 > V , "1 , *, T, F as constant symbols and a single binary function symbol, written as concatenation. Let H be the set of terms of Ly of the form f^a^ * ... * a n • G be the free semi-group over the constant symbols of k-^g w> a n a l e t R be the following set of relations: P||^ | s * t = T for a l l s, t e H for which s^ = t^ . P|j^| s * t = F for a l l s, t e H for which ~"] ( s w = fcw) • P.(t,, t ) = T for a l l t 1 } t e H and P. = P.. , P l 1 n 1' . n i 1' ' m such that P. holds at (t, , ...» t ). xw ha "w P. (t , ... , t ) = F for a l l t 1 , . .., t E H and P = P-- , .. . , P such that ~]P.(t.., t ) holds x 1 n Let log W be the structure G/R. We are going to show that - 20 -certain important subsets of log W are finitely describable. The set {a^ > . • • > a^, ^ Z9 *^1' • • • * > ^ * a * i > • * • » A is finitely describable. For let T, be T, together with the axiom 1 log W Symb(u) <—> u = a 1 V u = a 2 V ... Vu = f^ V ... \/ u = V ...Vu = x V . . . V u = Then T^ with predicate symbol Symb describe the set. Construct the theory T 2 by adding to T^ the following axioms length(u) = 1 <—> Symb(u) Symb(v) —> length(uv) = (length(u))| Nat(u) <—> u = length(u) Var(u) <—> u| = x length(u) Const (u) <—> (u| = a length (u)) V n = a^V . . . V u = . T 2 with predicate symbol Var describe the set of variables {x, x | , x | | , .. . }. T 2 with predicate symbol Nat describe the set {|, ||, |||, . T 2 with predicate symbol Const describe the set of constants {a, a | , a||> •••» » a2' • • *» a\i^ ' Let be T 2 together with the axioms : Fun. (u, n) <—> (Nat(n) A. 3 m (Nat (m) A u = F ). i n * m - 21 -Let c be the maximum arity of f^, f . For any i <_ c ,' i f there are p i-ary function symbols f. , f. among f.. , f, , then 1 p Fu^Cu, i) <—> u = f. v •«• V u = f. . If not, then ""iFu^Cu, i ) . Since Xl 1p there are only a finite number of function symbols f f , so a X x< finite l i s t of axioms define the predicate Fun^Cu, n). Fun(u, n)^ >Fun^(u, n) V Fm^Cu, n) . with predicate symbol Fun describe the set of n-ary function letters n * m' 1' ' I Similarly, a thoery with predicate symbol Pred can be constructed in the same manner as T_ such that T. with Pred describe 3 4 the set of predicate letters P , P. P • .' n * m 1 m The set of terms of log W is also finitely describable. Let T^ be (J together with the additional axioms : Const(u) V Var(u) —> Term(u) SeqnTerm(u, |) <—> Term(u) Term(u) A SeqnTerm(v, n) —> SeqnTerm(u A v, n|) SeqnTerm(u, n) —> Nat(n) . SeqnTerm(u, n) A Fun(v, n) —> Term(vu). Term(u) A ~1 Var(u) A ~l Const(u) —> EJ v, w, n (Fun(v, n) A SeqnTerm(w, n) A u = vw ). - 22 -SeqnTerm(u, n|) —> 3v, w (SeqnTerm(v, n) A Term(w) A U = v * w) . It is easy to see that T,. with the predicate symbol Term describe the set of terms, which is the smallest set of words containing the variable symbols and constant symbols and having the property that i f D is an n-ary function symbol and t.. , t are terms, then Dt. * ... * t is a term. I n 1 n Let Tg be T,. together with the following axioms : SeqnTerm(u, n) A Pred(v, n) —> Atom(vu) Atom(T) A Atom(F). Atom(u) A ~] (u = T) A ~1 (u = F) —> 3 v, w, n (SeqnTerm(w, n) A Pred(v, n) A u = vw ). Tg with predicate symbol Atom describe the set of atomic formulas. Following the description of the set of atomic formulas, i t is easy to describe the set of formulas. Let T^ be T^ together with the axioms : Atom(u) —> Form(u) Form(u) A Form(v) —> Form(\/uv) Form(u) A Var(y) —> Form(3yu) Form(u) —> Form(-)u) Form(w) —> Atom(w) v (3u, v (Form(u) A Form(v) A w = uv)) V ( 3 Y J u (Var(y) A Form(u) A w = 3 y u ) V (3u (Form(u) A w = ~| Tfi with .Form describe the set of formulas. Note that in here, we - 23 -are using V uv instead of the ordinary notation u v v . This is followed from Shoenfield's notation in Chapter II of Mathematical Logic. The idea is to avoid brackets in the formal language. The usual notations are introduced later. To deal with free and bound occurrences of variables, we introduce the notion of subformulas. Let T_ be Tn together with the following axioms: ImSub(u, v) <—> (v = ~]u) V (3y (Var(y) A v = 3 yu ) V ( 3 s, t (v = Vst A(s = u v t = u))) . SubForm(u, v) —> Form(u) A Form(v) • ImSub(u, v) A Form(u) —-> SubForm(u, v) . ImSub(u, v) A SubForm(v, w) —> SubForm(u, w) . Form(u) —> SubForm(u, u) . SubForm(u, v) —> (u = v) V ( 3w (SubForm(u, w) A ImSub(w, v))) . Atom(u) —> V* v (SubForm(v, u) —> v = u) . Notfree(y, u) <—> Var(y) A Form(u) A V s , t, t* (u = syt V u = sy) A 7 (t = t')) —> 3 v, w (SubForm(v, u) A v = 3yw A 3 P » Q» r, z ((s = pq V s = q) A (t = rz v t = r) A qyr = v )) . Sent(u) <—> Form(u) A Vy (Notfree(y, u)) . Tg with predicate symbol Sent describe the set of sentences. Construct an axiom which says that ImSubst(y, u, v, w) holds i f f y is a variable symbol and u is a term and v is a formula and w is - 24 -obtained from v by substituting u for a free occurrence of y. Using ImSubst, and the same technique as constructing SubForm from ImSub, an axiom which says Subst(y, u, v, w) holds i f f y is a variable symbol and u is a term and v is a formula, and w is obtained from v by a chain of substitutions of u for free occurrences of y . Then, construct an axiom which says that FinalSubst(y, u, v, w) holds i f f Subst(y, u, v, w) holds and w has no free occurrences of y and u is substitutible for y in v. Then, let T^ be obtained by taking the union of a l l axiom previously mentioned. Now we are going to construct axioms which describe the set of logical axioms ( [ 7 ] , p. 2 1 ) . Let T^Q be T^ together with the following axioms : Logax(u) <—> Propax(u) v Identax(u) v Equax(u) v Substax(u) . Propax(u) <—> 3 V (Form(v) A u = V~lw). Identax(u) <—> 3 y (Var(y) A u = P|j^jyy ) • Substax(u) <—> 3 y, s, v, w (Var(y) A Term(s) A Form(v) A FinalSubst(y, s, v, W ) A U = w 3 yv ). Seg(| , u, v, w) <—> Var(v) A Var(w) A u = V 1 P| |.^| vw . Seg(n|, u, v, w) <->3p> q> r, x, y, z (Seg(n, p, q, r) A Seg(|, x, y, z) A u = px A v = q*y A w = r* * a is substitutible for x in A i f for each variable y occurring in a , no part of A of the form 3yB contains an occurrence of x which is free in A . - 25 -Equax(u) <~> 3 n > x> y> z> v (Nat (n) A Seg(n, x, y, z) /s((Fun(n, v) A (u = x Pj j^j Vy Vz)) V (Pred(n, v) A u = x V l V y V z ) ) ) . T^Q with predicate symbol Logax describe the set of logical axioms. Let be T^Q together with the axiom : NonLogax(u) <—> u = T v u = ~ ] F . Then T^^ with NonLogax describe the set of nonlogical axioms. In order to describe the action of the rules of inference, we need to add symbols ER, CR, AR, TR and IR for the expansion rule, contraction rule, association rule, cut rule and 3-introduction rule ([7], p. 21) ER(u, v) <—> Form(v) A 3 W (Form(w) A u = V wv ). CR(u, v) <—> v = Vuu A Form(u) . AR(u, v) <—> 3 s , t, p (Form(s) A Form(t) A Form(p) A u = VwVst A v = VsV tw ). TR(u, v, w) <—> 3 s, t, p (Form(s) A Form(t) A Form(p) A U = V t p A v = V'st Aw = V~]sp ). IR(u, v) <—> V x , S (Var(x) A Form(s) A Notfree(x, s) —> V w (Form(w) v v = w —> S —> u = 3 xw —> S )) A sequence of formulas is a string of the form u^ * * ••. * U R , where iu are formulas. The set of sequence of formulas is finitely descri-bable using a predicate symbol SeqnForm and the theory T.^ which is - 26 -defined in a way similar to the description of the sequence of terms. Let Proof(u, v, w) be the predicate which holds i f f u is a formula and v is a proof using possibly u as an additional axiom of the formula w. The predicate Proof is finitely describable. Before descri-bing the predicate Proof, we need two auxiliary notions. The relation u < v between natural numbers is easily defined using a predicate symbol Less and the axioms : Nat(u) A 1 (u = 1) —> Less(l, u) . Nat(u) A. Nat(v) —> (Less(u, v) <—> Less(ul, vl)) . We also need the predicate Place(u, n, v) which holds i f f u is til the n formula in the sequence v of formulas. The predicate symbol PLAC with the appropriate theory mentioned before together with the following axioms describe the predicate Place . PLAC(u, n, v) —> Nat(n) A Form(u) A SequForm(v) . PLAC(u, n, u) —> Form(u) A n = 1 . PLAC(u, n, v) A Form(w) <—> PLAC(u, nl, w * v) . PLAC(u, 1, v) <-> u = v v 3w (SeqnForm(W) A U = u * w ). Now we are ready to give axioms for theory T^ with the predicate symbol PRF which describe the predicate Proof. Let T^ be the union of a l l the axioms mentioned so far in the chapter together with the following additional ones : - 27 -PRF(u, v, w) <—> SeqnForm(v) A \/n V s (PLAC(s, n, v) —> Logax(s) V NonLogax(s) V s = u v 3 k, I, x, y (Less(k, n) A Less(£, n) A P L A C ( X , k, v) PLAC(y, H, v) A (ER(s, x) v CR(s, x) v AR(s, x)v TR(s5 x, y) V IR(s, x)))) A ( 3 m (PLAC(w, m, v) A V t (lPLAC(t, m|, v))) . T^^ with predicate symbol PRF finitely describes the predicate Proof. A formula w is provable from the formula u i f f there is a proof v of w using u as an axiom. Let Thm(u, w) holds i f f w is provable from u. Therefore, Thm(u, w) <—> 3 v Proof(u, v, w). Since Proof is finitely describable, we have shown that : 1 1 1 . 1 Theorem. Thm(u, w) is finitely enumerable. So the set of theorems is a finitely enumerable subset of log W . However, the set of theorems is not a finitely describable subset of log W . If W is an empty set, then the language we are using is just the basic logic, denote i t by log . 1 1 1 . 2 Theorem. The predicate Thm(u, v) is not finitely describable predicate. Proof : Suppose Thm(u, v) is finitely describable. Then by Theorem 1 . 2 . 4 , Thm(u, P| A| v ) i - s finitely describable, and by another application of the same theorem Thm(u, P J ^ J u ) is finitely describable. By Theorem 1.2.1 *~lThm(u, P. I u ) is finitely describable. So there exists a finite extension | * l T °f ^ I Q O ' w i t n a unary predicate symbol (which can without loss of - 28 -generality be chosen to be P i i ) such that T | — P i i u i f f • 1*1 1*1. ~]Thm(u, P | A J u) . In here, T can be chosen to be finitely axiomo.tized. For let T be T' U Tn where T' is finitely axiomatized. One can replace T.. log J r log by T" having the following axioms : (i) (uv)w = u(vw) (ii) ~] (a = b) for a l l pairs (a, b) of constant symbols of L, where a is different from b . log ( i i i ) ""j (au = b) for a l l pairs (a, b) of constant symbols. (iv) 1(au = bu) for a l l pairs (a, b) of constant symbols where a is different from b . (v) (au = av <—> u = v) for a l l constant symbols a . T" gives a finite l i s t of axioms. Each axiom of T" is true in log, and T" is an extension of T, . Hence i f T I P i i u i f f ~lThm(u, P. i u), log 1*1 1*1 then i t is also true that T* U T"( P J ^ J u i f f ~lThm(u, P J ^ J u). By taking the conjunction of a l l axioms of T1 \J T" and expressing the resulting sentence in L, , we can find an element w of log such log' o 6 that wo[ P j ^ | u i f f "")Thm(u, u) f o r an U t j n particular, let u = w . Then, w I P i i w i f f Thm(w , P i i w ), and so we have o o 1 |*| o o' |*| o Thm(w , P i | w ) i f f ~J Thm(w , P i i w ) which is impossible. Hence the o I *| o ' o I*| o ^ predicate Thm(u, v) is not finitely describable. - 29 -III.3 Corollary. The predicate Thra(u) which holds i f f |—u, is not a finitely describable predicate. Proof : Suppose Thm(u) is finitely describable, and let f be a function defined as f(u, v) = u —> v . Then, by Theorem 1.2.4, Thm(f(u, v)) = Thm(u —> v) is finitely describable. By the Deduction Theorem ([7], p. 33), Thm(u —> v) i f f J— u —> v implies uj v . So Thm(u —> v) is finitely describable implies Thm(u, v) is also finitely describable. But by the above Theorem III.2, Thm(u, v) is not. Hence Thm(u) is not finitely describable. Let Consist(u) be a unary predicate which holds i f f u is a consistent sentence . III. 4 Theorem. Consist(u) is not finitely describable. Proof : u is a consistent sentence i f f ~] (u | f) i.e. ~\ Thm(u, f ) , where f is a sentence false in a l l structure. So i f Consist(u) is finitely describable, then ~] Thm(u, f) is also, and by Theorem 1.2.1, Thm(u, f) is finitely describable which is proved to false by III.2 . Therefore the set of consistent sentences is not finitely dgscribable . - 30 CHAPTER IV THE RELATION BETWEEN F I N I T E DESCRIBABIL ITY AND RECURSIVENESS In tills chapter we are going to show that finite describability is a generalization of recursiveness, and that for a significant class of structures W, the two concepts coincide. First we start with a very special structure W, and then go on to more general ones. Let W be the natural numbers under the successor operation, where L^ has constant symbol 0 and unary function symbol S . For convenience, write 0 instead of 0IT and S instead of S I T . As W W n times usual, n will be an abbreviation for S S . . . S O IV.1 Theorem. Any recursive function f on the set of natural numbers is finitely describable on W. Proof : We proceed by induction on the definition of recursive function. (1) Let f be the projection function i " , i.e. f(x^, X R ) = l?(x n, x ) = x. . Let T. be TIT together with the axiom l 1 n I 1 W ° F 1(x 1, x n) - x. . It is trivial to see that for any a_ = (a^, an) in Wn ., T.J F 1(a) = f(a) .. For any model M of T^ U T , where T is the set of a l l sentences of 1^ true in W, a model M1 for T^ U T can be constructed such that M' is M except for the interpretation - 31 -F (a , . .., a ) = a. for a l l n-tuples. Therefore T. U T Is consistent V 1 n Hi 1 and hence for any sentence Y of , i f T^j Y, then Y is true in W . So f is finitely describable. (2) . Let f be the addition function + , i.e. f(x^,x 2) = x^ + . Let T 2 be together with the following axioms : F2(x,0) = x and F^x^Sx^ = SF^x^x^ . Then for any a^, a 2 in W, we want to show that T21 F 2(a^,a 2) = f(a^,a 2) = + a 2 . Proving by induction, suppose a 2 = 0, then T 2I F 2( a i,0) = a± and f(a±,0) = a ; L + 0 = a± . Therefore T 2 | F^a^O) = f(a^,0) . Suppose T 2 ( F^a^.a^ = a^ + a2 for some a 2 . By axioms of T 2 , T 2 r — F 2(a ,Sa_,) = SF 2(a 1,a 2) . By assumption, T2) F^a^Sa^ = S(a^ + a 2) = a^ + (a 2 + 1) . Therefore, by induction, T2I F ^ a ^ a ^ = f(a 1 }a 2) for a l l a2.*a2 i n W • I t : i s c l e a r that \J T is consistent and hence for any sentence Y of 1^ , i f T21 Y, then Y is true in W . So f is finitely describable. (3) Let f be the multiplication function., i.e. f(x^,x 2) = X-JL* x2 Let T^ be T 2 together with the following axioms : F3(x,0) = 0 and F^x^Sx^ = F 2(F 3(x ] L,x 2) .x^ . With a similar proof as in (2), i t can be shown that for any a^,a2 in W, T^ | F 3(a^,a 2) = f(a^,a 2). It is also clear that for any sentence Y of 1^ , T^l Y implies Y is true in W . So f is finitely describable. - 32 -(4) Let f be the function 1^ , i.e. f(x^,x 2) = K^Cx^x,,) =0 if x^ < x^ and f(x^,x2) = K^Cx^x.^) = 1 otherwise. Let be together with the following axioms : 1(« < 0) (x 1 < Sx2) —> (X;L < x 2) V (2^ = x 2) (x1 < x 2) v (x 1 = x 2) V (x 2 < x x) (X]L < x 2) —> F 4( X ] L,x 2) = 0 l ( x 1 < x 2) —> F 4( X ; L >x 2) = SO . For any a-^ >a2 i n ^ , | a^ < a 2 i f f a^ < a 2 . So T^j F 4(a 1,a 2) =0 i f a]L < a 2 and F^Ca^a^ = 1 otherwise. Therefore T^| F^Ca^a^ = fC a ^ a ^ . It is clear to see that T^ \J T is consistent and hence for any sentence Y of L^ , T^ | Y implies Y is true in W . Therefore f is finitely describable. (5) Let f be a recursive function on the set of natural numbers defined as fCx^ xn> = gCh^x^ x ), ^ ( ^ J •••» XN>) where g, h^, h^ are recursive. Suppose g, h^, h^ are finitely describable, let T , T ..... T, be finite extensions of TIT , with g n l hk W function symbols G, H^ , that describe g, h^, h^ respectively. These theories can be chosen such that their languages have only L^ in common. Construct a finite extension T,. of T w , with function symbol - 33 -F such that T is T U T, U U T together with the additional 8 1 \ axiom ^O^, •••» \) = G(H1(x;L, ..., x n) , H^O^, •••> X R ) ) • For any a. , . . . , a in W , T_ I F c(a,, . .. , a ) I n 5 1 5 1 n = G(H^(a^, a R), . .., H^ Ca^ , . .., a n)) . With the properties of theories T c » T v, » ' *' ' T v, • ^ i G(Hi (ai > • • • > O » • • • » H u ( a i » • • • . a )) g n^ n^ 5 1 1 n k. 1 n = gCh^a^ . .., a n), h^(a^> ..., an>) = f(a 1, an> . Hence , T,. |— F,. (a^, ..., a^) = f(a^, ..., a^) . By Lemma 1.2.2, T U T U ... U T, U T is consistent, so for any model M of i t , g h x h k a model M' of T,. U T can be constructed such that M' is M except for the additional interpretation F^ (t) = G^ O*, (t), H (t)) for a l l n tuples. Therefore T^ U T is consistent and hence for any sentence Y of 1^ , T 5 I—Y implies Y is true in W . So f is finitely describable . (6) Let f be defined by f(x^, x^ ) = yy(g(x^, x n > y) =0), where g is recursive. Suppose g is finitely describable, let T be a finite extension of T^ with a function symbol G that describes g. Construct a finite extension T, of Tr, , with function symbol ¥, such o W o that T, is T U T, together with the additional axioms : 6 g 4 b ( F 6 ( X l , x n) = y) <-> (G( X ; L, x n, y) = 0) A (Vz)((z < y) —> -|(G(x1, ..... x n, z) = 0))) . - 34 -For any a^, • a n > in W , the additional axiom imply that T, I F,(a,, a ) = ub(G(a.,, ..., a , b) = 0) . With the o o 1 n 1 n properties of T , T, 1— F, (a. , .. ., a ) = f (a. , . .. , a ) . Also, i t is g 6 1 6 1 n 1 n clear that Tg U Y is consistent and hence for any sentence Y of , i f T, |— Y , then Y is true in W . So f is finitely describable. o Hence recursiveness implies finitely describable on the special structure W . The converse of theorem IV.1 also holds : IV.2 Theorem. If f : Wn —> W is a finitely describable function, then f is a recursive function. Proof : Since f is finitely describable, there exists a finite extension T of T^ , with function symbol F that describes f . Let P^ ,(a,u) be the predicate which holds i f f a is the index of a proof of the sentence with index u. Since T is a finite extension of Ty , and T^ is clearly recursively axiomatized, so T is recursively axiomatized and therefore P^ ,(a,u) is recursive. Define the function g by g(t»y) = index of the sentence F(t) = y. Then PT(a,g(t,y)) is recursive. Let S(a,t,y) hold i f f P^,(a,g(t,y)) holds. By substitution, S(K(b),t,L(b)) where K, L are the "unpairing functions" (inverses of the pairing function*) which are recursive. By the definition of recursive function, L(ub(S(K(b),t,L(b))) is recursive. But L(ub(S(K(b),t,L(b))) = f(t), so f(t) is recursive. * 1 2 The pairing function D(u,v) = — [ (u + v) + 3u + v] and D(K(w),L(w)) = w. - 35 -Hence the notion of finite describability agrees with recursiveness on the natural numbers. We w i l l now consider more general structures W and compare the notions of finite describability and recursiveness in a more general setting. Definition : The structure W is finitely describable i f TTT is a finitely J W describable subset of the set of a l l words on the basic alphabet for logic in Chapter III. Denote that set by log . IV.3 Lemma. Let W be a finitely describable structure. Let Ind be an effective indexing of log . Then Ind(Ty) is a recursive set of natural numbers. Proof : Since W is finitely describable, there is a finite extension T of T^og » w i t h a unary predicate symbol R, such that for any u, T | R(u) or T I lR(u), and T|—R(u) i f f u in TTT . Now T. is clearly W log recursively axiomatized, and since T is a finite extension of Tn , T log is also recursively axiomatized. By a standard result i f T is recursively axiomalized and Ind is an effective indexing of L^ , , the set of indices of Theorems is recursively enumerable. But the set of formulas of the form R(u) is recursive, so the set of indices of theorems of the form R(u) is recursively enumerable. Hence the set of indices of formulas u such:that T| R(u) is recursively enumerable. Similarly, the set of indices of formulas u such that Ti ~lR(u) is recursively enumerable. But for any formula u, either T| R(u) or Tl ~lR(u) and the set of indices of - 36 -formulas is recursive, so by a standard result, the set of indices of formulas u such that T|— R(u) is recursive, so Ind(T ) is recursive. w IV.4 Theorem. Let W be a finitely describable structure, and let S C be a finitely describable subset of If Ind is an effective indexing of , then Ind(S) is a recursive subset of N n . Proof : Since W is a finitely describable structure, there is a finite extension T of T w with a predicate symbol R such that for any 11 e T I — R(u) or T| lR(u), and u e S i f f T|—R(u) . By lemma IV. 3, T^ has a recursive set of indices, and since T is a finite extension of T^ , T is recursively axiomatized. Then the set of indices of theorems of T is recursively enumerable. But the set of sentences of the form R(u) is recursive, so the set of indices of theorems of the form R(u_) is r.e. Hence the set of indices of u such that T) R(u) is r.e. . Similarly, the set of indices of u such that T 1— 7R(u) is r.e. . But for any u. e W11 , either T (—- R(u) or T| ~] R(u) and the set of indices of sentences of form R(u) is recursive, so by a standard result, the set of indices of u such that T | R(u) is recursive. Since u e S i f f T|— R(u), Ind(S) is recursive. An essentially f u l l converse of the above theorem can be stated as follows : IV.5 Theorem. Let W be a small structure, and let Ind be a finitely describable indexing of L . If S C Wn and Ind(S) is a recursive - 37 -subset of N , then S is a finitely describable subset of Proof : Since Ind(S) is a recursive subset of N n , by theorem IV.1, i t follows that Ind(S) is a finitely describable subset of N° . Let T with predicate symbol R describe Ind(S). Since Ind is also finitely describable, let T' with function symbol F describes Ind. Let T g be T U T' together with the axiom R„ (x) <—> R(F(x)), where R is a new predicate symbol. For any _t in W° , Ind(t) in N n , so Tl R(Ind(t)) or T|-— ~IR(Ind(_t)) . By the property of T*, T U T' 1— R(F(_t)) or T U T'1 !R(F(t)) , The additional axiom of T implies that T | R (_t) or T g l 1 R S ( ^ ) • Also, Tj—R(Ind(it)) i f f Ind(t_) is in Ind(S) implies that T {— Rg(t) i f f t e S . It is tr i v i a l to see that for any model M of T U T' U T , a model M* can be constructed for T g U T . So for any sentence Y of • 1^ , T S ^ ~ Y i m P l i e s Y i s t r u e i n w • Hence S is finitely describable. Like the equivalences between finite describability and recursiveness, the notion of finitely enumerable is essentially equivalent to the notion of recursively enumerable. It can be stated as follows : IV.6 Corollary. Let W be a finitely describable structure, and let . S C wn be finitely enumerable. If Ind is an effective indexing of L^ , then Ind(S) is a recursively enumerable subset of N n . A converse of IV.6 can be stated as : - 38 -IV.7 Corollary. Let W be a small structure, and let Ind be a finitely describable indexing of L^ 7 . If S C Wn , and Ind(S) is recursively enumerable, then S is finitely enumerable. - 39 -Bibliography S. C. Kleene, Introduction to Metamathematics, Van Nostrand, The University Series, New York, 1952. G. Kreisel, Model-theoretic invariants : applications to recursive and hyperarithmetic operations. The Theory of Models, Proceedings of the 1963 International Symposium at Berkeley, North-Holland, Amsterdam 1965, pp. 190-205. D. Lacombe, Recursion Theoretic Structure for Relational Systems. Logic Colloquium 1969, Proceedings of the Summer School and Colloquium in Mathematical Logic , Manchester, August 1969, pp. 3-17. W. M. Lambert, Jr., A Notion of Effectiveness in Arbitrary Structures, Journal of Symbolic Logic, Vol. 33, No. 4, 1968. Y. N. Moschovakis, Abstract Computability and Invariant Definability, Journal of Symbolic Logic, Vol. 34, No. 4, 1969. H. Rogers, Jr., Theory of Recursive Functions and Effective Computability, McGraw H i l l , New York, 1967. J. Shoenfield, Mathematical Logic, Addison-Wesley, Mass. 1967. A. Yasuhara, Recursive Function Theory and Logic, Academic Press, New York, 1971.