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 In presenting this an advanced degree the I Library further for agree scholarly by h i s of shall this written thesis in at University the make i t that freely permission for It is financial for gain Department Date of of Columbia, British Columbia for extensive by the understood permission. The U n i v e r s i t y o f B r i t i s h V a n c o u v e r 8, C a n a d a fulfilment available p u r p o s e s may b e g r a n t e d representatives. thesis partial shall Head o f be requirements reference copying that not the of I agree and or that study. this thesis my D e p a r t m e n t copying for or publication allowed without my ii Abstract The notion of recursiveness i s 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. iii Table of Contents Chapter I Finitely Describable Sets and Functions 1.1 Definitions 1.2 Basic Properties Chapter II Page Finitely Enumerable Sets 3 • .. 3 7 11 II. 1 Definition 11 II.2 Properties 11 Chapter III Chapter IV Bibliography Some Non-Finitely Describable Sets The Relation between Finite Describability and Recursiveness 19 30 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 i n reading the thesis. support from the University of British Columbia i s greatly The financial appreciated. Introduction The important notions of 'recursive function' and 'recursive predicate' have been defined in many different ways. Among the more important ones are Herbrand-GSdel recursiveness, u-recursiveness, computability by turing machine, and computability by Markov algorithm. have so far turned out to be equivalent. A l l these notions 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 i n recursive theory and i t s generalizations. D. Lacombe i n [3] defined various notions of recursiveness and relative recursiveness on algebraic structures, and some of the more interesting notions are singled out and various equivalences are given. W. H. Lambert J r . i n [4] defined a notion of 'Schematic definability' and proved a number of results. He showed for instance that the set of 'schematic definable functions has the properties that one might reasonably 1 expect, and that certain devices for ordinary recursion theory, like definition 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 c a l l '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. Chapter II, the notion of 'finite enumerability' is studied. In This notion is intended to be a formulation in our setting of the ordinary notion of recursive enumerability. The main result of Chapter II i s that i f a set and i t s complement are finitely enumerable, the set is f i n i t e l y describable. The most interesting result of Chapter III i s an analogue of Godel's result on the undecidability of number theory. It i s proved in this chapter that the set of theorems of the predicate calculus i s not f i n i t e l y describable. A long construction shows that this set i s , however, f i n i t e l y enumerable. Finally, Chapter IV examines the relation between 'finite describability' and ' recursiveness'. It i s 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 theory. setting for recursion 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 d i f f i c u l t i e s do at times arise. - 3 CHAPTER I FINITELY DESCRIBABLE SETS AND FUNCTIONS I.I Definitions I.1.1 Small Structures Let that Ly be a first-order language with equality. We w i l l suppose L^ has only a finite number of constant symbols, function symbols, or predicates symbols. Let W be an I^-structure. underlying set of the structure W. |w| i s of the form In what follows, the letter W be the For any variable-free term 1^ , l e t a^ be the interpretation of a i n W. i f every element of Let |w| W a of i s said to be small a^ for some term a of L^ . always denotes a small structure. The word 'term' always means 'variable-free term' . 1.1.2 The Theory Let (i) a = b, T y be the theory with the following axioms : for a l l pairs (a,b) of terms for which the sentence a = b is true i n W . (ii) ~] (a = b) , for a l l pairs (a,b) of terms for which the sentence a = b (iii) i s false i n W . P(a^,...,a ), n for a l l predicate symbols tuples (a^,...,a ) of terms for which n P of L^ and a l l P(a^,...,a ) n i s true i n W. _ 4 - (iv) 1P(a^,...,a ), for a l l predicate symbols n tuples (a^,...,a ) of terms for which n 1.1.3 Let T P T. For any term M. Let |w^| and a l l P(a^,...,a ) i s false in W. n be a consistent extension of T^, of of and l e t M be a model a of L^, l e t a^ be the interpretation of a i n be the set of a l l a^ as a ranges over the terms of L^ . For any term of L^ , l e t " K ^ ) a • First we show that = < J > i s well-defined, that i s we show that i f a^ = b^ , -then But i f a^ = by , a = b i s true i n W . Hence |w| and so a^ = b^ . Since every element of a , (J) maps |w| Let elements of onto W M i s of the form |w| JW^I . Since f (a ,---,a . So the set |W^| . be "TI Tt L^ structure M . We have then : onto W^ . To show that |w| . Then < j > i s one-to-one < j > i s one-to-one, let a^ and b^ a= b i s false i n W , and so i s an axiom of T^ . Hence we have Let ,...,a M Proof : With the above, i t remains only to verify that be distinct elements of 1 ) = [f (a.. ,... ,a ) ] >f (a, >->*>a ) TI inherits a natural Lemma : $ i s an L^-isomorphism of W and i s an L^-morphism. a^ for some M f be a function symbol of Iv. , and let a by restriction from 1 (a = b) i s an axiom of |w"| . Tl belongs to a =b a^ = b^ , a^ £ b^ . f be a function symbol of 1^, > and let a^ = (a.. ,...,a ) \j "w be a tuple of elements of W . Then <j>(f (a„)) = d>(f(a)) = (f(a))„ = T7 tT - 5- = = ' ^ ^M^^-^W^ e t ^ be a predicate symbol of L^ , and let a^ be a tuple from W . Then of T^ i f f ^ ( ^ J J ) holds in the proof that P^(a^ ) holds in W i f f P(a) is an axiom . Since a^ = <f>(a^), so this completes < j > i s an L^-morphism • So i f M i s a model of an extension of T , M w L^-substructure which is i n a natural way L^-isomorphic to W . So we may, without loss of generality, assume that every model of has an T^ has W M of an extension as an L^-substructure. 1.1.4 Finitely describable subsets of W, n > 1 . n Let extension T SCW . S 1 1 of T is f i n i t e l y describable i f there exists a finite , with an n-ary predicate symbol R such that : w (i) For any model (ii) For any sentence then Y M of T, Y 0 W•= S . n of L^ , i f Y i s true i n a l l models of T, i s true i n W . If the situation described above holds, we say that predicate symbol R describes T with S. Using the completeness theorem for the predicate calculus, one can give an equivalent proof-theoretic definition of f i n i t e l y describable set. Before doing so, we make a simplifying convention. formula, and let. t_ be i n W n expression T I — R(t) terms of L^ such that . Since Let R(x) be a _t is not an n-tuple of terms, the does not make sense. So let _t = a^ . Let T I — R(t) a be an n-tuple of be an abbreviation for - T I— R(a) . theorem of If jt = a^ - h^. , T . So T I— R(a) 6 - a = b_ is an axiom of then i f f T|—R(b_), , hence a and so our abbreviation is permissible . sew T of , with an n-ary predicate symbol (i) For any 1 . (ii) ' 1.1.5 is f i n i t e l y describable i f there exists a finite extension 11 Jt in W, either n ft e W n R, T|—R(t) such that or T h- "| R(t), and | T |— R(t)} = S . For any sentence Y of 1^ , i f T |— Y, Finitely Describable total function from A total function exists a f i n i t e extension f :W 11 T of —> T^, W™ W then to Y i s true in W. n, m >_ i i s f i n i t e l y describable i f there with an n-ary function symbol F such that : (i) For any model M of (ii) For any sentence Y then Y is true in | w" = f. T, of , if Y i s true in a l l models of T, W . By the completeness theorem, conditions (i) and ( i i ) can be replaced by : (i)' For any t Here again jt and so that i n «" , T|—F(_t) = f ( t ) . F(_t) = f(t) is not a sentence, since for jt in f ( t ) are not terms. = jt . Let Let a be a tuple of terms of jb be a tuple of terms of L such that L^ K W, such = f(t) • n - 7 - T I — F(t) = f(t) is an abbreviation for Then T I — F(a) = b . By an argument essentially identical with the one in 1.1.4, this abbreviation i s permissable. (ii) For any sentence 1 1.2 Y of , i f T I — Y, then Y is true in W. Basic Properties 1.2.1 Theorem. If SCW" i s finitely describable, then S = S' is also finitely describable ". Proof : Since extension (i) T For any {_t e W 11 then Y SC of i s finitely describable, there exists a finite T »' with an n-ary predicate symbol _t in is true in T' t_ in {it e W 11 R' T |— ~] R(t) , Y of and , i f Th- i s a new n-ary predicate symbol. T |— R(t) T' I or If T'J— Y, T I "1 R' (t_) | T*h— R ' ( 0 ) = '{t e w" | T| then IR(t). or T'( S'cZ W Lemma : Let Y, For The additional axiom R' (_t) . 1 R(t_) }• = S' . T f— Y (i) Futhermore, ( i i ) Let Y be a which implies that Y is W . Hence 1.2.2 either . or ( i i ) For any sentence implies that either sentence of true in T |— R(t) T . together with the additional axiom where 1 T' either such that W . be (R (X) <—>~]R(x)), of , 11 | T|—• R(t)} = S . Let any W R n i s f i n i t e l y describable. T^, T2 Suppose for any sentence Y be theories such that of L , T, |— Y or L^, T„| 0 L^ Y = 1^ . implies that - 8 - Y is true in W. Proof : Let Let r = T U T = T i T u Then U T |-—Y be the set of a l l sentences of r and I"- = T \J V . 2 Rob inson U T |— ~|Y. and is impossible. Hence 1.2.3 W . which are true in 1^ U T = r U 2 is consistent. of L^ W. U r U T 2 V r I — Y. Y of Since If S^ 1^, U S C T^ U r I — Y and and the assumed properties of W and if T U T W 1Y i s true in 1 U T 2 f — Y » W T^ which t h e n i s consistent and every true T^ U T 2 U T , Y i s true i n are finitely describable, then 11 2 is inconsistent, i s consistent. 2 i s a consequence of Theorem. T By the Craig- (J such that i s true in U T For any sentence formula of Y Y 2 2 U By the definition of T , this implies that U T L^ is true in Joint-Consistency Lemma ([7], p. 79), i f then there exists a sentence 2 Then Y U r. 2 We want to show that T implies that S W . 1 H S 2 is also f i n i t e l y describable. Proof : Since extensions S^, S C T^, T of 2 such that : (i) for any and either { t e W n TJ T^ and 2 | Tj T 2 R (t) 2 1 Y of 1^, are finitely describable, there exist f i n i t e 11 T with n-ary predicate symbol w> jt in or R (jt) } = S 1 any sentence W 2 W, T1 1 l ^ ^ ' 2 1 T l — R^t) either 11 and i f T^|— or respectively 1^—IR^t), | T |— R (t) } = S^ n or 2 Furthermore, { t/e W Y R.^, R 2 T f — Y, 2 can be chosen in such a way that 2 then Y ( i i ) For i s true in L^, ' H L^, = L^. W . - 9- T Let U T be (R(x) <—> R^(x) A R (x)), 2 (i) of For any Jt i n W and T , T j 2 where R is a new n-ary predicate symbol . , by the additional axiom in n T together with the additional axiom 2 R(t) or T| 1 R(t). 1 A For any sentence Y and the properties Also ( t e w " | T h—R(t)} = { t. e W* | T . J — R^jt) (ii) T of L^, i f T I—- Y, T J 2 R (t) } = S ± 2 fl S 2< then by Lemma 1.2.2, Y is true in W . Hence fi S^C W i s f i n i t e l y describable. 11 From theorems 1.2.1 and 1.2.3, i t follows that any Boolean combination of f i n i t e l y describable sets is f i n i t e l y describable. 1.2.4 Theorem (Substitution). Let P(x^, bable n-ary predicate, functions. and f^, Then the predicate P(f^(y^, y^), x^) be a f i n i t e l y descri- f • be k-ary finitely describable Q(y^» •••> y^) which holds i f f ^ (y^» •••> y^)) holds i s a finitely describable n k-ary predicate. Proof : Let Tp be a finite extension of T^, with an n-ary predicate symbol T, W tT Rp that describes with function symbols respectively. Theories T be T F, , 1 T^, T^ 1 their languages have only Let P. Let T^ , ..., T^ be finite extensions of 1 n p F n that describe f.. , ...» f 1 n can be chosen i n such a way that n L^ in common. U T U f 1 U T f n together with the additional - 10 - axiom RpC^^Cx) > •••> F (y_))) where (R(y_) <— > R is a new k-ary predicate symbol. k t_ in W , either It i s t r i v i a l to see that for any or T |— R(t) T| ~lR(t). Furthermore, T | — R ( t ) i f f P ( f _ ) , . . . , f (t)) holds — — I n — i f f Q(t) holds. T U T u . • • • U T U T , where T i s the set of 1 n a l l true sentences of i s consistent by lemma 1.2.2. So for any model p M of I U T p f 1 U ... u T constructed such that R^ (t) <—> M' f n U T is M Rp (F, (t) , . . . , F MM °M , a model. M* So Q(y , 1 y.) T U r can be except for the additional interpretation (t)) for a l l k is consistent and hence for a l l sentences is true i n W. of Y of tuples. L^, Therefore T i f T 1— Y, then i s f i n i t e l y 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. Y - 11 - CHAPTER II FINITELY ENUMERABLE SETS 11.1 Definition SC W i s f i n i t e l y enumerable i f f there exists a f i n i t e l y n describable predicate P(x^, is i n S i f f 3 x ^ 11.2 x^> y^, y^) such that x ^ P ^ , ..., x^., y ^ (Y;L> • • • » Y N ) y >)« n Properties : II.2.1 Theorem. If S C W n i s f i n i t e l y describable, then S i s finitely enumerable. Proof : Since S i s f i n i t e l y describable, there exists a f i n i t e extension T of T , with an n-ary predicate symbol w in (ii) W, n either T|— R(0 For any sentence Let R or T f — l R ( t ) such that (i) For any _t and {_t e W n Y of 1^ , i f T |—- Y , additional axiom y^) , i s in S . Let T^ be T (R^(x, y ^ y^) <—> R(y^, R(t)} - S. Y i s true i n W . then P be an (1 + n)-ary predicate such that holds i f f (y^, | T| P(x, y^, together with the Y ) ) > where N a new (1 + n)-ary predicate symbol. (i) For ary (u,Jt) in W 1+n R p is ' , either T| T I p' R(t) or T| The additional axiom of T P implies that Also, the set {(u,t) e W | T |—• R (u,t)} = {t e W 1+n y ) R (u,t) P ~ n ~]R(t) . or T I P l 1 R (u,t). P - | T | — R ( t ) } = S, - 12 - i.e. P(u,t) (ii) holds i f f T |— R (u,t). For any model M sentences of P i where r (u,_t) <—> R^OO M' is M for a l l (l+n)-tuples. M and hence i f T I P describable. Y, then Y By the definition of S. Since P This implies that M' can be except for the additional interpretation Then T P M is in is the set of a l l which are true in W, a corresponding model constructed such that R T u P , of i s true in W . P, So u r P P(x, y^, ..., y ) n is i - n i s finitely holds i f f (y^, . .., R (y^» •••» Y ) i s consistent iff 3 S has proved to be finitely describable, therefore X S P( > ••• x is finitely enumerable. For the next result, we need to extend the notion of f i n i t e l y describable function a l i t t l e b i t . Let uniquely expressed as a function from f_ = (f^, ...» f) , where each r to of the f. is. 1 II. 2.2 Theorem. If W W . SCw" . Then f can be f^ , 1 <_ i <_ n is f_ i s said to be finitely describable i f each and S ^ <j> , then S is f i n i t e l y enumerable i f f i t is the range of a finitely describable function. Proof : -> If SCW is finitely enumerable, then there exists a finitely 11 describable (k+n)-ary predicate 3 x . P(jx,y_) . function of f_(x,x) = X W Since k+n P(x,y_) such that S ^ <|> , choose a fixed w into W n defined as i f P(x,jy_) . Therefore S y_ in in jf(x,y_) = w S iff S . Let f i f ~| P(x,jy_) is the range of f_ . be a and - 13 - To show that up a theory T^ f_ is finitely describable, we are going to build which finitely describes the predicate symbol R f_ . Let the theory describes P . Let T,, —> p and (R (x»Z) —> F p where F F^, components of (i) T -| w . , ± Z(JL»_i) IL • Y of P , i t turns out that = B k+n , either T I M ' ^ = M of T P 1^ , a model . M' f o r and hence T^ \— Y describable . ( a 1 1 R k S = f^W ) <= If W . Let T^ that describes f_ . Let into k + n implies holds i f f f/x) = y_ • T |—• R (_>Ji) So o r p imply that f U T , where of (t,u) —> ) Y - t u Pl T T| ;F(jL>2i) _ =w f U T is the set of a l l can be constructed such F , (t) = u.. and w 1 R ~~ e s (t,»u.) • i s true in S o W . (t,u) P ~~ M T f U T Therefore i s consistent f_ is f i n i t e l y for some finitely describable function be a theory with function symbol P are the _(t.,u) = f.(jt,u) . f M > w^ n P -— n •••> ^ ) • T |— M except for is 1 1 1 definition and the finitely describability t n e For any model true sentences of 1 1 ± (t,u) . The additional axioms of (ii) P l<i<n' (*>l) = y ) » (jt,u) in W T^| M ± Express _F = or that F (x,_) = w ) with together with are new n-ary function symbols, and the r For ary 1R ± T I P the following additional axioms : (lR (x,x) be T^ F^, be a (k+n)-ary predicate such that y_ in S i f f 3x 0i>y_) . p _f of F^ P(x,y_) To show that P - 14 - i s finitely describable, let axioms ; ( p(2L>i) R < — > be together with, the additional F(x) = y_) , where is a new (k+n)-ary predicate symbol. T I p 1 k+n (_t,u) in W , either R (t,u) i f f f ( t ) = u i f f p — — — (i) It is t r i v i a l to see that for ary R (t,u) or T | ~1R (t,u) and I | p —'— p' p —'— p P(_t,u) holds. (ii) For any model sentences of true in M of T^ U P , where W , a model M is the set of a l l U T of 1 r can be constructed (t,u) <—> F..(t) = ir, . So T \J T • P. -^M p i s consistent and hence for any sentence Y of , T | — Y implies Y such that M' is M except for R M i s true in W . Hence 3 jx(f_(jx) = y_) II. 2.3 then P i f f 32£ P(2i»Z) > Theorem. S i s finitely describable. If S CW™ and Since S S iff is finitely enumerable. W^N^S = S' are both f i n i t e l y enumerable, i s finitely enumerable, there exists a f i n i t e l y describable (k+n)-ary predicate Let the theory Similary, T S' = W \ n A such that with predicate symbol S P x e S i f f 3 2. A(2i>y_) • finitely describe A . is finitely enumerable, so there exists a f i n i t e l y describable (q+n)-ary predicate T S y_ in is finitely describable. Proof : Let s o Therefore with predicate symbol B Q such that x £ S' finitely describes i f f 3 i B(x,z) . B . - 15 - Construct the theory adding to T A with new predicate symbol r^) f o r a l l m-tuples ( r ^ , m r ^ = j ^) a ^ a n J (1) .£ J ( ) Ji ••• 5. J ( ) > <l ^» •••> 2 the constant symbols of (b) L^ . P(TTU.., .... iru )) 1 m m f o r a l l m! P*(x , u , k U l , u )) — > m permutations of m /. u ) > <_ 2 F( m <—> P ( f ^ ( x ^ , . . . , x -\> u 2 1 » u m ) )— ..., u )) r e (P*(Fu , ... .,Tfu ) <-> 1 m 1. .... m . -.-A m JL ( * ( f ( x , ••• , x ^ , u , ..., u ) > p i 1 2 f o r a l l the function symbols The axioms (a), (b), (c) force i n the following sense . Let M m P ^ and i s a term, and since JL T^ . of P k*fn I f _t i n W , This i s c l e a r , f o r axioms (a), (b) P * to agree at tuples of the form W ^ P * to behave very much l i k e be a model of ( 0 holds i f f P ^ ( t ) holds. and (c) force a n t 2 M a j ^> u , P a ( P * ( x , u,, .. . , u ) <-> P ( x , u , . .. , u ) A 1 then an r^) • ( P * ( u , ..., u ) <-> P ( ± m l (c) P * by the following axioms : P * ( r ^ , . .., r ) <—> P ( r ^ , (a) where T* i s small, each tuple from S i m i l a r l y , construct the theory T* W a^ where ja i % of t h i s form. with the predicate symbol Q* B by adding to T_ Ji replaced by axioms (a), (b) and (c) with P replaced by Q and P * Q* . Now l e t T be T* U T* A 15 (1) P(x) <-» P ( X ) A P * ( X ) (2) Q(x) <-> Q ( x ) A Q*(x) together with the following axioms : - 16 - (3) R(x) <-> g y_ P(x,_) . (4) axioms (a), (b), (c) with R* . Denote these axioms by (5) R(x) <-> R(x) v (6) R(x) <-> 1 3 z Q (x, z) Here P, Q, R, R*, R P replaced by S . For any in S, then of the theory T*|— are new predicate symbols of the appropriate arities. T with predicate symbol i s certainly a finite extension of Jt in W n , either 3 — A(t,u) — — . Let U uo jt in in W T 1 T, T|— T| R(t) and _t in S . If _t 1 A(t,u—o ) . Since P(_t,u ) . By the axioms (t^) from T, T | W k+n 3uP(t,u) . R(t) . Using essentially the S' , t _t^S, in T teW T\ then i f f J; in w i l l follow from the consistency of the theory For i f T | — R ( t ) or and by axiom (1) of s t i l l have to show that i f T | — R ( t ) , then complete the requirement that S for any same argument, one can show that i f _t in T finitely . be such that T* , PCt,^) <—> P*^,^) By axiom (3) and then axiom (5) of and R had only a finite number of constant symbols or (P(jt,u ) A P*(^,u )) prove next. replaced by . i f f T j — P(t,u ) , therefore A(_t,u ) so T P* R*(x) Since function symbols, and T* . R We want to show that this theory describes R S, lR(_t) . We which w i l l S . However, this which we are going to 11 S, so T| ~|R(t) i s inconsistent. Let M be a model of a l l true sentences of T. U T A B U T , where T i s the set of L^ . We want to construct a model for TUT From M. - 17 - II.2.3.1 Lemma. Let ^ ( n ) ~ ' ^ j ^ — ^ < P*(_u) <—> (P^.CJLI) otherwise. for u_ , > Define Q* , a sequence from similarly. W, and 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 U —> V . A l l the other ones are in the form Take _u not from U W, then p M ( u ) <—> ~] CjJ.) • So the antecedents of axioms (b) and (c) of T* are always false. are true then. If _u i s from W, The implications U —> V 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 (u) <—> (u;) A P^Cli) p M Q (H) <-> Q (_) A QJ(U). M f o M 1 1 li • Similarly, Let R^u) <-> R^u) V M (2) and (5) of theory r a T hold. _) • So axioms (1), These definitions lead to the following lemma : II. 2.3.2 — (i) P (u) <-> P (u) Lemma. M M for a l l u from k+n — W , P (u) i s M always false otherwise. (ii) Q (u) <-> Q (u) for a l l u from W , — Bj^Cu) <—> ^ ( u ) for a l l u from k+n — W . R^Cu) i s always M M q+n i s always false otherwise. (iii) true otherwise. Proof : T r i v i a l . - 18 - R^Ct) be true of 3 u P (_t ,u) . By the definition of P , Let vi if i s from M w since P^(t_»u) M doesn't hold otherwise. So R^^(jt^) i s fals t. i s not from W . Then axiom ( 3 ) of T i s now satisfied. The only axiom that i s left to be checked i s axiom ( 6 ) . To show that axiom ( 6 ) R(x) <—> ~j 3 JZ Q(x,_z) f i r s t suppose that _ i s true in this constructed model, i s not from W . Then by Lemma I I . 2 . 3 . 2 ( i i i ) i s false by II. 2 . 3 . 2 ( i i ) for a l l u, and P^Ct) i s true . Q^t^u) hence ~] ^ _u Q^(t,_) i s true. Rjj(j_) i s true, then R^Ct) i s true by Lemma I I . 2 . 3 . 2 ( i i i ) . some u.,P (_t,u) ± M Therefore s t r u e anc Secondly, suppose Jt i s from W . If j hence t i s in S • If ^ ( t ) P Ct,u) M But then fo i s true by I I . 2 . 3 . 2 (i) . i s false, then ^ _u Q (_t,u) . Since M Jt i s from W , R^.(jt^) i s false and so Jb i s not i n S which implies that ^ H Qj^-tju) So if * true and "| ^ u Q^(t'.H.) false. T U r s i s consistent and hence for any sentence Y of L^ T I— Y , then Y i s true i n W . Hence S i s f i n i t e l y 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 i s not f i n i t e l y describable. However, i t i s finitely enumerable. We w i l l start by letting W be a small structure for the language L^ which has constant symbols a^, and predicate symbols P^ . Let i o g y which has x, a, a^, P^, a^, function symbols L a^, f^, f^, P^, |, F, P> 3 > V , "1 , *, T, P F m be Ly of the form f^a^ * ... * the constant symbols of k-^g > a n a n a w be the set of terms G be the free semi-group over t be the following set of relations: R for a l l s, t e H for which s^ = t ^ . s * t = F for a l l s, t e H for which ~"] ( P.(t,, l 1 P. w t ) = T n holds at x ~]P.(t.., x 1 Let log W for a l l t 1' 1 } . t eH n s = fc w w ) • and P. = P.. , i 1' P ' m (t, , ...» t ). ha "w P. (t , ... , t ) = F such that Let H P||^| s * t = T P|j^| such that e f i r s t order language as constant symbols and a single • l f^ together with the letters binary function symbol, written as concatenation. of t n e f^, for a l l t , . .., t 1 E H and P = P-- , .. . , P t ) holds n be the structure G/R. We are going to show that - 20 - certain important subsets of log W The set {a^ > are finitely describable. ^Z . • • > a^, 9 is finitely describable. For l e t T, be 1 Symb(u) <—> u = a 1 ^*1' > ^* a * i > •*•» A T, together with the axiom log W V u = a V ... V u = f^ V ... 2 \/ u = Then •• •* T^ with predicate symbol Symb Construct the theory T 2 V ...Vu = x V . . . V u = describe the set. 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 T 2 with predicate symbol .. . V u = . Var describe the set of variables {x, x | , x | | , .. . }. T 2 with predicate symbol Nat T 2 with predicate symbol Const {a, a | , ||> •••» a Let » 2' • • *» \i^ a a be T 2 describe the set {|, ||, |||, . describe the set of constants ' 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 are p i-ary function symbols Fu^Cu, i ) <—> u = f. v l f^, f f. , 1 . For any f. p •«• V u = f. p among i <_ c ,' i f there f, f.. , . If not, then ""iFu^Cu, i ) . there are only a finite number of function symbols f f f i n i t e l i s t of axioms define the predicate ' Fun describe the set of n-ary function letters I Similarly, a thoery with predicate symbol constructed i n the same manner as the set of predicate letters The set of terms of be (J Fun^Cu, n). >Fun^(u, n) V Fm^Cu, n) . with predicate symbol 1' , so a x< X n * m' Since 1 X Fun(u, n)^ , then T_ 3 such that P , P. n *m 1 log W Pred T. with 4 P • .' m can be Pred describe i s also f i n i t e l y describable. 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 ). Let T^ - 22 - SeqnTerm(u, n|) —> 3v, w (SeqnTerm(v, n) A Term(w) A U = v * w) . It i s easy to see that T,. with the predicate symbol Term describe the set of terms, which i s the smallest set of words containing the variable symbols and constant symbols and having the property that i f D function symbol and t.. , I Let Tg be t are terms, then n Dt. * ... * t 1 n i s an n-ary i s a term. 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 i s 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 ( 3 u , v (Form(u) A Form(v) A w = uv)) V(3YJ T fi u with .Form (Var(y) A Form(u) A w = 3 y u ) V describe the set of formulas. ( 3 u (Form(u) A w = ~| Note that i n here, we - 23 - are using V uv instead of the ordinary notation u v v . This i s followed from Shoenfield's notation in Chapter II of Mathematical Logic. to avoid brackets in the formal language. The idea i s The usual notations are introduced later. To deal with free and bound occurrences of variables, we introduce the notion of subformulas. Let T_ be T n 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) —> Form(u) —> SubForm(u, w) . SubForm(u, u) . (u = v) V ( 3w (SubForm(u, w) A ImSub(w, v))) . SubForm(u, 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) t')) —> 3 v, w (SubForm(v, u) A v = 3yw A 7 (t = A 3P» Q» r, z ((s = pq V s = q) A (t = rz v t = r) A qyr = v )) . Sent(u) <—> Form(u) A Vy Tg with predicate symbol Sent (Notfree(y, u)) . describe the set of sentences. Construct an axiom which says that y i s a variable symbol and u i s a term and ImSubst(y, u, v, w) v holds i f f i s a formula and w is - obtained from v by substituting 24 - u for a free occurrence of y. Using ImSubst, and the same technique as constructing SubForm axiom which says u Subst(y, u, v, w) i s a term and v holds i f f i s a formula, and w of substitutions of u y ImSub, an i s a variable symbol and i s obtained from v by a chain for free occurrences of y . Then, construct an axiom which says that FinalSubst(y, u, v, w) holds and w y from has no free occurrences of y holds i f f Subst(y, u, v, w) and u i s substitutible for i n v. Then, l e t 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 ~ l w ) . 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 i s substitutible for x i n A a , no part of A of the form is free i n A . 3yB i f for each variable y occurring i n contains an occurrence of x which - 25 - Equax(u) <~> 3 > > y> > n x z (Nat (n) A Seg(n, x, y, z) v /s((Fun(n, v) A (u = x Pj j^j Vy Vz)) V (Pred(n, v) Au = x V l V y V z ) ) ) . T^Q with predicate symbol Let be Logax describe the set of logical axioms. 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 rule, association rule, cut rule and for the expansion rule, contraction 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 = V s V 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 —> A sequence of formulas i s a string of the form where iu are formulas. u = 3 xw —> u^ * S )) * ••. * U R , The set of sequence of formulas i s f i n i t e l y descri- bable using a predicate symbol SeqnForm and the theory T.^ which i s - 26 - defined i n a way similar to the description of the sequence of terms. Let formula and formula w. Proof(u, v, w) v be the predicate which holds i f f u i s a proof using possibly The predicate bing the predicate Proof Proof, The relation using a predicate symbol u is a as an additional axiom of the i s finitely describable. Before descri- we need two auxiliary notions. u < v between natural numbers is easily defined Less and the axioms : Nat(u) A 1 (u = 1) —> Nat(u) A. Nat(v) —> Less(l, u) . (Less(u, v) <—> Less(ul, vl)) . We also need the predicate Place(u, n, v) which holds i f f u i s til the n formula i n 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, n l , 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 symbol PRF which describe the predicate Proof. T^ with the predicate 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 PLAC(X, k, v) PLAC(y, H, v) A (ER(s, x) v CR(s, x) v AR(s, x)v TR(s x, y) V IR(s, x)))) A ( 3 m (PLAC(w, m, v) A 5 V t (lPLAC(t, m|, v))) . T^^ with predicate symbol A formula proof v of w provable from w using u. PRF finitely describes the predicate i s provable from the formula u as an axiom. Therefore, Let Thm(u, w) i f f there i s a holds i f f w Thm(u, w) <—> 3 v Proof(u, v, w). Proof i s finitely describable, we have shown that : 111.1 Theorem. Thm(u, w) u Proof. is Since is finitely enumerable. So the set of theorems is a finitely enumerable subset of log W . However, the set of theorems is not a f i n i t e l y describable subset of If W is an empty set, then the language we are using i s just the basic logic, denote 111.2 i t by Suppose Thm(u, | | P v A same theorem ) Thm(u, v) Thm(u, v) i s not finitely describable predicate. is finitely describable. Then by Theorem 1.2.4, i - finitely describable, and by another application of the s Thm(u, P J ^ J u ) *~lThm(u, P. I u ) |*l °f log . Theorem. The predicate Proof : T log W . ^IQO ' w i is finitely describable. i s finitely describable. t n By Theorem 1 . 2 . 1 So there exists a finite extension a unary predicate symbol (which can without loss of - 28 - generality be chosen to be P i i ) such that T| — P i • 1*1 iu iff 1*1. ~]Thm(u, P | J u) . A In here, T be T' U T log n by where can be chosen to be f i n i t e l y axiomo.tized. T' i s f i n i t e l y axiomatized. L, log r (ii) where a (uv)w = u(vw) ~] (a = b) for a l l pairs i s different from b . ( i i i ) ""j (au = b) for a l l pairs (iv) 1(au = bu) i s different from (v) T" One can replace T.. log J T" having the following axioms : (i) a For l e t T for a l l pairs (a, b) of constant symbols of (a, b) of constant symbols. (a, b) of constant symbols where b. (au = av <—> u = v) gives a finite l i s t of axioms. for a l l constant symbols Each axiom of a. T" i s true i n log, and T" i s 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 i s 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 T \J T" and expressing 1 the resulting sentence i n L, , we can find an element w of log such log' o that w [ P j ^ | u i f f "")Thm(u, ) f n j particular, l e t 6 o u u = w . Then, o w I o 1 o r a U t n P iiw i f f Thm(w , P i i w ), and so we have |*| o o' |*| o Thm(w , P i | w ) i f f ~J Thm(w , P i i w ) which i s impossible. o I *| o ' o I*| o ^ predicate Thm(u, v) is not f i n i t e l y describable. Hence the - 29 - III.3 Corollary. The predicate Thra(u) which holds i f f | — u , i s not a finitely describable predicate. Proof : Suppose Thm(u) defined as i s finitely describable, and let f(u, v) = u —> v . Then, by Theorem 1.2.4, Thm(u —> v) i s f i n i t e l y describable. Thm(u —> v) i f f J— —> v implies u describable implies above Theorem III.2, uj f be a function Thm(f(u, v)) = By the Deduction Theorem ([7], p. 33), v . So Thm(u —> v) Thm(u, v) i s also f i n i t e l y describable. Thm(u, v) i s not. Hence Thm(u) is finitely But by the i s not f i n i t e l y describable. Let Consist(u) be a unary predicate which holds i f f u is a consistent sentence . III. 4 Theorem. Consist(u) Proof : u where f i s not finitely describable. i s a consistent sentence i f f ~] (u | i s a sentence false i n a l l structure. f i n i t e l y describable, then f) i.e. ~\ Thm(u, f ) , So i f Consist(u) i s ~] Thm(u, f) i s also, and by Theorem 1.2.1, Thm(u, f) i s f i n i t e l y describable which i s proved to false by III.2 . Therefore the set of consistent sentences i s not finitely dgscribable . - 30 CHAPTER IV THE RELATION BETWEEN F I N I T E D E S C R I B A B I L I T Y 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 to more general ones. operation, where L^ Let IV.1 n 0 instead of and unary function symbol S and IT Any recursive function is f i n i t e l y describable on 0 0 W w i l l be an abbreviation for Theorem. and then go on be the natural numbers under the successor has constant symbol For convenience, write usual, W W, S . W instead of S. As I T n times S S ... S O f on the set of natural numbers W. Proof : We proceed by induction on the definition of recursive function. (1) Let f be the projection function l?(x , l 1 x ) = x. . Let n I F (x , x ) - x. . n 1 1 T. 1 be T W IT f(x^, X ) = R together with the axiom ° n It i s t r i v i a l to see that for any T.J i " , i.e. F (a) = f(a) .. For any model M 1 of a l l sentences of constructed such that 1^ true in M' is M W, of a_ = (a^, a) T^ U T , where a model M 1 for in n T T^ U T except for the interpretation W ., n is the set can be - 31 - F (a , . .., a ) = a. V 1 for a l l n-tuples. Hi n and hence for any sentence W . So f T f be 2 and Then for any = f(a^,a ) = + a 2 ai T then + , i.e. Suppose 2 in W, 2 we want to show that = f(a ,0) ± + 0 = a a;L 2 a 2 2 1 = f(a a ) • for a l l 2.* 2 a 2 a and hence for any sentence So f (3) Let T^ i n W Y of It: i s c l e a r 1^ , that if T1 T | a 2 F^a^O) 2 . By axioms 2 F^a^Sa^ 2 TI F^a^a^ 2 i s consistent \J T Y, 2 2 then T) 2 F (a^,a ) 2 = 0, 2 for some 2 Therefore, by induction, 2 T1 . Therefore ± T ( F ^ a ^ . a ^ = a^ + a 2 W . . 2 = S(a^ + a ) = a^ + (a + 1) . 1 } is true in f(x^,x ) = x^ + , T r — F (a ,Sa_,) = SF (a ,a ) . By assumption, 2 Y F^x^Sx^ = SF^x^x^ . a^, a and ± = f(a^,0) . of Y, . Proving by induction, suppose 2 F ( ,0) = a 2 i f T^j Is consistent together with the following axioms : 2 2 , be the addition function F (x,0) = x TI of T. U T 1 i s finitely describable. (2) . Let Let Y Therefore then Y is true in i s finitely describable. Let be f T 2 be the multiplication function., i.e. f(x^,x ) = 2 X -JL* 2 x together with the following axioms : F (x,0) = 0 and 3 F ^ x ^ S x ^ = F (F (x ,x ) .x^ 2 3 ]L 2 . With a similar proof as in (2), i t can be shown that for any a^,a 2 in sentence W, Y T^ | of F (a^,a ) = f(a^,a ). 3 1^ , T^l finitely describable. 2 2 Y implies Y It i s also clear that for any is true in W . So f is - 32 - (4) if Let f be the function 1^ , i . e . f(x^,x ) = K^Cx^x,,) =0 2 x^ < x^ and f(x^,x ) = K^Cx^x.^) = 1 otherwise. 2 Let be together with the following axioms : 1(« (x < 0) < Sx ) —> ( 1 2 2 1 1 < x ) —> F ( X]L 2 l(x 1 4 2 a F ( a , a ) =0 4 1 Therefore 2 2 T^| 2 2 X]L ,x ) = 0 < x ) —> F ( 4 For any -^>2 i T^j 2 < x ) v (x = x ) V (x < x ) (x ( < x ) V (2^ = x ) X;L a n 2 X ; L > x ) = SO . 2 ^, if a < a ]L x | 2 a^ < a and F^Ca^a^ = f C a ^ a ^ (5) W . Therefore 2 . So . It i s clear to see that Y of L^ , T^| Y T^ \J T implies Y f i s f i n i t e l y describable. Let f be a recursive function on the set of natural numbers defined as f C x ^ where i f f a^ < a F^Ca^a^ = 1 otherwise. is consistent and hence for any sentence is true in 2 g, h^, x > = gCh^x^ h^ are recursive. describable, l e t T , T ..... T, g l k n function symbols G, H^, ^ ( ^ J •••» x ), n Suppose g, h^, >) IT , with W that describe g, h^, h^ respectively. These theories can be chosen such that their languages have only common. Construct a finite extension N h^ are f i n i t e l y be finite extensions of T h X T,. of T w L^ i n , with function symbol - 33 - F such that T is T U T, U 1 8 axiom 1 = G(H^(a^, ;L n X R i n W , T_ I F (a,, . .. , a ) 5 5 1 n c 1 R T n T n^ n^ = gCh^a^ H^O^, •••> ) ) • a ) , . .., H^Ca^, . .., a )) . With the properties of theories c » v , » ' *' ' v , • ^ i g together with the additional \ ^O^, •••» \) = G(H (x , ..., x ) , For any a. , . . . , a I n T U T G ( i ( i > • • • > O » • • • » u( i » • • • . H a 1 5 . .., a ) , h^(a^> n a H n 1 k. 1 ..., a >) = f ( a , n )) a n a > . Hence , 1 n T,. | — F,. (a^, ..., a^) = f(a^, ..., a^) . By Lemma 1.2.2, T U T g h a model x U ... U T, h U T i s consistent, so for any model M' of T,. U T can be constructed such that for the additional interpretation F^ all Y n tuples. Therefore of 1^ , T I—Y 5 M of i t , k M' (t) = G^O*, (t), i s M except H (t)) for T^ U T is consistent and hence for any sentence implies Y i s true i n W . So f i s f i n i t e l y describable . (6) where x^) = yy(g(x^, Let f be defined by f(x^, g is recursive. Suppose r X l x ) = y) <-> (G( , n X;L x , y) = 0) A (Vz)((z < y) —> n -|(G(x , ..... x , z) = 0))) . 1 n be g. ¥, such o b (F ( , 6 y) =0), G that describes T, of T , , with function symbol o W T, is T U T, together with the additional axioms : 6 g 4 that n > g i s f i n i t e l y describable, l e t T a f i n i t e extension of T^ with a function symbol Construct a finite extension x - 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 i s g 6 6 1 n 1 n 1 Tg U Y clear that if T, |— Y , o then i s consistent and hence for any sentence Y i s true in W . So f Y of , i s f i n i t e l y describable. Hence recursiveness implies finitely describable on the special structure W . The converse of theorem IV.1 IV.2 Theorem. f If f : W n i s a f i n i t e l y describable function, then i s a recursive function. Proof : Since T —> W f is f i n i t e l y describable, there exists a finite extension of T^ , with function symbol Let F Ty , and T^ Let S(K(b),t,L(b)) S(a,t,y) where = f(t), T i s a finite extension T i s recursively Then P (a,g(t,y)) i s T holds. By substitution, are the "unpairing functions" (inverses of which are recursive. By the definition of recursive L(ub(S(K(b),t,L(b))) so F(t) = y. hold i f f P^,(a,g(t,y)) K, L the pairing function*) function, Since i s the index P^,(a,u) i s recursive. Define the function g g(t»y) = index of the sentence recursive. u. i s clearly recursively axiomatized, so axiomatized and therefore by that describes f . P^,(a,u) be the predicate which holds i f f a of a proof of the sentence with index of also holds : i s recursive. But L(ub(S(K(b),t,L(b))) f ( t ) i s recursive. * 1 The pairing function 2 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 f i n i t e describability and recursiveness in a more general setting. Definition : The structure W is f i n i t e l y describable i f TW is a finitely TT J 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 f i n i t e l y describable structure. Let Ind be an effective indexing of log . Then Ind(Ty) i s a recursive set of natural numbers. Proof : Since W i s finitely describable, there is a finite extension of T^og » i t h a unary predicate symbol R, such that for any or T I lR(u), and T|—R(u) iff u recursively axiomatized, and since is also recursively axiomatized. T| TT n By a standard result i f T of Theorems i s recursively enumerable. L^, , is recursively the set of indices But the set of formulas of the form is recursive, so the set of indices of theorems of the form recursively enumerable. R(u) Hence the set of indices of formulas is recursively enumerable. formulas u formula u, such that either T| Ti R(u) ~lR(u) or R(u) T . Now T. i s clearly W log i s a finite extension of T , T log T in axiomalized and Ind i s an effective indexing of R(u) u, T | w T u is such:that Similarly, the set of indices of is recursively enumerable. Tl R(u) ~lR(u) But for any 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 be a finitely describable subset of of , then Ind(S) Proof : Since extension T T I — R(u) or T^ of If Ind is an effective indexing is a recursive subset of T N n . i s a f i n i t e l y describable structure, there i s a finite T with a predicate symbol w T| lR(u), and u e S is recursively axiomatized. i s recursively enumerable. R T By lemma IV. 3, is a finite extension of Then the set of indices of theorems But the set of sentences of the form R(u) is recursive, so the set of indices of theorems of the form r.e. Hence the set of indices of Similarly, the set of indices of for any u. e W , 11 either of sentences of form of indices of T|— R(u), u such that Ind(S) u u such that such that T (—- R(u) R(u) 11 e such that for any i f f T|—R(u) . has a recursive set of indices, and since T^ , T of W S C or T| T) R(u) T 1— 7R(u) ~] R(u) R(u_) is is r.e. . i s r.e. . But and the set of indices is recursive, so by a standard result, the set T | R(u) is recursive. Since u e S iff i s recursive. An essentially f u l l converse of the above theorem can be stated as follows : IV.5 Theorem. Let W describable indexing of be a small structure, and let L . If S C W n and Ind Ind(S) be a f i n i t e l y is a recursive - 37 - subset of N , Proof : Since then S Ind(S) is a recursive subset of N i t follows that , by theorem IV.1, n Ind(S) i s a finitely describable subset of with predicate symbol describable, l e t T' T U T' i s a finitely describable subset of R describe Ind(S). Since with function symbol together with the axiom F Ind i s also f i n i t e l y describes R„ (x) <—> R(F(x)), N° . Let T Ind. Let where R T g be is a new predicate symbol. For any _t in W° , Ind(t) in N T|-— ~IR(Ind(_t)) . By the property of T*, T U T'1 or g implies that model M R S ( ^ ) • Also, T {— Rg(t) Tl R(Ind(t)) T U T' 1 — R(F(_t)) Tj—R(Ind(it)) or implies that i f f Ind(t_) or T | R (_t) i s in Ind(S) i f f t e S . It i s t r i v i a l to see that for any of T U T' U T , a model So for any sentence Y S , so !R(F(t)) , The additional axiom of T 1 T l n M* of • 1^ , S ^ ~ T Y can be constructed for T i m P l i e s Y i s t r u e i n w g U T . • Hence i s f i n i t e l y describable. Like the equivalences between finite describability and recursiveness, the notion of f i n i t e l y enumerable i s essentially equivalent to the notion of recursively enumerable. It can be stated as follows : IV.6 Corollary. be a finitely describable structure, and let . S C Let W be f i n i t e l y enumerable. Ind(S) If Ind i s an effective indexing of i s a recursively enumerable subset of N A converse of IV.6 can be stated as : n . L^ , then w n - 38 - IV.7 Corollary. Let W describable indexing of enumerable, then S be a small structure, and let Ind L^ . If S C W n 7 , and i s finitely enumerable. Ind(S) be a f i n i t e l y is recursively - 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, A. Yasuhara, Mathematical Logic, Addison-Wesley, Mass. 1967. Recursive Function Theory and Logic, New York, 1971. Academic Press,
- Library Home /
- Search Collections /
- Open Collections /
- Browse Collections /
- UBC Theses and Dissertations /
- Another notion of recursiveness
Open Collections
UBC Theses and Dissertations
Featured Collection
UBC Theses and Dissertations
Another notion of recursiveness Yeung, Stella Mei-Yee 1973
pdf
Page Metadata
Item Metadata
Title | Another notion of recursiveness |
Creator |
Yeung, Stella Mei-Yee |
Publisher | University of British Columbia |
Date Issued | 1973 |
Description | 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 slightly together. |
Subject |
Recursive functions |
Genre |
Thesis/Dissertation |
Type |
Text |
Language | eng |
Date Available | 2011-05-06 |
Provider | Vancouver : University of British Columbia Library |
Rights | For non-commercial purposes only, such as research, private study and education. Additional conditions apply, see Terms of Use https://open.library.ubc.ca/terms_of_use. |
DOI | 10.14288/1.0302221 |
URI | http://hdl.handle.net/2429/34303 |
Degree |
Master of Arts - MA |
Program |
Mathematics |
Affiliation |
Science, Faculty of Mathematics, Department of |
Degree Grantor | University of British Columbia |
Campus |
UBCV |
Scholarly Level | Graduate |
Aggregated Source Repository | DSpace |
Download
- Media
- 831-UBC_1973_A8 Y49_5.pdf [ 2.06MB ]
- Metadata
- JSON: 831-1.0302221.json
- JSON-LD: 831-1.0302221-ld.json
- RDF/XML (Pretty): 831-1.0302221-rdf.xml
- RDF/JSON: 831-1.0302221-rdf.json
- Turtle: 831-1.0302221-turtle.txt
- N-Triples: 831-1.0302221-rdf-ntriples.txt
- Original Record: 831-1.0302221-source.json
- Full Text
- 831-1.0302221-fulltext.txt
- Citation
- 831-1.0302221.ris
Full Text
Cite
Citation Scheme:
Usage Statistics
Share
Embed
Customize your widget with the following options, then copy and paste the code below into the HTML
of your page to embed this item in your website.
<div id="ubcOpenCollectionsWidgetDisplay">
<script id="ubcOpenCollectionsWidget"
src="{[{embed.src}]}"
data-item="{[{embed.item}]}"
data-collection="{[{embed.collection}]}"
data-metadata="{[{embed.showMetadata}]}"
data-width="{[{embed.width}]}"
async >
</script>
</div>
Our image viewer uses the IIIF 2.0 standard.
To load this item in other compatible viewers, use this url:
http://iiif.library.ubc.ca/presentation/dsp.831.1-0302221/manifest