Annals of Pure and Applied North-Holland

Logic 52 (1991) 249-308

249

Generalizing classical and effective model theory in theories of operations and classes
Paolo Mancosu
Subfaculty of Philosophy, Wolfson College, Oxford University, Oxford, United Kingdom OX2 6lJD Communicated by D. van Dalen Received 6 July 1989

Abstract Mancosu, P., Generalizing classical and effective model theory classes, Annals of Pure and Applied Logic 52 (1991) 249-308. in theories of operations and

In this paper I propose a family of theories of operations and classes with the aim of developing abstract versions of model-theoretic results. The systems are closely related to those introduced and already used by Feferman for developing his program of explicit mathematics. The theories in question are two-sorted, with one kind of variable for individuals and the other for classes. The individual variables range over a domain closed under pairing and containing, among other things, natural numbers and (partial) operations. All the theories used assume a common group of axioms that insure that the individuals in the domain satisfy the conditions for a partial combinatory (applicative) algebra with pairing. We also assume a class N of natural numbers and a class induction axiom on N. Finally there are various class existence axioms. I work mainly with three theories, FMT,, FMT and FMT,, which differ from each other both in their class existence axioms as well as in some further applicative axioms. These theories have various interpretations in which every object is explicitly presented by some means of definition as well as classical, or standard, set-theoretical interpretation. The systems are formulated in a flexible general language which can be used to prove abstract theorems of mathematics (analysis, algebra, model theory, etc.), thereby (depending on the system) generalizing recursive, hyperarithmetic and admissible versions of classical mathematics. The aim of my work is to give an abstract development of portions of model theory in the afore-mentioned theories, in a way to look as much as possible like classical mathematics. Thus, FMT, generalizes portions of countable and recursive model theory; FMT further generalizes portions of countable and hyperarithmetical model theory and finally FMT, provides a generalization of the classical L(Q)- completeness theorem and of an admissible version of L(Q)-completeness due to Bruce and Keisler. This continues the development of the program mentioned above, originating with Feferman.

1. Effective

analogues

for model theory and explicit model theory

for

In the past twenty years we have witnessed the emergence of several analogues set-theoretical model theory, viz. recursive (or decidable), arithmetic,
0 1991Elsevier Science Publishers B.V. (North-Holland)

0168-0072/91/$03.50

250

P. Mancosu

hyperarithmetic and admissible model theory. The motivations for pursuing these enterprises differ technically and philosophically. From the latter point of view, some work in recursive model theory has been fostered by interest in constructive mathematics and especially in constructive algebra (see [lo]), while the work in hyperarithmetic model theory was explicitly motivated at the outset by predicativist concerns (see [9, 121). From the technical point of view the adjectives attached to each analogue development give a hint of the kinds of techniques used to establish the relevant results. In this introduction I will give a sketchy overview of each one of the above-mentioned analogues for set-theoretical model theory. I will then develop abstractly, using suitable theories of operations and classes, a unified model theory encompassing portions of each one of the mentioned analogues. This develops a program initiated for uncountable model theory in [19] and for countable model theory in [20]. By set-theoretical (or classical) model theory I mean here the usual development of model theory in ZFC as found, for example, in [7]. Many parts of model theory do not require the full strength of ZFC. However, there are parts of model theory which make heavy use of the machinery provided by the transfinite theory of ordinals and cardinals, axiom of choice and the continuum hypothesis. Sometimes this machinery is used as a tool for obtaining results of a more elementary nature. Recent work [2,36] has shown that the use, for example, of saturated and special models can be eliminated in some proofs of elementary results for countable structures by using countable recursively saturated structures. This opens the way for the development of countable model theory. Typical results in this area are the completeness theorem for countable theories, existence under suitable conditions of countable prime models and of countable saturated models, and certain results in stability theory. Results which are clearly outside this area are the Lowenheim-Skolem theorem, general existence theorems for saturated models, results on ultraproducts, categoricity in uncountable powers, etc. Many of the analogue developments rest on intuitive analogies concerning the notation of countability. Recursive and hyperarithmetic model theory have their analogy and countable starting point in the countable - recursive hyperurithmetic, respectively. Other developments in #-model theory and admissible model theory were set up with the idea of providing a natural analogue for the opposition countable/cardinality SK,. We now turn to the description of these analogue developments. It is difficult to say when recursive model theory began. The result that every decidable theory has a decidable model has been part of the folklore for quite a long time and it is an almost immediate corollary of the lemma found in [40, p. 151 to the effect that every decidable consistent theory has a decidable complete consistent extension. A decidable model is defined to be a structure A such that Th(A, (I)_~ is recursive. In other words, A is decidable if { (9, a): A k +[a]} is a recursive set. This definition is due to [33, p. 2331. The subject of recursive model theory has

Generalizing classical and effective model theory

251

been developed extensively in the West through work of Harrington, Millar, Morley, and in the Soviet Union through work of Ershov, Goncharov and others (for an overview, see [15,31]). There are a number of classical results for countable model theory that hold in the recursive analogue. The following are paradigm examples. Fact 1R. A consistent decidable Fact 2R. Each recursive
theory has a decidable model. decidable theory is

nonprincipal type of a complete omitted from some decidable model of that theory.

Fact 3R. A decidable

lzkt of the principal

theory types.

T has a decidable

prime model iff there is a recursive

In recursive model theory many of the classical notions are retained in their classical sense and not relativized. This feature of recursive model theory makes it problematic for a more abstract development. For example, in decidable model theory a decidable prime model is defined to be a decidable model that is (classically) embeddable in every model of the theory. I will take another line of approach: an A-prime model is taken to be one which is A-embeddable in any A-model of the theory, where A represents the universe of objects dealt with in the analogue. Thus, in this account, a decidable prime model is a model that is recursively embeddable in any decidable model of the theory. Considering this reformulation I part company with much of recursive model theory in which a mix of recursive and classical notions is often adopted. My rendering of the analogues will be such that once we interpret a model-theoretic result in one of the interpretations of the metatheory, then we will be immersed, so to speak, in a purely analogue-universe (be it recursive, hyperarithmetic or admissible) without being able to see what happens classically unless we switch to the classical interpretation. This point of view is very close to what happens in Cutlands hyperarithmetic and admissible analogues to which I now turn. Hyperarithmetic model theory was initiated by Cleave [8,9] and later pursued by Cutland in his dissertation [12]. Cleave developed the hyperarithmetic analogue program for ultraproducts and saturated models, and for results connected with real closed fields. This analogue was developed further for portions of countable model theory in the first part of Cutlands dissertation [12, pp. l-791. Cutland showed how to give a hyperarithmetic treatment of the completeness, omitting types and prime model theorems and several results on saturated models. Cutland was also very careful in exploring alternative ways in which one could develop hyperarithmetic analogues of classical notions. A structure A is called hyperarithmetic if the set of natural numbers that codes it in one of the standard fashions is hyperarithmetic. There is no need to require the satisfaction relation to be hyperarithmetic since there is a recursive function that from a code for A and L gives a code for the satisfaction relation on A,

252

P. Mancosu

thereby showing that the satisfaction relation on a hyperarithmetic structure is hyperarithmetic. This is analogous to the classical case where the satisfaction relation for a countable structure is immediately seen to be countable. Here are some typical theorems which are provable in this analogue. Fact 1H. A consistent hyperarithmetic
theory has a hyperarithmetic model.

Fact 2H. Each hyperarithmetic nonprincipal

type of a complete hyperarithmetic theory is omitted from some hyperarithmetic model of that theory.

Define a hyperarithmetic structure A to be h-prime iff A is hyperarithmetically embeddable in any hyperarithmetic structure B =A. Then the next fact follows. Fact 3H. A hyperarithmetic structure is h-prime iff it is atomic. Fact 4H. Zf T is atomic, then there exists a hyperarithmetic h-prime model A of T. Cutland also provided analogues for the Lowenheim-Skolem theorem and various theorems on saturated models making essential use of the hierarchy provided by the constructive ordinals. The underlying analogy used in the latter facts is countable -bounded in HYP. The second part of Cutlands dissertation was devoted to an analogue development that he called Z7:-model theory (for a published account see [13]). Whereas in the hyperarithmetic analogue the only structures considered were hyperarithmetic structures, in the I7:-development one looks at structures whose complexity in terms of the analytical hierarchy is n:. Unlike hyperarithmetic model theory where a hyperarithmetic structure has automatically a hyperarithmetic satisfaction relation, the corresponding statement is false for I7:-structures; thus in II:-model theory one restricts attention to I7:-structures whose satisfaction relation is also #. Such structures were called by Cutland covered I7:-structures and when the structure is properly n: (i.e., not A:), then we talk of properly covered I$structures. The basis for Cutlands analogue development in II7:-model theory is that the Z7:-A: sets correspond classically to sets of cardinality K1 and the hyperarithmetic sets correspond to countable sets. In this framework Cutland considered natural analogues for (a) the downward Liiwenheim-Skolem theorem, (b) the Ehrenfeucht-Mostowski theorem, (c) Vaughts two-cardinal theorem, (d) results on X1-categoricity, (e) results on saturated models, etc. The development of I7:-model theory was successful, but up to this point the reasons for the success of such analogues were still hidden. With the emergence of admissible set theory a much deeper insight was obtained into the analogies. Cutland then recast his previous work in the more natural and general setting provided by admissible set theory. In particular, he recast model theory on hyperarithmetic sets as a development of model theory in L,;L (constructible sets

Generalizing

classical and effective model theory

253

up to recursive or) which is identical to the class of hereditarily hyperarithmetic sets (HH). II:-structures are then structures which are z1 on HH and then one studies structures whose satisfaction relation is also & on HH. Cutland [14] extended the setting to any admissible set (with o(M) > w) satisfying &-global well ordering (&GWO). This condition asserts that there exists a 2:,(M) map f :o(M)+ M which is one-one and onto. When M is a locally countable admissible set (i.e., every element of M is countable in M) satisfying &-GWO and o(M) > co, one obtains an analogue development in which the sets in M correspond to the countable sets and sets 2r over M correspond to sets of power SK,. Cutland then redeveloped his previous analogue in this setting by considering models A whose satisfaction relation is E, on M. This development is called
model theory on admissible sets.

The above definitions and comparisons have been introduced to make plausible and more understandable the general approach followed by Feferman in his work on generalizations of classical model theory and model theory on admissible sets. In [19] Feferman stressed the need to give an abstract account for the successful analogue developments developed by Cutland. It is therefore important to be clear on what we have to account for. It seems to me that different analogue developments pursue different goals and are driven by different insights and analogies. I think it is important to distinguish two different types of analogies which emerge from the above described developments. The first type of analogy is the one pursued in portions of recursive model theory and hyperarithmetic model theory. This approach centers around the correspondence between recursive or hyperarithmetic and countable. Here one compares a classical notion (countability) with different effective notions (recursive or hyperarithmetic). The second type of analogy is the one that emerges from Di-model theory and model theory on admissible sets. Here we compare a pair of classical notions (countable vs. cardinality SK,) with a pair of effective notions (A: vs. nt, in II:-model theory, and countable in M vs. Z,(M), in admissible model theory). Feferman [19] accounted for the second type of development. There he proposed a theory Tn of operations, classes and ordinals and introduced the central notion of Q-valuated model. Sz denotes a class whose members satisfy several axioms for ordinals and is such that o E 52. A class A is Q-enumerable (o-enumerable) if there exists a function which sends S2 (w) onto A. Feferman then showed how to associate with each model K LZFC and each locally countable admissible set M satisfying &-global well ordering, associated models K* and M* such that K* L Tn and M* I=Tn. In particular the class constant Sz is interpreted as K1 in the classical model and as o(M) in the admissible model. K* and M* were shown to have the following properties: A is o-enumerable in K* iff A is countable in K; A is O-enumerable in K* iff IAl s K1;

254

P. Mancosu

in M* iff A is countable in M; in M* iff A is .Z1 on M. A structure A = (A, Ro.. .R,) is said to be G-enumerable iff the domain and each of the relations are a-enumerable. An D-enumerated structure is said to be Q-valuated iff the satisfaction relation on A is Q-enumerable. Thus, under the previous interpretations, any theorem of TQ about Q-valuated structures generalizes at once an analogue theorem in admissible model theory and a classical theorem. In the classical sense an a-enumerable structure is automatically &?-valuated but this is not true in the admissible analogue where &?-valuated structures correspond to models A in M where LA is Z1 on M. This program was developed by Feferman with special emphasis on saturated structures. This kind of approach is extended in the present work in two different directions. In one direction the program will be pursued further by using a theory very similar to Tn in which one can prove an abstract version of the completeness theorem for L(Q) (Q is the quantifier there exist uncountably many). This generalizes (see Section 4) the classical L(Q)-completeness theorem and an admissible development due to Bruce and Keisler [4] and extended by Wimmers A is o-enumerable
A is Q-enumerable

[All.
The second direction originated from [20]. In that paper Feferman developed a certain amount of countable model theory in a second-order theory of individuals and classes called FM. A weaker theory FM, was also studied, which was sufficient for the development of an interesting amount of metamathematics. In [20, p. 1221 a valuated model is defined to be a model whose satisfaction relation is a class in FM. I will introduce the notion of o-valuated model which is, in my opinion, a satisfactory notion for accounting for portions of model theory which have been developed according to the first type of analogy I described above. A structure A is said to be w-enumerable iff its domain and each of its relations are u-enumerable. An o-enumerable structure is said to be o-valuated iff the satisfaction relation on A is w-enumerable. Classically (hyperarithmetically) every w-enumerable structure is o-valuated since the satisfaction relation for a countable (hyperarithmetic) structure is countable (hyperarithmetic). In the recursive analogue o-valuated models correspond to decidable models. I will propose a theory FMT, in which to account for the first type of analogy I described: countable - recursive or hyperarithmetic. Furthermore a strengthening of FMT,,, FMT, will be considered in which one can provide a better treatment for the analogy countable - hyperarithmetic. I develop to begin within FMT,, and further in FMT, a certain amount of w-valuated model theory thereby generalizing results on completeness, omitting types, atomic and prime models, saturated models, etc. This development is contained in Sections 2 and 3. The conceptual motivations and the technical choices I have made are very much in line with Fefermans program of explicitmathematics. Since 1975 Feferman has developed several systems of operations and classes

Generalizing classical and effective model theory

255

which embody three main tenets: (a) the systems have various interpretations in which every object is explicitly presented by some means of definition; (b) the systems also have a classical interpretation; (c) the systems provide a flexible general language in which to prove abstract theorems of mathematics (algebra, analysis, model theory, etc.) thereby (depending on the system) generalizing constructive, recursive, predicative, hyperarithmetic and versions of classical mathematics. One origin of this program was to give a logical account of Bishops style of constructive mathematics; Bishops work made people realize that constructive mathematics could equally well be read as a piece of classical mathematics. Although different from Bishops approach in many respects the program envisaged in explicit mathematics is that of making the development of mathematics look as much as possible like classical mathematics and yet having a variety of explicit interpretations. In a lecture on explicit mathematics in Rome, May 1987, Feferman described his approach as follows: First of all I want it to be abstract because I do not want to say, we are talking just about recursive things, hyperarithmetic things, . . . , because that is a restriction to the way mathematicians look at their subject. If it is to be the way mathematicians look at it, it has to be formulated in a way that looks as general as mathematics looks to the mathematician. [...I And secondly, the mathematician should be able to look at this and see that if a theorem is proved it sounds like a theorem that he knows, not that it is an analogue of a theorem that he knows. . . So that is why I emphasize that the approach should be abstract. I would also add that the proof should sound like a proof that he knows. The flexibility and the abstract development provided by systems 5 la Feferman are the main reasons for which I feel compelled in my work to follow the path opened by him. The present work is therefore intended to be a contribution to the program of explicit mathematics. 2. Generalizing countable and recursive versions of model theory In the following, I will present an abstract theory of operations and classes, FMT,, which will be my base theory for developing abstract theorems of model theory. The emphasis will be in looking at some paradigm cases and not in pushing the program as far as possible. After developing basic syntax and semantics in FMT,, I will show how to prove in the same theory abstract versions of the completeness theorem, the omitting types theorem and results on atomic and prime models. We meet limitations to this part of the program when we come to saturated models. Analysis of this situation shows the need to strengthen the theory (which is extremely weak as we shall see) with new axioms in order to capture some of the unprovable theorems. Naturally, we may expect that every time we do this we lose some of the analogues since the stronger the theory the

256

P. Mancosu

more we cut down on the number of its interpretations (and therefore the number of analogues). By an interpretation of FMT,, we mean a model of FMT, considered externally, i.e., in the informal sense. The word model will be used formally in FMT, for structures (identified with certain classes) which satisfy the definition of being a model for a first-order language, or for the corresponding structures in interpretations of FMT,. 2.1. The theory FMT,; language and axioms FMT,, is a theory of operations and classes which combines features of Fefermans theory EM, [18, p. 1841 without the ontological axiom, and his FM,, (see [20, pp. 97-991). The theory is formulated in a two-sorted language. The universe of individuals contains, among other things, numbers and operations which may be thought of as explicitly presented objects. In particular, there are basic (combinatory) operations for closure under explicit definition, pairing and projection operations, a definition-by-cases operation, and operations for successor and predecessor on natural numbers.
The language of FMT,

We have two sorts of variables, one for individuals and one for classes.
Individual variables: a, b, c, . . . , x, y, z. Class variables: A, B, C, . . . , X, Y, 2. Logical constants: A, v, 7, +=, V, 3. Individual constants: k and s are the symbols for the combinators representing the operation producing constant functions and substitution, respectively. d stands for definition-by-cases over the universe. p, pl, p2 stand for pairing and left and right projection. Finally, we have a symbol 0 for zero and sN, pN for successor and predecessor on N. Relational constants: App stands for a ternary relation on the universe. App(tl, t2, t3), where tl, tZ, t3 are terms, intuitively means that the operation tl applied to t2 yields the value t3. The symbol E represents the relation of is classified under. So tl E W, where W is a class term, means that the individual tl is classified under the class W. We also have a relation symbol = standing for equality and a relation cN standing for less than on N. We often abbreviate

ApI&,

t2>f3) by tit2 = 13.

Terms: We need to distinguish class terms and individual terms, as follows. Individual terms: Individual variables and individual constants. Class terms: N is a class term. Each class variable is a class term. Atomic formulas: If tl, t2, t3 are terms, then tl = t2, tl CNt2, App(tl, t2, t3), tl E W (where W is a class variable or constant) are atomic formulas. Formulas: Obtained by adding to the atomic formulas equations of the form

X = Y and closing under each connective and quantification of both sorts. Extended atomic formulas: Obtained by adding to the atomic formulas those of the form x #y.

Generalizing classical and effective model theory

251

3+-formulas: Obtained by closing the class of extended atomic formulas under A, v, bounded numerical quantification and existential quantification over individuals. Application terms: We now expand the syntax of FMT,, to allow so-called application terms. Individual terms are application terms. If ti, f2 are application terms, then (tlt2) is an application term. Application terms may not have a value. Relations between application terms are explained as formulas in L(FMT,J as follows. We first define t1 = t recursively on r1 by
tl = 2,

if t, is a variable or a constant,

(4 = 2) :=

3x, y [(t* =x) A (r3 = Y) A APP+, Y, z)l { if t1 is an application term (f2t3), where x, y are new variables.
tJ : = 3x (t, = x),

We then define 4 = t* : = vx [t1 =x ++ t2 =x],

tEW:=3x(t=xAxEW).

We will omit parentheses when dealing with application instead of (flf2). In general tlf2...rn stands for (tlt2...tn_&.

terms and write tlr2

Remark. tJ and t ==x are 3+-formulas but r1 = c2 is not. We write f1 = t2 for ti = t2 when tlJ or t2J is already known. The logic is assumed to be classical two-sorted predicate logic with equality.
Axioms for

FMT,, The axioms are divided into three categories. Roughly, the applicative axioms determine the use of the individual constants and state uniqueness for the App-relation; the N-axioms state induction and the least-element principle for classes; finally, the class (comprehension) axioms will tell us which classes are assumed to exist. (1) APP-uxioms k&J A kub = a; (Constant operations) SUbi A SUbC = UC(bC); (Substitution) (Pairing) pu,u,i /\pluA ~p,ui ~ p ~(p u ~ u ,) =ui (for i = 0, 1); (Definition by cases) dubcd~~(c=d-+dabcd=u)A(c#d-+dabcd=b); (Successor) U,bE~+(sNu~ApNU~A&,&U)=U)A(s,u#O); (Unicity) App(u, b, c) A App(u, b, d)+ c = d. Any structure which satisfies APP is called an APP-structure (or applicative structure). (2) N-axioms (a) O~NAV~(XEN+S~XEN); (b) (ClassinductiononN).O~X~~x(x~X~~~x~X)~~x(x~~~x~X); (c) (Least-element principle). 3x E N (x E X)-* 3x E N (x E X A d y < ~ X l(y E

X ));

258

P. Mancosu

(d) x<Ny-+~~N~y~N; (e) i(x<NO)A(~<NsNy*x<Ny vx=y); (3) Class existence (3+-comprehension axiom). For each 3+-formula 3x Vx (x E x f, e(x))< This concludes the description of FMT,,.

#(x),

Remark. The least-element principle follows from class induction only in the presence of stronger comprehension axioms, including closure under complementation. 2.2. Consequences of the axioms In this section we review first some of the consequences of the axioms for class existence, then of the APP-axioms and finally relate, after having determined the proof-theoretic strength of FMT,, the two kinds of axioms through the essential notions of o-enumerable and D-classes. Notational conventions. Let X G Y stand for Vx (x E X+x E Y). Define X = Y, the relation of extensional equivalence, to be X E Y A YE X. By EXT (extensionality) we mean the statement VX VY (X = Y+ X = Y). Although FMT, + EXT is consistent, we will not assume extensionality in what follows. This allows consistency with Fefermans theories some of which disprove EXT. We write
f :A*B f:A%B f:AsB

for Vx (x E A - fx E B), for(f:A

--+B)/\VyEB3xEA(fx=y),

for(f:A+B)AVx,yEA(x#y+fx#fY).

Various classes A come equipped with an equivalence relation =A G A*. Since we are not assuming EXT we cannot in general obtain quotients A/=*. The preceding notation is extended to such classes as follows. We write
f : (A/=,+ (B/E~) (B/sB)

forf:A-*B~Vx,yEA(x=~y+fx=~fv), for f : (A/=J(B/ss)

A

f:(A/Q=% The notions of l-l fashion.

Vz E B 3x E A (fx =B z).

mapping and l-l

onto mapping are defined in a similar

Elementary classes. The following classes are proved to exist in FMT,.

U= {x 1x f @ix, p2x)> (where (ri, f2) :=&fJ; V={xlx=x}; 0= {x Ixfx}; {Xl, * * .,x}={x~x=x,v*~~vx=x,}; v - {Xi, . . . , X ,} = { X ~ X # X , A-A X f X ,};
X X Y = { X I X =(p , X , p 2 X ) A p l X E X A p 2 X E Y }; D a m(x) = {X 13~

(x, Y) E X1 ;

x n Y = { X l X E x A y E Y };

Generalizing classical and effective model theory

259

XUY={x~xEXVyEY};

A=A~A~...xA(ntimes);
A <w={xIx=(plx,p zx ) A p 2x E N A Vk<j,rp2x[p1xk~ ~p,xk EA]};

XOY={O}XXU{~}XY,

wherel:=sNO.

Y=Y. Then (X, Y):= Note. X CD is such that X 0 Y A X 0 Y +X=Xr\ Y X 0 Y acts like ordered pair of classes up to =. k-ary relations on a class A are identified with subclasses of Ak.
Consequences of the APP-axioms

The following results are proved in [16, pp. 95,961 (cf. [3, p. 1011). (1) Introduction of A terms. With each application term t and variable x, we can associate a new term t* with the same variables except for x such that APP k t*i A vx
t*
[t*X

t ].

will be written Ax.t[x].

(a) Zf tisx, then Ax.t:=skk; (b) if t fx and t is a variable or a constant, then Ax.t := kt;
(c) if t is of the form t1t2, then Ax. t : = s(Ax. t,)(Ax. t2).

Proof. (a) skkx = kx(kx) =x; (b) ktx =t;

(c) st:t;x = (tfx)(t2*x) = t1t2. cl

(2) Recursion on V. There is a term RY such that APP proves

R,f 5 A [g = R,f + Vx (gx =fgx)].

Proof. Let h = )LyAxf(yy)x. Thus hyi for all y. Then hhi and hh = Ax.(f (hh)x). Hence g = hh serves as R,f. Take R, to be Ac ((Aytif (yy)x)(Ayhf (yy)x)). Cl This result is also called the recursion theorem.
of App + N-axioms Primitive recursive functions can be introduced using The N-axioms are used to show that the fixed points defining equations for the derived functions. Let m, restricted to the class N. The following are well-known axioms (see [3, p. 1033, [16, p. 981). Consequences

the recursion theorem. so defined satisfy the n stand for variables results about App + N-

(3) Primitive recursion. There exists a term PR such that for all g and h with f = PR(g, h), f satisfies the primitive recursion scheme
f (x9 0) = g(x), f(x, snn) = h(x, n, f(x, n)).

260

P. Mancosu

The idea of the proof is that f is defined by cases, using RV, with f(x, n) = g(x) if it = 0 and f(x, n) = h(,lc,PNn, f(x, p@)) otherwise. Note that if g : N+ V, h:N*xV+V, thenf:N*+V. (4) Minimum.
There exists a ferm c such that cg is pm(g(m) = 0) for each total function g : N + N. Thus, FMT,, proves

(g:f+-+N)~[cg~AcgElG+3m(g(m)=o)] A [cg E N+VY < (cg)1(g(y) = 0) A (g(cg) = O)]. We use this result mainly in the form of selection on N: f:N+NA%EN(fX=O) +
(CfENAf(Cf)=o).

From the above it follows that we have the next statement. (5) Pairing on N. There are operations f(f(ml, mJ) = mi for mi E N and i E (0, l}.
f, fi, f2 such that f : N*+ N and

will be denoted in what follows by the standard bracket notation We will use in the following some standard properties of well-behaved pairing functions as, for example, m, n <N (m, n).
m) (n, m).

f (n,

(6) The relation < on N is decidable.

m,nEN +

There is u term 1 such that

(Imn=0vZmn=1)~(Imn=0t,m<,n).

(7) Bounded quantification. Using primitive recursion on N we can define a term b which decides bounded numerical quantification :
f:kd-,NAnEk, +

bnflA[bnf

=ovbnf

=l]A[bnf

=o~vm<,n(fm=0)].

Proof -theoretic strength of FMT,

We want to compare the proof-theoretic strength of FMT,, with that of a subsystem of PA. Let PA-+Zy - IND be the subsystem of PA which has induction restricted to 2: formulas. To be more precise, PA- consists of the following axioms: (1) VX (x+0=x); (2) vx (x + y = (x + y)); (3) vx (x0 = 0); (4) vx (xy = (xy) +x); (5) Vx1(O=x); (6) Vx, y (x =y+x =y). Then we take .X7- IND : #(o)
A ix (G(x)-+ qb(x))-+Vx $(x),

where C#J g. is In [30, pp. 25-271 one can find the proof of the following theorem.
Theorem 2.2.1. FMT,, = PA- + 2: - IND.

Generalizing

classical and effective model theory

261

Corollary 2.2.2. FMT, is a conservative extension of PRA for z Proof.

sentences.

Use Parsons theorem [34] to the effect that 0 conservative extension of PRA for @ sentences.
w-enumerable and D-classes Definition 3f:N=+B. Lemma 2.2.4. Let A, w-enumerable. B be w-enumerable.

PA- + 2: - IND

is a

2.2.3. A class B is said to be o-enumerable

iff B is empty

or

Then A fl B, A U B,

A X B are

Proof. We prove it for A U B. Suppose f : N % f (n/2), h(n) = (g((n - 1)/2),

A and g : N %

B. Define

if n is even, if n is odd.
q

Then h is the required function from N onto A U B.

Remark 2.2.5. In what follows we will often need to use for any w-enumerable class A, an w-enumeration of the finite tuples from A. There are two different ways to proceed depending on the construction of the class of finite tuples of an o-enumerable set. One possibility is to use the definition of A<. This class may not be o-enumerable since we do not have an w-enumeration of all functions totally defined on finite initial segments of the natural numbers. In this case one works with the class (A, A+) where A<Uis such that (f, n) =A<W(g, m) f, n = m A vi CN n[fi = gi]. Here an w-enumeration of (A, =A<W) is a function f :N % A40/A<w, i.e., f is onto up to =A<O. If x EA<O, the length of x, lb(x), is simply p2(x). Alternatively, when A is W-enumerable, one can exploit the well-known l-l primitive recursive onto-mapping from N to its finite tuples; consider A as coding its finite tuples by simply pulling back to N, whenever we need to compute which tuple a specific element a EA codes. In this case the length function is given by the standard lh function for n-tuples of N. In other words, when a class is wenumerable, we can treat it informally as if it were N and thus exploit the standard coding of sequences in /V. In the development of model theory I will think informally of n-tuples of w-enumerable sets as given in this second way. I will also use N to denote this alternative representation of finite tuples. Uniformization and choice for w-enumerable classes

The following facts are easy consequences

of the existence of a selector given Thenwehave

by c. Let (*) denote the hypothesis 3g (g : N aR)r\RcAxB. the next theorem.

262

P. Mancosu 2.2.6. (*)-, If Vx (3y (x, y) E R +fx E B A (x, fx) E R).

Theorem Proof.

and RcAxB. Then, (a,b)~Rc;,3n~N (gn=(u,b)). Let g : N %R The idea is to look for the least it such that a is the first coordinate of g(n) and then fu is simply the second coordinate of g(n). More formally,
3y((a,y)~R) c* 3nEN(p,(gn)=a) t* 3n~N(hn=a) =s 3n~N(h,un=O),

where h = Az.pI(gz), and hoan = 0 t* hn = a where ha : = Au. Az.dOl(hz)u. Since for a E A, h,,u is total on N, we can apply selection on N. Let fi := Au.c(h,u). Hence, 3n E N (h,-,un= O)+fiu E N A h,,u(fiu) = 0. Finally letf := I.u.p2(g(fIu)). Cl
Corollary 2.2.7. (x7 fx) E 31. Proof. Apply Theorem

[(*) A (3

: N onto\ B)] +

[3fVx

(3y E B ((x, y) E R)--+fx

EB A

2.2.6 to the relation RI = (Dam(R) is o-enumerable (use pl: R %

B) fl R. Since R is

w-enumerable, w-enumerable.
corouary

Dam(R) Cl

Dam(R)).

Thus R, is

2.2.8.
[(*) A (ah : N -

B)]

Proof. Immediate R)dfx~B~(x,fx)~R.

from Corollary
Cl

2.2.7. since x E A implies 3y E B ((x, y) E

Definition 2.2.9. A class A is said to be decidable or determinate if function d such that d :V+ (0, and x E A t-, dx = 0. A class A l} determinate relative to a class B if A c B and we have a function such that for x E B, u!x = 0 t*x E A. Henceforth a determinate class

there exists a is said to be d : B+ (0, l} will be called

a D-class.
Theorem 2.2.10 (Generalized Posts theorem). Zf A c B is w-enumerable B - A is w-enumerable, then A is a D-class with respect to B. Proof. We and

want an f such that x E B + (fx = 0 v fx = 1) A (fx = 0 *x E A). Apply Theorem 2.2.6 to the relation R = A 0 (B -A), where R c B X (0, l}. Then there exists an f such that for an arbitrary x E B, 3y ((x, y) E R)+ fx E (0, l} A (x, fx) E R. f is the desired function. 0 We trust that the above theorems give an idea of how these kinds of proof work. We will be more free-wheeling in this respect in the rest of the paper. We conclude this section with a theorem on classes which, although not used in what follows, is important to establish the connection with the theory FM, of [20, pp. 98,991.

Generalizing classical and effective model theory

263

Finitary inductive generation

Assume we are given classes X,,, R such that R is a subclass of V3. We think of R as a rule of inference and we want the smallest X closed under
xocx , YlEX Y2EX XEX (~9 YI, ~2) E R.

We denote this class by Z(XO, R). Theorem 2.2.11. Let X,, and R as above. Then Z(XO, R) exists and satisfies
(9 X, = Z(X,, R);

(ii) (iii)

R(x> Y,, YZ) A Y, E Wb,

+

R) A ~2 E W,,

R)

x E&K,,

R);

X,~~~V~,Y,,Y,[R(~,Y,,Y~)~Y,~~AY,EW~XEW]

Z(X,, R) c W.

Proof. We can obtain the existence of such a class and a corresponding of induction as follows. Define by 3+-CA x EZ(X,, R) c, 3Y (Y = (PrYjP2Y) AP2Y E N AP2Y f0 A Vi<p2y
APIY(P2(Y) [plyil - 1) A (plyi EX~ v 3k9 l<i

principle

[Np~yipp~ykpIyQl)

=x1).

We prove that Z(XO, R) so defined satisfies (i)-(iii). (i) Let x E X0. Let s be a pair (f, 1) such that f0 =x (for example, let f be the constant function with value x). Then x E Z(X,,, R). (ii) We are given sequences s,,, = (f, m), s,,*= (g, n) which witness y, E Z(X,,, R) and y2 E Z(XO, R). Define a new sequence s, = (h, n + m + 1) such that j7c,
hk= gk, ifk<m, ifmGk<n+m,

i x,

if k>n+m.

It is easy to check that S, witnesses x E Z(XO, R). (iii) Assume x E Z(X,, R). Let S, = (f, n) be a sequence witnessing x E Z(X,,, R). We prove Vi <It [fi E W] by induction on i. Let i = 0. Then f0 E X0. But X0 c W. So, f0 E W. Assume true for all i < k <It. Now fk E X0 v 3j, I < k R(fk, fl, fi). Either fk E X,,, so j7c E W or there exist j, 1 <k such that R(fk, j7, fj), and then by inductive hypothesis fi, fZ E W. So fk E W. Hence Vi <n [ji E W]. In particular f (n - 1) = x E W. Cl 2.3. Interpretations of FMT,, We now give a general method for building interpretations of FMTO. We begin (following [17, pp. 70-791, [18, pp. 197-2001) by giving structures for the APP-axioms. The starting point is the notion of a pairing structure. A tuple P=(v,PP,P1,P2,0Jh+PN)

264

P. Mancosu

is said to be a pairing
p&Ix) = x.

structure

iff P: V*+= V, fi(P(x,,

x2)) = xi,

s,x #O,

Familiar examples of pairing structures are the natural numbers and settheoretical universes with the standard recursive pairing function and settheoretical pairing, respectively. Given any pairing structure P we can generate an applicative structure over it. An applicative structure is a tuple
A(V, =, k, s, d, p, PI> P2,
SN, PN, 0,

f >,%s

(f a code for /E 9) where 9 is a family of functions / V + V, possibly empty,

such that 191 s [VI. V is the universe of the pairing structure and = is an interpretation of App in V. Here x E N is interpreted as x E o where o is the least subset of V containing 0 and closed under x + s+. Given any pairing structure we can build an applicative structure as follows. First we choose codes for k, S, d, p, pl, p2, c, 0, sN, pN, /(for each/E 9). For example let the code for k be k, the code for s be S, the code for d be d and so on. Now for each X, y, z E V choose distinct codes k,, sX, sX,,, . . . for kx, SX, sxy, dx, dry, rlxyz, px, fx (for each/E 9), etc. For example, one can choose k, to be P(k, x), s, = P(s, x) and so on. Now consider the smallest relation App on V such that (writing ab = c for (a,b, c) E App), we have
Base: kx -k,, k,y =x, sx = s,, s,y = sxy, dx = d,, d,y = dxy, d,,z = d,,,, fx -e(x) for each/E 9,

d,..=w =x

if z = w, dXyzw= y if z # w,

etc.
Znductive: If xz = U, yz = w, uw = u, then s,,,z = V.

It is clear by construction

that
SN, 0,

A = (V, =, k, s, d, P, pl, p2,

f )fi9k APP-axioms
-/(xl...xn).

and for each nary/E

Examples

9, fxl...x,_,~

h fxI...x,_lx,

Besides the general method for obtaining interpretations of APP just given, we have a number of direct interpretations using recursion theory and its extensions. Consider the applicative structure A = (w, =, k, s, d, p, PI, P2, C, SN, PN> 0) where XY = z is interpreted on o as Kleenes relation z, and each individual constant is interpreted as a code of a recursive {X>(Y) = function satisfying the APP-axioms for that constant. The relation 2: is obtained by the enumeration theorem which allows one to define each partial recursive function Ge as Ge(x) = U(pyyT(e, x, y)). In this applicative structure the total
(i) Ordinary recursion theory.

Generalizing classical and effective model theory

265

functions from N into N are simply the total recursive interpreted as the class w.

functions,

where N is

(ii) #-recursion theory. The domain of the applicative structure is w. Assign codes as in the preceding example to the individual symbols. We use n:uniformization of a Hi-enumeration of II:-relations to obtain a #-relation c$(x, y, z) which expresses that the partial fl:-function with code x when applied to y yields, if defined, the value z, where every partial #-function has a code X. Interpret xy = z as 9(.x, y, z). Again take N to be the class o. Here the functions from N to N are the total II;-functions from w into o, in other words the hyperarithmetic functions. (See [35, pp. 402-4091 for details.) (iii) Admissible recursion theory. Here we let V = M where M is an admissible set with o(M) > w satisfying effective global well ordering: there is a &(M) function Y: o(M) ---, M which is one-one and onto. (We also say that M is recursively listed, in this case.) Under these hypotheses we obtain a E,(M) enumeration of the Z;(M) partial functions. Let fx =y be the & relation saying that the fth function at x has value y. Again interpret N as o. Here the class of total functions from N to N is simply the class of &(M) functions from o to o, or the functions which are A,(M) on w. Typical cases of interest are admissible sets L,. When IX is the first nonrecursive ordinal (w$) the Z,(M) partial functions from N to N coincide with the #-partial functions on w. (See [l, pp. 164-1681 for details.) Remark.

In the above examples the class of functions 9 is empty.

(iv) Set-theoretical structures. Let A = V, where A.is a limit greater than o. The family 9 of set-theoretical functions from V, into V, whose graph is a set in V, has cardinality G IVJ. We suitably assign codes in A to each individual constant and /e 9. The construction of the smallest class satisfying = as presented in the construction of a general APP-structure is set-theoretically definable. Interpret N as w. Here the extensions of the operations from N into N are simply the set-theoretical functions from o into o.

We shall use this wide range of interpretations of APP to generalize aspects which are common to classical model theory and effective analogues of model theory. An interpretation for FMT,, is a two-sorted structure V = (K App, N, K, EV), where V is the universe for some applicative structure. N is included in V, belongs to K and satisfies the N-axioms. K is a class of subclasses of V containing App and closed under class construction in FMT,. Finally, eV c V x K. For each

266

P. Mancosu

one of the above described applicative structures one can easily specify an interpretation for FMTO just by giving a class K of subclasses of the universe containing the App-relation and closed under class construction. I will now describe four interpretations of FMT, which represent our paradigm interpretations for what follows. The first three are minimal interpretations in the sense that the collection K is chosen as small as possible. In the last case we are more interested in the maximal interpretation, i.e., K is the collection of all subsets of the universe. It is clear that we could describe the maximal interpretations associated to applicative structures of the form (i), (ii), (iii) just by choosing the collection K as the collection of all the subsets of the universe of the applicative structure. Description of MI. We interpret App as in (i). K is simply the collection of recursively enumerable subsets of IX. N is interpreted as w. cN is interpreted as the standard < relation on w. The w-enumerable classes turn out to be the same as the members of K. The D-classes are the recursive subsets of CO. Description of itI*. We interpret App as in (ii). K is given by the I7:-classes. N is interpreted as w. cN is the standard < relation on w. The o-enumerable classes are in this case the same as the D-classes, i.e., they coincide with the A:-classes of integers. Description of M3. We interpret App as in (iii). o is simply the set of standard integers in M. cN is ew on o. The collection K of classes are given by the E:,(M) classes. The w-enumerable classes are the countable members of M. The D-classes are the A,(M) classes. Description of M4. Interpret App as in (iv). Here we let K be the collection of all subclasses of V, where V is the universe of App. We let N denote the standard integers in V. <,,, is E on w. The w-enumerable classes are simply the countable sets in V. The D-classes are the same collection as K. We can now prove three simple incompleteness results for FMT,. Consider the following statements: (a) A c B and B o-enumerable+A w-enumerable; (b) A is a D-class+ A is an w-enumerable class; (c) A w-enumerable+A is a D-class. Theorem 2.3.1. StutemenLs (a), (b) and (c) are independent of FMT,. Proof. Statement (a) is true in M4 but false in M2 where we choose B = o and A to be a Z7:-A:-subset of w. Then A cannot be w-enumerable, since the w-enumerable classes in M2 are exactly the A: subsets of w. Statement (b) is true in M2 and Ml but false in M4. Statement (c) is true in M2 and M4 but false in Ml. 0

Generalizing classical and effective model theory

267

Remark. The reader familiar with admissible set theory can immediately see that the examples Ml-M4 can be treated in a framework closer to that of admissible sets A satisfying Xl-GWO, with the functions being the &(A) partial functions and the classes closed under ET-definitions. However, the general construction outlined above leads to a much wider range of interpretations. 2.4. Syntax in FMT, An elegant formalization of syntax in FM, + APP is given in [20, pp. 114-1191. The concept of finitary inductive generation is used there to give an abstract treatment of formal systems. That approach has been improved in [22]. The reader is referred to those two articles for a general coding of syntax. That treatment can be followed by using our Theorem 2.2.11. Here I will follow instead the more familiar representation of syntax in the natural numbers. The advantage of doing so is that knowing that the APP-structure represents every primitive recursive function on N, the reader will have no trouble in believing many statements about the existence of various syntactic functions and relations in FMT,. We will code a universal first-order (single-sorted) language (for a standard account see [39, pp. 835-8381). Let u, := ( (1, l>, n>, c, := ( (1,2),
rn.m := ( (1,4),

n>, (n> m> >,

:= fn.m ((1,3), (n, m> >,

Var = (21,: n E N},

Const = {c,: it E N}, Rel, = {r,,,: n E N}, Rel= {r,,,: n,mENhm>O}.

{fnsm: EIV}, n Fun = {fn,, : rl,rnENAhrnO},

Fun,,, =

Fun,,, is the class of mary function symbols and Rel, is the class of mary relation symbols. These classes are all D-classes relative to N. We also choose codes for the logical operation symbols. We always assume that equality is r,,2. A language is a subclass L of Const U Fun U Rel which contains r,,*. We assume throughout in the following that L is a D-language. Then the class of terms (formulas) of L, Term, (Form,), are D-classes. Hence we can (1) carry out definition by recursion on Term, (Form,); (2) carry out proofs by induction on Term, (Form,). Moreover, we need several syntactic functions among which is free(a) = n giving max{i: Xi occurs free in (u} where a, is a term or a formula of L. If z,. ..z,_~ are in Term, and x~...x,_~ are in Var,, we can define sub@,, . . . 3 2,-l, x0, * * * f x,-~, y ) by recursion on y E Form,. This is the function for simultaneous substitution of Zi for xi in y and we write y(zo/xo, . . . , z,_~/x,_~) instead of sub(-, y). The definition is assumed to be given in such a way that sub can be performed only when z,,. . .z,._~ are free for x o...x,-l in y. From now on we shall work more informally in FMT,. Since I shall follow the model-theoretic development as found in [7], I will assume that the predicate calculus is formalized in a Hilbert style system as is

268

P. Mancosu

found there on pp. 24, 25, with sentential axioms, quantifier axioms, identity axioms and the rules of modus ponens and generalization. However, we will not need to refer to the specifics of this particular axiomatization. The class of logical axioms is easily seen to be a D-class relative to N. An axiomatic system is a pair S = (L, Ax) where Ax is a subclass of Sent,. We say that S is D-based when L and Ax are D-classes. When that is the case we can inductively define the predicate Proof(d, y, S), which says that d codes a proof of y from S. When S is D-based we have the following facts: (1) Proofs = {(d, y) 1Proof(d, y, S)} is a D-class; (2) we can carry out definition by recursion and proof by induction on Proof,; (3) Prov, = {y 13d Proof(d, y, S)} exists by 3+-CA. From now on, we shall use Greek letters 9, I#, 8, etc. for members of Form,, where L is a language. We write S k $J for @ E Prov,.
Theories

If X is a D-class, we denote Prov, by X*. A theory in L is simply a subclass T of Sent, which is closed under logical consequence, i.e., if @ E Sent, and $J E T*, then $ E T. T is consistent iff (x #x) $ T. T is complete iff for every # E Sent, either @ E T or l@ E T. We say T is a D-theory if T is a theory and a D-subclass of Sent,. The following two theorems are easily proved.
Theorem

2.4.1. An w-enumerable

complete theory is a D-theory.

Proof. By the generalized Theorem

Posts theorem (Theorem

2.2.10).

2.4.2. A complete D-theory is w-enumerable.

Proof. Let cT be the characteristic function for T. Let f : N % g:=crOJThusg(n)isOiffnETandisliffn$T.Let

Sent,.

Define

h(O) = pm(g(m) = O), Thusfoh:N=+

T. Cl

h(n + 1) = ym > h(n)(g(m)

= 0).

I will also assume that the basic theorems about syntax for first-order logic (e.g., the deduction theorem, the interpolation theorem, etc.) can be proved in FMTO.

A type r is a maximal consistent class of formulas in a fixed finite number of variables. A D-type Tis a type which is a D-class. As in Theorem 2.4.1 one easily sees that an w-enumerable type is a D-type. r is a type of a theory T iff r is a maximal class of sentences consistent with T.

Generalizing classical and effective model theory

269

Extension of languages by constants

Assume we are given a D-language L and a D-class of constants K, disjoint from L. Let L = L U K. Then L is a D-class (uniformly in the parameters L and 9. 2.5. Semantics in FMT, The main notions of semantics are those of structure and satisfaction; these are treated in FMT,, as follows. Let L be a D-language.
Definition 2.5.1. A structure A for L is a class which satisfies the following properties. A is the disjoint union of four classes A @ C @R G9F where (1) A is a nonempty class called the domain of the structure; (2) C c (Const fl L) x A is such that Vc E Const fl L 3!x E A ((c, x) E C); (3) R c (Rel fl L) X A is such that r E Rel, fl L & (r, x) E R +- lb(x) = m ; (4) F c (Fun II L) x A is such that f eFun,,,nL&(f,x)EF

lh(x)=m+l&Vx~A3!y~A[(f,x*(y))~F]

(* stands for the concatenation

operation).

For what follows we need to concentrate our attention on o-enumerable structures. A structure A = A @ C @ R 09 F is w-enumerable iff A, C, R, F are oenumerable classes. Let A be an o-enumerable structure. We can define an interpretation function for symbols of L as follows. cA = the only x such that (c, x) E C, &, = {x: (mm, x)
Interpretation of equality
l

RI,

f&z = {x: (fn,, x) E FI.

Note that the first element of R is =A, i.e., the interpretation of r,,, (the equality IXZhtiOn). We shall assume from now on that =A iS a congruence ElatiOII on A. In other words =A satisfies (1) zA is an equivalence relation on A; . . ,a,)E@f*(bo,. . . , b,)Efl]; (2) Uo=A b. A ---~a,=,b,+[(ao,.
. . ,a,,)~f~f*(b~ ,..., b,)EfA]; (3) a0 A b. A ~-~~(~,=~b,,+[(a~,. r and f are arbitrary relation and function symbols of suitable arity.

The notions of homomorphism and isomorphism between structures are defined as in the classical case, but with notions of onto and l-l given up to =. When one develops semantics and model theory in the standard ZFC framework, continual use is made of the possibility (guaranteed by the axiom of extensionality) to obtain quotients from sets and equivalence relations =A defined on A. Extensionality is then used to prove the uniqueness of the equivalence classes. Since we do not assume extensionality (see the following remark), we

270

P. Mancosu

work with pairs (A, A),

where A is a class and =A is an equivalence

A. When A is the real identity on A, we write =. When there is no confusion

relation on Z

will denote structures as A = (A, So). Let A = (A, cA) and B = (B, =B) be structures. A map f : (A, =J+ (I?, =B) is called a homomorphism iff (1) for each n-place predicate symbol r and each n-tuple (ai, . . . , a,) E A,
(a,, . . . > a,) E IA iff (f(4), . . . , f(4) E p;

(2) for each n-place function symbol h and each n-tuple (a,, . . . , a,) CA,
(a,, * * * 9 a,,, b) E h* + (f(d, . . . ,.%n),f(b)) E hE;

(3) f(P) ==B P. Iffis l-l (up to A and eB), then we have an isomorphism of A into B. Iff is l-l and onto (up to Ed), then A and B are said to be isomorphic and f is an isomorphism of A and B. A is a substructure of B iff A c B, =A is extensionally equivalent to A* f~ =B and the identity map is an isomorphism from A into B. Remark on extensionality. We could have dispensed carrying along an equivalence relation for each structure since all our paradigm interpretations are extensional. The reasons for doing so is that by carrying along the equivalence relation with each structure we can be totally noncommittal about extensionality for classes. The system is therefore neutral with respect to this issue and can thus be extended consistently in two different directions. (a) One could assume extensionality for classes. The reader may check that nothing in the development of model theory in FMT, is affected by this extra assumption. (b) The system may be extended to a theory a la Feferman [16-191, in which classes may be elements of V (ontological axiom) so that they can become arguments of operations from V into V. An assignment s in A is a finite sequence s E A<. Given an o-enumerable structure A, a term t and an assignment s with dom(.s) = free(f) (or any initial segment of w greater than free(t)), we can define by recursion on Term, the value of f in A at S. This is denoted by P[s] and is defined as follows: tA[s] = cA if t is a constant symbol c; t[s] = s(i) if t is a variable ui (where s(i) is the ith term of the sequence s); t[s] = the unique y such that (g[~]...e_~[s], y) efA, whenever t is a term of the formf(t,, . . . , tn_l). The above is a recursion by course of value with parameter s since it appeals only to subterms of t, whose numerical codes are less than t. Recursion by course of value on N is obtained from primitive recursion on N. We are now ready to formalize the notion of satisfaction, A k $[s], where C#E Formt and s is as above. A satisfaction relation for A is a subclass SatA of

Generalizing classicaland effective model theory

211

Form, x A (0) (1)

(2)

which satisfies the following clauses: free(@) s lb(s),

s) E Sat, (G?[~]...fAm-~[s]) E fl,

(@, s) E Sat, + @(to, . . . , Ll>,

(-$, s) E SatA f,

(G, s) $ W4,

(3) (4)

(# A v, s) E Sat, ++ [(9, s) E Sat, A (% s) E Sat,],

Cgvi 9,
S)

Sat.4

f,

3s*Vz<lh(s)(r#i+s*z=sz~s*ieA A ($, s*) E Sat,).

We cannot always guarantee in FMT,, given the weakness of the class axioms, for any o-enumerable language L and w-enumerable structure A for L, the existence of a satisfaction relation Sat,. Consider for example L = (0, , +, -} and let A with domain N be the standard structure for PA. We know that Sat, is not arithmetically definable. But the interpretation of FMT,, M,, consists simply of the recursively enumerable subsets of integers. Hence Sat, cannot be proved to exist in FMT,. We now come to the central definitions of our approach to model theory.
Definition 2.5.2. An u-enumerable structure A for a language L is said to be valuated iff 3s (S is a satisfaction relation for A). 2.5.3. An o-enumerable

Definition

structure A for a language L is said to be

w-valuated iff

3f : w %

Sat,, where Sat, is a satisfaction relation for A.

Clearly A o-valuated+A valuated. In order to show that A valuated does not imply A w-valuated we show that there may be an o-enumerable structure which is valuated but not o-valuated. Consider the interpretation iUs of FMT, with domain o obtained by letting the functions be the partial recursive functions on w and interpreting the classes to be the arithmetically definable subsets of w. Let L = {r}, where r is unary, and define a structure N = (0, =N, #) where 6 c N is a recursively enumerable subset of w whose complement is not recursively enumerable. If N were w-valuated we could o-enumerate {x 1N L-W(X)}, i.e., the complement of r would be recursively enumerable contrary to hypothesis. Yet N is easily seen to be valuated. In the interpretation M4 every o-enumerable model is automatically wvaluated since every countable structure has a countable satisfaction relation. In the interpretation Ml, w-valuated models coincide with the decidable structures. This is a corollary of Theorem 2.5.11. Let 0 denote the empty sequence. If o is in Sent, and A is a valuated structure for L, we write A b (Tfor (a, 0) E Sat,. It is now possible to prove a number of standard theorems on Sat,. For example, the following.

272

P. Mancosu

Theorem 2.5.4. Let A be a valuated structure. Then o E SentL+ A b (Tv A b xx Proof. By definition of SatA. Definition 2.5.5. Two valuated structures for L, A and B, are said to be elementarily equivalent (A = B) iff Va (o E Sent, + A b (JH B L a). Definition 2.5.6. With A and B as above we say that A is an elementary of B (A < B) iff (1) A is a substructure of B, and (2) for each 9 E Form, and s E A with free(@) G dam(s) we have (+, s) E SatA f, (f#, s) E Sat,.

substructure

Extensionalization of o-valuated structures

I already remarked that the context is nonextensional and therefore we cannot in general form quotients A/= A. Under what conditions can this be done? This is answered in the following theorem. Theorem 2.5.7 (Extensional
o-enumerable

elementary

structure A = (A, =J

substructures). Suppose we are given an for L. Assume A-E~ is o-enumerable. Then

wecanfindAlcAsuchthatA,iso-enumerableand~x~A3!y~A,[(x,y)~~,].

In other words, we can obtain an extensional substructure Al = (Al, =A,). Moreover if Sat, exists, then defining Sat,, = {(+, s) E Sat, 1Vi < lb(s) (s)~ E A,} makes Al an elementary substructure of A. Proof. Since =A and A-=, are o-enumerable, =A is a D-class by the generalized Posts theorem. We are looking for an enumerative function for AI. A and the characteristic function f=, of eA. We are given a function f : N a Now given an arbitrary n E N there exists a least m such that (g(n), g(m)) E =A. Thus, Vn Bm (f-,(g(n),
g(m)) = 0 A Vh <

m [f-,(g(n),

g(h)) =

11).

The expression inside brackets is equivalent to an expression of the form tnm = 0. So Vn 3m (tnm = 0). Now {(n, m) ) tnm = 0} is o-enumerable. Hence, by Theorem 2.2.6, 3h : N-* N such that (Vn) t(n, hn) = 0. Let AI = {g(h(n)) ) n E N}. This shows AI to be o-enumerable. Clearly VX E A 3!y E AI [(x, y) E ~~1. Finally, if Sat, exists, then the above definition of Sat,, is trivially a satisfaction relation on Al which makes Al <A. 0 Corollary 2.5.8. Let A be an o-valuated
elementary extensional substructure Al of A. structure. Then we can find an

Proof. If A is w-valuated,

then A2-zA is o-enumerable.

Generalizing classical and effective model theory

273

For this reason, all o-valuated structures A dealt with in the following are assumed to be extensional, i.e., A is = restricted to A.
Model-theoretic operations

We have shown how to extend a language L effectively to a language L U K where K is a D-class of constants. The model-theoretic counterpart of this operation is the expansion of the structure A for L to a structure A* for L U K. This is done simply by forming the disjoint union of the class of elements of A which interpreted the original constants and of the w-enumerable class of A interpreting the new constants. Although there are several ways to expand a structure A for L to a structure A* for L U K there is only one way to reduce a structure A* as described to a structure A, denoted A* 1L. The following lemmas are easily proved, under the assumption that L, K are D-classes.
Lemma 2.5.9. A* valuated +A* A o-valuated +A* 1L valuated. on L U K o-valuated. satisfaction class for a structure A.

Lemma 2.510. Theorem 2.5.11.

Let Sat, be an o-enumerable

Then Sat, is a D-class. Proof. The complement

the enumeration D-class. 0

Remark

of Sat, in Form, x A< can be o-enumerated by using for Sat,. Hence, by generalized Posts theorem, Sat, is a

2.5.11 establishes the connection between recursive model theory (and the other forms of effective analogues for model theory) and classical countable model theory. Classically every countable set has a characteristic function. Thus the lemma asserts something trivial in the classical case. But when interpreted in MI the lemma tells us that our request that Sat, be o-enumerable (i.e., recursively enumerable in M,) is really strong enough to prove that Sat, is a D-class (i.e., a recursive set). In the following I will develop a certain amount of w-valuated model theory. From the above results it follows that every theorem about o-valuated structures in FMT, translates into a recursive version of the theorem (or an hyperarithmetic version or an admissible version) when we look at the interpretations of the theorem in MI (or M2 or M,). The same theorem can then be interpreted in M4 to give the standard classical result. Thus every theorem about w-valuated structures in FMT, generalizes several effective analogues of a classical theorem. To the extent that these effective analogues are identical to the existing body of effective analogues for model theory, every theorem about o-valuated structures generalizes at once theorems of decidable, hyperarithmetic, admissible and classical countable model

2.5.12. Theorem

274

P. Mancosu

theory. We shall see that this is the case for the completeness and the omitting types theorem. However a more delicate situation will have to be addressed with atomic and prime models. Remark 2.5.W. Although I will be mainly interested in w-valuated model theory, one is not restricted to countable model theory in this approach. One could indeed develop model theory for arbitrary valuated structures (not necessarily countable) because in our framework sets and functions are not interdefinable. This is an advantage with respect to the formalization of model theory in fragments of second-order arithmetic in which sets and functions are interchangeable and every set is o-enumerable (see [38, Lemma 3.6, 0 11.3.41). The interested reader should consult [2.5] in which several systems are developed, in strict analogy with the main systems of reverse mathematics, in which one can develop a certain amount of general (not necessarily countable) stability theory. The approach in terms of valuated (but not o-valuated) structures was already developed in the last section of [20, p. 1221 using a system stronger than FMT,,. It turns out that the portion of model theory developed there by Feferman can be already developed in our system FMTO strengthened with a suitable version of Weak Kiinigs Lemma (see [30, Appendix] and [22, p. 2181). 2.6. Model theory in FMT, We now show that we have enough o-valuated structures to develop in FMTO abstract versions of elementary theorems in countable model theory, namely the completeness and omitting types theorems, and certain theorems on prime and atomic models. The following is the completeness theorem for countable theories. We assume we are working with a D-language. Theorem 2.6.1 (Completeness theorem). Let T be a D-theory, i.e., a D-class of sentences closed under logical consequence. Then T has an o-valuated model. Proof. Let K be a new D-class of distinct constants ki. Consider L(T) U K . This is a D-class, so F~rm~(~),,~ is a D-class. Thus we can give an w-enumeration An. C& of the formulas in L(T) U K which have only one free variable. We may assume that k,, does not appear in any #i for i s n. We now define a sequence of sentences a, in L(T) U K recursively such that AiS,, oi is consistent with T for each It. Define a,, = 3v, @n(vO)+ &(k,). Let 2 = {a,, 1n E N}. The claim is that 2 U T is a consistent D-class. Assume 2 U T is not consistent. Then there exists a proof of a contradiction from a finite subset of 2 and T, i.e., 3q 3 {T U A T h u s the class {i 13q {T U { q ,... q } k I + IA -I V } } I is non{ a ()... q } k V +! Ji t)}. empty and is defined by a 3+-formula. By the least-number principle there exists a smallest i in this class. Thus, for that i, T U { u o . . . D i-1) I-l U i e N O W use the standard argument to show that { uo.. . Ui-I} is inconsistent, thus contradicting the choice of i as least.

Generalizing classical and efectiue model theory

275

We now want to show that (2 U T )* is a D-class. Let sub-(q) = VX,,...~, r+l&/k,...x,/k,J, where n = max{i 1ki occurs in q}, if some new constants appear in W, and sub-(W) = W otherwise. We can now use the fact that T is a D-class. Let fr be the characteristic function for T. Then r# E (T,U X)* efT(sub-l(l\irn Ui+ q)) = 0, where n is as in the definition for sub-(q). This holds because if v E (T U Z)*, then the derivation need use only a,.. . a,, from .Z. Hence, T I-/& oi-* q, i.e., ence, fT(Sub-(~i~n oi+ @)) = 0. The other direcT 1 VJ (Aten ai(y/k)+ V)* H tion is immediate. So g =f 0sub- is the D-function for (T U 2)*. Let now An. q,, be an o-enumeration of all the sentences of L(T) U K. Define w(n) recursively by

w(n)=

Vn ( 7,

if g(w(0) A --- A w(n - l)+ r&J = 0, if g(w(0) A **aA w(n - l)-+ q!&)= 1.

Let Comp, = {w(n): 12E N}. This class is a complete, consistent and wenumerable extension of T. Hence Comp, is also a D-class by Theorem 2.4.1. We are now ready to define an w-valuated structure A for T. We denote by ci arbitrary constants in L U K. We let A = ConstLUK. Let
C = {(G, c,): c, E ConstLuK},

R = {(rii, c): rii E L A c E A <w A lb(c) =j A rjj(c) E Comp,}, ~={(~~,C):~~ELACEA<~A~~(~)=~+~A~(C~.._C~_~)=C~EC~~~~}. The claim is that A, C, R and F are o-enumerable. This is obtained from the Hence A = A %3C G3R G3F is an o-enumerable o-enumerability of Camp,. structure for L U K. We now prove that A is o-valuated. Define Sat, = { (#, c) : free(@) = rz A lb(c) > n A sub(@(c/v)) E Camp,}.

Clearly Sat, is o-enumerable and by Theorem 2.5.11 it is a D-class. One must finally check, and this is routine, that Sat, is indeed a satisfaction class for A. Finally, we define a new structure for T by taking the reduct A 1L. This concludes the proof. 0 The proof shows that an o-valuated
and T.

model can be found uniformly

from L (meta-)

From the point of view of the real world we have the following corollaries. Corollary 2.6.2. A consistent decidable theory T has a decidable model. Proof. Interpret Theorem 2.6.1 in Ml. Cl

(Similarly for interpretations

in M,, M,.)

276

P. Mancosu

Corollary 2.6.3. A consbtent countable theory has a countable model. Proof. Interpret

Theorem 2.6.1 in M4.

From now on we leave to the reader to infer the (meta-)corollaries from each theorem about o-valuated structures. Can we drop the assumption that T is a D-class? The answer is negative.
Theorem 2.6.4. The statement T consistent+ T has an o-valuated model is

independent from FMT,. Proof. First we show that there exists a consistent T which has no u-valuated model in a specific interpretation of FMTo. Consider a language with two unary predicates P1 and P2 and with a countable number of constants c,. Consider now two recursively inseparable recursively enumerable sets AI and A*. Let

S = {P,c, 1n E A,} U {P2c, 1n E AZ} U { V x (Pg ++lP2x)}. Assume S* has an o-valuated model. Consider the interpretation MS for FMTo, with domain w, where the classes are the arithmetically definable subsets of o and the functions are the partial recursive functions from o into w. Suppose in that model we can find a class A that acts as an o-valuated model for S. Thus A P$={n IAkP,c,} and P; = {n 1 kP,c,} would give a recursive separation of AI and AZ. Contradiction. Since the statement in question is true in M4, it also cannot be disproved from FMT,. 0
Remark.

It is possible to obtain Metacorollary 2.6.2 to Theorem 2.6.1 working in more familiar subsystems of second-order arithmetic like the system RCA studied in the context of reverse mathematics. Indeed, RCA has a model in which the classes are simply the recursive sets of natural numbers. Hence theorems of RCA can be shown to have a recursive interpretation. Thus in [38] one finds the completeness theorem for first-order sets of sentences which are closed under logical consequence (see [38, Theorem 8.41). Simpson remarks in a note: Theorem 8.4 applied to the w-model Ret implies that every recursively decidable theory has a recursive model with a recursive satisfaction predicate. This result of Morley is the beginning of a subject known as recursive model theory. This suggests a similarity with our own aim to obtain abstract results by proving them in suitable axiomatic systems. However, the emphasis in reverse mathematics is on finding a theory with enough strength to prove a certain result in its classical conception and then to show by reversing it that one cannot improve the result by using a weaker theory. The emphasis here on the contrary, is to use the fact of provability in a weak system and the larger number of interpretations that such a theory possesses, to generalize at the same time the classical and the various effective analogues.

Generalizing classical and effective model theory

277

This conceptual difference on the importance of analogue developments is a central issue in determining the choice of an appropriate logical framework and of suitable abstract languages in which to carry through the development. Among other things, a theory based on the language of second-order arithmetic cannot deal with uncountable objects, and as Harnik recognized [25, p. 2311 there are areas of model theory and algebra where a development limited to countable objects as in the current reverse mathematics program seems most awkward. It is exactly on the issue of generalizing countability and uncountability that the choice of suitable abstract languages allows for a better development than the ones available in subsystems of second-order arithmetic. A Henkin construction similar to the one used for the completeness theorem is exploited for proving an abstract version of the omitting types theorem. But first we need a few definitions.
Definition 2.6.5. A type T(x) is omitted by a sfrucfure A iff there is no a E A such that each element of T(x) is satisfied by a. A type is realized by u structure A iff it is not omitted. Definition 2.6.6. A type T(x) is said to be w-enumerable

iff it is an o-enumerable

class.
Definition

is said to be uniformly @(x) is consistent with T, then g(4) = v(x) is an element of T(x) such that @(x) A ly(x) is consistent with T. In other words, g($) gives a witness in T(x) to the fact that 9(x) does not imply all elements of T(x). T be a theory. A type T(x)
nonprincipal with respect to T if there exists a function g such that whenever Lemma 2.6.8. Zf T(x) is a nonprincipal uniformly nonprincipal. D-type of a D-theory T, then T(x) is

2.6.7. Let

Proof (informal). Given any consistent @ one searches through T(x) until one finds, by using the fact that T is a D-class, a suitable v(x). 0 Theorem 2.6.9. Let T be a D-theory and let T(x) be a D-type of T which is nonprincipal. Then T has an w-valuated model which omits T(x). Proof. Let K be, as in the proof of the completeness theorem, a D-class of new individual constants k,. Enumerate all the formulas of L U K with one free variable as G,,(x), &(x), . . . We may assume that k, does not appear in any I#J,. for i in. We want to define by recursion on N a sequence a,, of formulas of L U K such that r\isn ai is consistent with T and k,, $ q for all i <n. The construction of the a,, will also insure that for each n, k, witnesses the negation of a formula in T(x). Consider +,, in the enumeration. Assume we have already

278

P. Mancosu

defined oo.. . u,_~, so that /\i<n ui is consistent with T. We show how to obtain 0,. Define o= (3~0 &(uo)+ @,(k,)) A Ai<n oi. NOW U is easily seen to be consistent with T if T U A \i < n G i is consistent. Let C,. = {ki 1ki occurs in a} and consider C,. - {k,}. Define d to be the formula obtained from o by substituting every ki in C,. - {k,} by the variable vi and then quantifying existentially on such variables. It is clear that these syntactic manipulations are all effective. This has the form o = 3~.r,...ui, [o(kn, Vi,... Vi,)]. Thus cf(x/k,) is consistent with T. Since we have a nonprincipal D-type we know that T(X) is uniformly nonprincipal. Hence we can produce Y(X) in T(X) such that o(x) A l&x) is consistent with T. Now define a,, =ly(k,) A 3vo &(vo)+ &(k,). Consider 2 = {an: n E N}. Then (T U Z )* is a consistent D-theory. Then as in the proof of the completeness theorem we obtain an o-enumerable complete extension from which one extracts an o-valuated model. The model obtained is easily seen to omit F(x). Cl Remark. The above theorem can be strengthened to show that if we have an w-enumeration of o-enumerable nonprincipal D-types, then we can find an o-valuated model which omits all of them. The o-enumeration would be given by an f(n, m) such that for fixed n, f,(m) o-enumerates the nth type. We pass now to the abstract treatment atomic and prime models. Consider a complete theory T in L. in FMTo of standard theorems for

Definition 2.6.10. A formula +(x i.. .x,) is said to be complete 1.. formula 1+9(x .x,) exactly one of
T FVxI...x,, (c#J(x~...x,)+ q(xl...xn)), T FVx,...x,

(in T) iff for every

(@(xl...x,,)+~~(xl...x,J)

holds. Definition 2.6.11. A formula q(x i...x,) is said to be completuble (in T) iff there exists a completeSformula $J such that T I-Vxl...x, (@(xr...x,)+ ~(xi...x~)). Definition 2.6.12. A complete theory T is said to be atomistic consistent with T is completable in T. iff every formula

Definition 2.6.13. T is said to be uniformly atomistic iff there exists a function f such that every formula @ consistent with T is completable in T by f(@). We think of a uniformly atomistic theory as being given by a pair (T, f). Definition 2.6.14. A model A is said to be an atomic model iff A is w-enumerable and every n-tuple ~~...a,, E A satisfies a complete formula of Th(A).

Generalizing classical and effective model theory

219

Definition

2.63. An w-valuated model A is said to be uniformly atomic iff 3f such that for every n-tuple a,...a, EA, f(aI...a,) = 0(x,, . . . ,x,J is a complete formula of Th(A) with A k 8[a,. . . a,]. We think of an o-valuated uniformZy atomic model as a class pair (A, f). Theorem 2.6.16. Let T be a complete w-enumerable theory. uniformly w-valuated atomic model iff T is uniformly atomistic. Then T has a

Proof. (+) Assume T has a uniformly o-valuated atomic model A. Suppose @(x1, . . . , x,) is consistent with Th(A). Since T is complete, T t3x1...x, $(x1, . . . , x,). Then A L3q...x, +(x1, . . . ,x,). Since A is ovaluated, we can choose a ,...a, EA such that A t=$[aI...a,]. Now we use the uniformity of the o-valuation of A to pick a complete formula 0(x1, . . . , x,) satisfied by a,...a,. Thus T F Vxl...x, (0(x,, . . . , x,,)-, $(x1, . . . , x,)). The procedure described is uniform in $J and gives us an f satisfying the definition for

uniform atomicity. Thus T is uniformly atomistic. (G) Assume T is uniformly atomistic. We want to show that T has a uniformly w-valuated atomic model. We use another Henkin-type construction. Add to T a new sequence of constants K = {k, 1n E N}. Let iln. &, be an w-enumeration of the class of formulas in one free variable. Assume again that k, does not appear in any & for is n. We want to define by recursion on N a sequence a,, of formulas of T, such that each AiGn Ui is consistent with T and k,, 4 /\i<n q. The construction of the Ui will also insure that for each n, k,... k, are witnesses for a complete formula. Consider &(x) in the enumeration. Assume we have already defined a,. . . u,_~ such that A\i<n Ui is consistent with T. a,, is obtained as follows. Define

f(d(x,...

u is consistent with T. Consider now o = u(xo/ko...x,Jk,). x,)) is a complete formula 0(x,.. .x,) such that
T I-Vxo.. .x,, (0(x o...x,)+ d(xo...x,)).

By assumption

Define a,, = O(k,...k,) A (So & + &(k,)). Then Air,, Ui is consistent with T. Consider Z = {a,, 1n E N}. T U 2 is consistent and (T U . Z )* is a D-class. We now go to a complete extension Camp, as in the proof of the completeness theorem and we obtain an w-valuated model A. The model so obtained is uniformly atomic. Let in fact a 1.. .a,,, E A. Each ai (0 < i s m) is the denotation of a constant k,,i. Let n be the maximum of the nis. Look at the first conjunct of a,, and replace the k_s by variables. Existentially quantify out the remaining constants from K. This process gives us a complete formula satisfied by a,. . .a,. Thus (A, g) is uniformly atomic and w-valuated. 0

280

P. Mancosu

Theorem

2.6.17 (Uniqueness (B, g) be

theorem for uniformly atomic o-valuated

w-valuated uniformly atomic models

models).

Let (A, f) and Then A = B. Proof. Assume

and A = B.

A and B are not finite. Let a, be the first element in the o-enumeration of A and let f (ao) be a complete formula O(X) satisfied by a0 E A. Since A k 3x O(x), we have B k 3x O(x). So, since B is w-valuated, we can choose b. E B such that B k O[b,]. Now let bI be the first element of B - {b,}. Let g((b,, b,)) be the complete formula 0,(x,, x1) satisfied by bo, bI in B. Then B~00(xo)-+3x, O,( x0, x1). Choose a, EA to satisfy 3x1 @,(a,, x1). Now let a2 be the first element of A - {ao, a,} and so on. We therefore obtain two sequences ak, bk, k E N, such that A = {ak 1k E N} and B = {bk 1k E RJ}. It follows that the mapping a,+ b, is an isomorphism of A onto B (since each of the n-tuples ao...un-l, bo. ..b,_I satisfy the same complete formulas). 0

Finally let us look at prime models in FMT,. A mapping f :A -+ B is said to be an elementary embedding of A into B iff for all formulas @(x1...~,) of L and n-tuples ~,...a, EA we have
A b @[al... a,]

iff

B k $[fa,...fu,].

In standard model theory, A is said to be countably prime iff A is elementarily embedded in every countable model of Th(A). The corresponding definition in FMTo is the following.
Definition 2.6.18. Let A be o-valuated. A is o-prime embedded in every w-valuated model of Th(A). Theorem o-prime. Proof. This is simply the forth direction in the argument theorem for uniformly atomic models. q Theorem 2.6.20. Zf A is o-prime and o-valuated, 2.6.19. Zf A is an w-valuated uniformly

iff A is elementarily

atomic model,

then A is

for the isomorphism

then A is an atomic model.

Proof. Let A be W-enumerable, w-prime and assume A is not atomic. Then for contains = {r$(xo... x,_~): A k @[a,, . . . , a,_,]} some a,, . . . , a,_,, r(q)...&_*) no atomic formulas. Thus, since A is o-valuated, r is a nonprincipal D-type of Th(A). Hence, by the omitting types theorem there exists an o-valuated structure B such that B omits r. Hence A cannot be embedded into B. But this is a contradiction to A being w-prime. 0 Remark 2.6.21. Examples of decidable theories which are uniformly atomic are the well-known decidable theories of algebraically closed fields (of any charac-

Generalizing

classical and effective model theory

281

teristic) and real closed fields. No interesting general condition is known to the author which suffices to show that a theory is uniformly atomic. Theorem 2.6.16 is not a generalization of Harringtons theorem on prime models [26, p. 3051. In Harringtons version of the theorem from the existence of a decidable prime model one is able only to recursively obtain the code for a type but not the complete formula generating it. This is why we strengthened the definition of atomic model to that of a uniformly atomic model. One should remark that prime model is taken in the classical conception in Harringtons article, i.e., a model that can be (classically) embedded in every other model of the theory. This fact and the use of the priority method in the proof of Harringtons theorem do not allow us to give an abstract account of his result in our setting.
Remark 2.6.22. I have not been able to settle whether FMT, proves the converse of Theorem 2.6.19. Note that the proof of Theorem 2.6.20 is by contradiction and so does not allow us to conclude that A is uniformly atomic.

2.7. Limitations to a development of countable saturation in FMT,

I now take up a classical theorem on existence of countably saturated models whose treatment in terms of o-valuated structures requires a theory stronger than FMT,,. In general, given a theorem of countable model theory one wants to formulate an abstract version of it as done up to now. In general, there may be several classically equivalent statements which give inequivalent versions in a weaker theory such as FMT,, and then there may be no clearly preferred formulation. Once a candidate is chosen, to show that a certain theory cannot prove the abstract theorem one needs to provide an explicit counterexample to it by using one of the many interpretations of the theory. For analogues of the classical existence theorem for countably saturated structures, the abstract statement I will propose here is chosen to mirror the analogue development proposed by Cutland and coincides in the recursive interpretation with the notion of recursive saturation in the sense of Barwise and Schlipf [2, p. 5311. Classically a countable model A is said to be countably saturated if for any set of formulas T(X) in Ly (Y a finite subset of A) finitely satisfiable in Th(A, Y), there exists an a E A such that (A, Y) k IJa]. The classical theorem states: assume T is a countable complete theory with a countable list of all its types. Then T has a countably saturated model.
2.7.1. An w-valuated model A is said to be w-saturated iff whenever T(X) is an w-enumerable class in Ly (Y a finite subset of A) and r(x) is finitely satisfiable with Th(A, Y), then there exists an a E A such that (A, Y) k r[a]. Definition

282

P. Mancosu

Definition 2.7.2. An o-valuated o-saturated model is said to be uniformly o-saturated iff the (I in the conclusion of Definition 2.7.1 can be found uniformly (in the enumeration of r and Y). Can we prove in FMTO the existence of uniformly saturated structures in a way that captures the classical theorem quoted above? More precisely we would like to prove a statement, call it (*), of the following sort. (*) Let T be a complete D-theory with an w-enumeration of all its w-enumerable types. Then T has an o-valuated uniformly w-saturated model. An o-saturated model in Mr is a decidable model which is recursively saturated. Recall that a model A is recursively saturated iff whenever {&(x)}~~~ is a recursively enumerable set of formulas of Ly with free variable x (and Y finite) which is finitely satisfiable in Th(A, Y), then there exists an Q E A such that A I= &[a] for all n E w. Thus the reading of (*) in the 44r interpretation is: every decidable theory with a recursive enumeration of the recursive types has a decidable model which is recursively saturated. An o-saturated model in & coincides with Cutlands hyperarithmetic analogue for the definition of countable saturated model. An hyperarithmetic structure A is said to be hyperarithmetically saturated iff for all Y E A< any hyperarithmetic element type of Th(A, Y) is realized in (A, Y), Statement (*) holds in i&. In fact every hyperarithmetic theory with a hyperarithmetic list of all its hyperarithmetic types has a hyperarithmetic model which is hyperarithmetically saturated. An w-saturated model in M4 is simply a countably saturated model. Statement (*) holds in M4. In fact, if a countable theory has a countable enumeration of the types, then it has a countably saturated model. Theorem 2.7.3. (*) is independent of FMT,. Proof. (*) holds in M4 and MZ but can be shown to fail in Mr. The counterexample comes from recursive model therory. According to [33, p. 2391 there exists a complete decidable theory with a recursive enumeration of all the recursive types such that no decidable model of the theory is recursively saturated in the sense of Barwise and Schlipf. 0 This shows how to exploit the variety of interpretations of FMTO to determine limitations to an abstract development in a weak theory. This negative result suggests looking at stronger theories in which o-valuated w-saturated models can be shown to exist. This is done in the next section where a theory stronger than FMT,, FMT, is introduced. FMT provides a better development for abstract results generalizing an interesting portion of hyperarithmetic and countable model theory.

Generalizing classical and effective model theory

283

3. Generalizing

countable

and hyperarithmetic

versions

of model theory

In the present section I shall introduce a new theory FMT, which allows one to overcome some of the limitations presented by the development of model theory in FMT,. The theory Fh4T is related to the theory T,, without the ontological axiom and inductive generation, proposed in [16, pp. 120,121]. The main features that FMT shares with Tl are the existence of an operation eN which decides existential quantification on N and a class existence axiom (elementary comprehension) for elementary formulas, i.e., formulas which, roughly speaking, are defined by closure under connectives and quantification over individuals but not under class quantification. In [16, p. 1251 Feferman remarked on the relevance of systems like Tl to account abstractly for hyperarithmetic developments of model theory. There is one recent positive development in hyperarithmetic mathematics that ought to be re-examined with an eye to generalizations by means of formalization in Tl, namely hyperarithmetic model theory [. . .]. Denumerable models should play a special role since for these the satisfaction relation is decidable. In this section we work in the theory FMT to substantiate Fefermans intuition on the adequacy of systems possessing features similar to Tl for developing interesting parts of hyperarithmetic model theory. I claim that Fh4T is a theory adequate to formalize a substantial portion of classical countable model theory and hyperarithmetic model theory. However, one important point should be stressed. Fefermans quotation was motivated by the published work of Cleave and Cutland, which also attempted an analogue development of classical theorems dealing with uncountable cardinalities by using the ordinal levels of the hyperarithmetic hierarchy. Thus, for example, Cutland proposed an analogue to the classical notion of K-categoricity by using the levels provided by the constructive ordinals and defining a notion of a-categoricity for a E 0. In the following I will concentrate on abstract statements which will capture portions of hyperarithmetic model theory which do not depend essentially on the existence of a hierarchy or ordinal levels. Such is for example much of the development in the first part of Cutlands dissertation [12, pp. l-791, where one uses the ordinal levels only to estimate where a certain constructed object falls in the hyperarithmetic hierarchy. This part of Cutlands program dealt with completeness, omitting types, prime and atomic models, saturation and ocategoricity. The technical reason for restricting attention to the above-mentioned topics is that in FMT, unlike T,, we do not have the resources to develop an abstract theory of ordinals. This requires, in general, either axioms guaranteeing the existence of certain inductively generated classes (as in T,) or alternatively an explicit ordinal theory (as in Ta or FMTn, see Section 4). For the reasons given

284

P. Mancosu

above I will not deal with a-categoricity. However, I will present a notion of o-categoricity which, although unrelated to Cutlands notion, still has a natural hyperarithmetic interpretation. Thus, my claim that FMT is a theory adequate to formalize an abstract version of countable and hyperarithmetic model theory should be taken with the above provisos. However, the development of model theory in FMT is significant and accounts for a substantial body of theorems which have natural hyperarithmetic interpretations. Furthermore, in FMT we can give a development of model theory which is much more general than the one we offered in FMT,. There are three main advantages which justify the switch from FMT,, to FMT. In FMT we can (a) provide a better treatment for certain areas of countable model theory such as concern atomic or saturated structures; (b) develop model theory for arbitrary o-enumerable structures, since it is a theorem of FMT that every o-enumerable structure is o-valuated; (c) develop model theory for arbitrary w-enumerable classes of sentences without being limited, as we were in FMT,,, to theories, i.e., o-enumerable classes of sentences closed under logical consequence. Naturally, this does not come without a price. By strengthening the applicative structure we lose the recursive interpretation in which the APP-axioms are interpreted in the sense of ordinary recursion theory. However, this was to be expected, for in general the stronger the theory the fewer the number of its possible interpretations. 3.1. The theory FMT
Language of FMT We add to L(FMT,,)

an extra constant eN which stands for an operation decides existential quantification over N.
Elementary formulas

which

The class of elementary formulas is obtained from the atomic formulas of FMT,, by closing under 1, A and universal and existential quantification over individuals.
Axioms for FMT

We add to the axioms of FMT,, an axiom for the constant eN and a stronger comprehension axiom.
(f:N-+N) + (eNf =OveNf -l)h(eNf -0*3xEN(fx=O)). (eN)

The comprehension axiom of FMT, is strengthened to allow the construction of classes by the use of comprehension for elementary definable classes. By the

Generalizing classical and effective model theory

285

elementary

comprehension

axiom is meant the schema

3x (x E x e 9(x)) for each elementary

Remark.

WA)

formula 9(x).

Since classes are closed under complement, we can derive the leastelement principle for classes from the class induction axiom for N.
Some easy consequences (0) (f:N+N) +

(eNf-lt,VxEN(i(fx=O)). unbounded minimum

(1) The constant eN allows us to define the (total) operator p. (following [16, p. 1201) by defining
clef =

0, 1 cf,

if eNf = 1, if eNf = 0 (where c is the partial unbounded

p-operator).

Thus
(f : l+J N) + --* pof L A [3x (fx = O)+f (ruof) = 0 A VY < ,uof (fy =+(31.

(2) We can show that the following classes exist by ECA. (a) -X = {x: 1(x e X)}, (b) AB = {f: Vx (x lB+fx EA)}. (3) If A is o-enumerable,
Proof.

then A is a D-class.

Let g : N %
XEA

A. Consider the following equivalences: =x) t* 3nEN(g+n=O) c* eN(gd)=O

f* 3nEN(gn

where g,,xn = 0 f* gn =x. Let d := )3x.d01eN(gox)0. Then dx =0-x 3.2. Interpretations of FMT The strategy for building interpretations of FMT is the same as the one used for providing interpretations of FMT,. However, some modifications are necessary to insure that the applicative structures there presented can be expanded to interpret the constant eN and that the class collection is closed under ECA. Although M,, M,, M4 can be so expanded, this is not the case for Mi. In fact when eN is added, the partial recursive functions are not a model of the APP-axioms extended with the axiom for eN. In M4 one can easily modify the inductive construction of = to accommodate an extra clause for eN. In order to interpret eN in M,, i.e., in the applicative structure generated by the codes for I7:-partial functions, we notice that the
EA.

286

P. Mancosu

definition of eN is fl: and hence we may choose a number eN to satisfy

In the context of M3 the above defines eN as a Z,(M)-function. Finally, expand the class structure of Mz and M3 to be maximal, i.e., consider all the subsets of the universe; this takes care of the class axioms. Thus i&, M3 and M4 can be expanded to structures Mz, Mz and Mz which are interpretations of FMT. These are the paradigm interpretations for FMT and we will refer to them respectively as the hyperarithmetic, admissible and classical interpretation. 3.3. Model theory in FMT The formalization of syntax and the notions of semantics are as in FMT,,. From now on we will consider only D-languages without function symbols. As is well known this restriction can be assumed without loss of generality.
Theorem

3.3.1. Let A be an w-enumerable

structure for L. Then A is o-valuated.

Proof. LetA=A@C@Rwithg:N%Randd:N%A. Addnewconstants c, so that every element of A is named by a constant, say dn by c,. Then it is R we can obtain a function enough to enumerate Th(A, dn),,N. Since g : N % is an atomic sentence and Th(A, dn),,N k @}. This allows us to h:N=+{+j5 define the characteristic function for

{# ) C#I an atomic sentence in L U {ci}ieN and Th(A, dn)nsN k $} is by consequence (3) of Section 3.1. We now define the characteristic Th(A, dn),sN as follows: S,(@) = 0 X4(1$) = Iiff Th(A, dn),,N k +, for # atomic, function of

S,4(#),
0,

1,

if eN(An.S,($(c,lvi))) otherwise.

= 0,

S, is defined by the recursion theorem of Section 2.2; then it is proved by course of values induction on the logical degree of $I that SA($)J for all @ E Sent,,{,),=,. Let To enumerate Th(A, dn)neN, simply let w send N onto Sent,,t,),E,.
f (0) = PYN4(4Y)) = O), 0 that a f (n + 1) = PY (Y >f (n) A &(w(Y)) = 0).

Then gof :N%Th(A,

dn),,N.

(Meta-)Corollary 3.3.2. By interpreting Theorem 3.3.1 in Mz we obtain hyperarithmetic model has a hyperarithmetic satisfaction relation.

Generalizing classical and effective model theory

287

(Meta-)CoroUary 3.3.3. When we interpret Theorem 3.3.1 in M:, we obtain that a countable structure has a countable satisfaction relation. Theorem 3.3.4 (Theories of finite substructures). Suppose A = A @ C @ R is w-enumerable and X is a D-subclass of A. Then Th(A, X) is o-enumerable, uniformly in X.

Proof. As in Theorem

enumeration language L U { c x : x c X }.

3.3.1, Th(A, dn),EN is o-enumerable. Then the wis simply obtained by restricting attention to the of Th(A, x),,~
Cl

Completeness and omitting types We can now prove a version of the completeness

theorem. class of

Theorem 3.3.5 (Completeness). Let S be a consistent o-enumerable sentences. Then S has an o-valuated model. Proof. It is enough to show that we can obtain an w-enumerable

that S c S* and S* is closed under logical consequence. exists and has the required properties. Let S*={$I #ESentL

class S* such We now show that S* 9, x)]},

A 3x, y E N [Seq(x) A Vi < lb(x) (xi E S) A Proof(y,

where Seq(x) is the usual predicate x is a sequence number and Proof(y, @, x) means y is a proof from the class X = {(x)~: i < lb(x)}. Since we can decide by use of eN the defining clause of S*, we have an w-enumerable class S* satisfying the required properties. Now S* is also a D-class. Hence we can apply Theorem 2.6.1 to obtain the desired conclusion. Cl
(Meta-)CoroUary 3.3.6. By interpreting the result in M: one obtains that every consistent hyperarithmetic class of sentences has a hyperarithmetic model with a hyperarithmetic satisfaction relation. (Meta-)Corollary 3.3.7. By interpreting the result in M: one obtains that every countable consistent class of sentences has a countable model with a countable satisfaction relation. Definition 3.3.8. A class of sentences

T(x) is locally omitted by a consistent class of formulas S iff whenever $(x) is a formula consistent with S, then there exists a y E T(x) such that $J A -my is consistent with S.
Theorem 3.3.9 (Omitting types). Let S be an w-enumerable class of sentences. Assume T(x) is a consistent w-enumerable class of sentences which is locally omitted by S. Then there exists an o-valuated model for S omitting T(x).

288

P. Mancosu

Proof. This follows from Theorem

2.6.9 once we show that if T(x) is locally omitted by S, then it is uniformly nonprincipal. To prove the latter claim, let #(x) be consistent with S. We know, since T(X) is locally omitted by S, that there exists a y(x) E T(x) such that S U { c/)(. x ) A y( x )} is consistent. Since S is a we can test S U { q( x )} for consistency, for arbitrary I+!J. D-class by use of eN, Thus we simply run through T(X) until we find a suitable n(x) such that is consistent. We now apply Theorem 2.6.9 to obtain the s u {9(x) A lYitx)l desired conclusion. Cl Theorem 3.3.10 (Strengthened omitting types).
Let S be a consistent o-

enumerable class of sentences. Assume there exists an f such that for each n, f (n, m) is an o-enumeration of a class (not necessarily complete) T,(x) = m E N} of formulas consistent with S which is locally omitted. Then there {m,nI: exists an o-valuated model for S omitting each T,(x).

Proof. As in Theorem 2.6.9 we construct a class S U Z except that at each stage since we are trying to omit an o-list of types and not just one. a, is built in such a way that for all i <m there exists a yi,i E c(x), for some i E N, such that lYi,j(ci) is a conjunct of a,. Cl
m, a, is more complicated Prime and atomic models Let A be an w-enumerable structure. Since A is o-valuated, we have that A is w-prime iff A is elementarily embeddable in every w-enumerable structure B =A.

We shall prove below that this is equivalent to A being atomic.

we have a characteristic function for the predicate C#I an atom of T in n variables. is

Lemma 3.3.11. Zf T is complete and o-enumerable,

Proof.

Define Atom&n, +) := @ E Form, A ~v~...v,_~ ~(v~...v,_~)

A Vq E N [q E Form:+

ET E T) E T)].

(VV~...V,_~ (#(v~...v,_~) * ~(uo...u,-I))

v (VV,,...V,_~ (~#&,...v~_~)--+~ly(v~...v~_~))

Since T is a D-class, we can use eN to decide the second clause. Thus we see that

the predicate @ is an atom of T, is a D-class. Note also that the predicate 3n E N Atom&n, 4) is decidable too. El The lemma allows us to show that in FMT an o-enumerable model is atomic iff it is uniformly atomic and that a theory T is atomistic iff it is uniformly atomistic. Theorem 3.3.12. Let T be a complete o-enumerable
it is uniformly atomistic. theory. Then T is atomistic iff

Generalizing classical and effective model theory

289

Proof. If T is uniformly

atomistic, then clearly it is atomistic. Assume T is atomistic. Let f3(v,. . . u,_i) be consistent with T. We can o-enumerate by Lemma 3.3.11 the atoms of T in n variables. Since T is a D-class, we choose the first complete #(Q.. . u,_~) in the enumeration satisfying T 1 VQ...V,_~ ($~(u~...u,._~)+ The procedure described is uniform and provides us with a B(v,. . . v,_,)). Cl function satisfying the conclusion of the theorem.
Theorem uniformly

3.3.13. Let A be an o-enumerable

atomic.

structure.

Then A is atomic

iff A is

Proof. One direction is trivial. For the other direction, assume A is atomic and by Theorem 3.3.1 it is also let ao, . . . , a,_I EA. Since A is w-enumerable, w-valuated. Consider

T(vo...v,_,) Define

= {@(v~...v,_,): A k #[ao, . . . , a,_,]}.

F* = {~(v~...v,_,):

~(v,...v,_J

E F(vo...u,_J

A Atom,&n,

#)}.

Pick This class is nonempty, for A is atomic, and it is w-enumerable. 8(vo... v,_~) E F* to be the first in the enumeration. The procedure is uniform Cl and provides us with a function satisfying the definition of uniform atomicity.
Theorem atomic. Proof. One direction is simply Theorems 3.3.13 and 2.6.20. 0 Theorem 3.3.15 (Existence be a complete w-enumerable T is atomistic. Proof. By Theorem 3.3.12, T is atomistic iff it is uniformly atomistic; by Theorem 3.3.13, A is atomic iff A is uniformly atomic. Thus it is enough to prove that T is uniformly atomistic iff T has a uniformly atomic model. But this is 3.3.14. Let A be an w-enumerable structure. Then A is o-prime iff A is

Theorem

2.6.19.

The

other

direction

uses

theorem for w-enumerable

theory.

atomic structures).

Then T has an o-enumerable

Let T atomic model iff

Theorem 2.6.16.

0 of atomic structures). Let A such that A = B. Then A = B.

and B be two

Theorem 3.3.16 (Uniqueness w-enumerable atomic structures Proof. This is simply Theorem

w-valuated by Theorems

2.6.17, for A and B are uniformly 3.3.13 and 3.3.1. Cl

atomic and

290

P. Mancosu

Corollary 3.3.17 (Uniqueness

of prime structures). Let A w-enumerable prime structures such that A = B. Then A = B.

w-categoricity

and B be two

Definition 3.3.18. A complete theory T is said to be w-categorical iff whenever A and B are infinite o-enumerable models for T, then A = B. One can prove in FMT a famous theorem Svenonius. Definition 3.3.19. Let
E+={(c$, V/J,) @, VeForrn,~ 1

by Engeler,

Ryll-Nardzewski

and

T~Vv,...v,_,(~(v,...v,_,)t*ly(v,...~,_,))}.
then EF is a D-class.

Lemma 3.3.20. Zf T is complete and w-enumerable,

Proof. If T is complete and w-enumerable, then T is a D-class. Thus the condition defining E; is given by a characteristic function. Hence E; is a D-class too. 0 Remark 3.3.21. To say that Form:/& is finite means that there are &,. . . &,, in Form, such that for every I+!Jin Form:, there exists an i 6 m such that (9i> $) E EnT.
theory. Assume finite models. Then the following conditions are equivalent: (1) T is w-categorical; (2) Vn E f+J 3m E N ([0, m] %

Theorem 3.3.22. Let T be a complete w-enumerable

T has no

Form~IE,).

Proof. Simply follow the proof given in [32, pp. 447,448] making a few suitable modifications. 0
w-saturated and w-universal models

Deli&ion 3.3.23. An o-enumerable structure A is said to be w-saturated if class r(x) = for every finite X = {x0. . .x,-i} in A and each w-enumerable {f#&) ( n c N} in L = LU {cx,...c,._,}, such that for each finite subset r of r there is an a E A with (A, X) k A P[a], there is.an a E A such that (A, X) I=$[a] for all @ E K Definition 3.3.24. An w-enumerable structure A is uniformZy w-saturated if A is w-saturated and the element a in the conclusion of Definition 3.3.23 can be found uniformly in X and the enumeration of r

Generalizing

classical and effective model theory

291

Lemma

3.3.25. Zf A is an w-enumerated w-saturated model, then A is uniformly

w-saturated. and w-saturated. Let X be a finite subset of A and r, an arbitrary w-enumerable class of formulas in one variable, say x, in Lx. We use Theorem 3.3.4 on w-enumerability of finite substructures to obtain an X, a). For any f, wenumeration of Th(A, X, a). Let ha : N %Th(A, enumerating a class of formulas T(x) in Lx, define 0, 1, Since
(A,

Proof. Let A be w-enumerated

if Vn E N [(A, X) L @,&I], otherwise.

(A, X, a) k &&x/c,)

X) L &[a]

iff

iff 3m E N ham = d%h/G)h

we can define g by applying eN. Hence we can choose the element a in the conclusion of Definition 3.3.23 of w-saturation as the first one for which gfa=O. Cl
Theorem 3.3.26 (Uniqueness for w-enumerable w-saturated structures). Let A and B be w-enumerable w-saturated structures such that A = B. Then A = B. Proof. Assume A and B are infinite. Let a : N % to define two new sequences

A and b : N %

B. We want

a*:N*A such that

and

b*:N_B

(A, az...a,*... ) = (B, b,*...b:...). Suppose that a:. . .ai_l, b,*...b,*_, are already defined, with
(A, a:... a,*_J = (B, b,*...b,*_,).

(9

(*)

Assume n is even. Choose m minimum such that a,,, #a for i < n. Let a,* = a,. Define r = {$: @ has at most one free variable x, 9 is in the language of (A, a,*)i<n and (A, Oicn b 4Wl>. r is w-enumerable, by w-enumerability of the theories of finite substructures proven in Theorem 3.3.4. By (*), each finite subset of r is realized in B. By using the uniformity of w-saturation of B we pick a b E B such that (B, b,*...b,*_,, b) k r[b]. Let b,* = b. Thus,
(A, a:... a,*) = (B, b,*...b,*).

If n is odd, interchange the role of a and b, (a&,, and (b&, Finally, let f (a:) = b). This is the desired isomorphism. 0

and A and B.

292

P. Mancosu

Theorem

3.3.27

(Existence

of w-saturated

o-valuated

models).

Let L be an

o-enumerable language and let L = L U C for an o-enumerable class of infinitely many distinct new constants C. Let T be an o-enumerable complete theory. Assume that we have a uniform w-enumeration of the o-enumerable complete l-types over T in all expansions LB (for finite B in C). Then T has an w-enumerable o-saturated model.

In order to prove the theorem we need the following lemma and corollary (cf. [20, pp. 123,124]).
Lemma 3.3.28. Let {Gn( x ) : n E N} = T(x) be an o-enumerable class of formulas in L(T) with at most x free. Zf c is a constant which does not appear in T or T(x) and T is consistent, then it is consistent with (3x (AiSll &(x))+ AiSn &(c)},,,.

We have two cases. Case 1. Assume T is consistent with 3x (Air &(x)) for all n E N. Then T is consistent with {&(c)}~~~. Thus T is consistent with (3x (Aim r#+(x))-, l\& &(C)),,N* Case 2. Assume for some n E N, T 113x (AiGn &(x)). Let k be the least such IZ. We now show that for any n, T U (3 ~ ( A i s ,, + i( X ))+ A \i s n p i },,, is consistent by looking at the cases n <k, n 2 k. For n <k, T U ( 3 x (/ji c k & ( x ))} is consistent by choice of k. Thus T U ( 3 x (/ji c k 4 +( x ))- /ji s k t # +( c )} is conis inconsistent, since sistent. Assume n 3 k. Then T U ( 3 x ( A i < ,, & ( x ))} T U (3 ~ ( A i = ,, # Q ( X ))} k l\i < n C & ( C ) for all n 2 k. T k l!I X ( A \i s k @i( X ))Thus, ! Hence T U (3 ~ ( A i < n # i( X ))+ A is, & ( c )},, N is consistent.
Corollary 3.3.29. Let {#m,i(X)},,i,N b e an w-enumeration of formulas in one free variable x, where for each m there are at most finitely many constants beyond L(T) in all ~m,i(X). Let c, be a constant symbol not in T or ~i,i for j s m and i E N. Zf T is consistent, then it is consistent with (3x (AiSn &,Jx))-, AiS,, #m,i(Cm)}n,maN.

Proof.

We are now ready to prove the theorem. The idea is to use Corollary 3.3.29 by constructing in one swoop an o-enumerable class which will insure that each type is realized by a constant and that the complete extension we will obtain from it has witnessing constants for each existential formula in the expanded language. Assume T has an w-enumeration of all its o-enumerable types in finitely many extra constants B from C given by a function g. Let &(x) be an o-enumeration of all the formulas in L U C with one free {&(x): i E N} and define h*(n, i) = h(n). Let variable. Let h : N %
g((n + 1)/2, i), i) f(n i)=(h*(n/2 > >

Proof of Theorem 3.3.27.

if n is odd, if 12is even.

Generalizing classical and effective model theory

293

Thus for each fixed IZ, {f(k, i): k <n A i E N} has finitely many extra constants from C. Let f(j, i) be denoted by ~j,i(X) and ctO) is the first constant not Then S = T U ( 3 x ( A i ~ n q j, & ))+ appearing in T or any ~lk,i for kcj. is consistent (by Corollary 3.3.29) and w-enumerable. From Aisn Vji,iCCt(j))>j,neN S we pass to the deductive closure S* which is shown to be a D-class. We then proceed as in the proof of the completeness theorem to obtain a complete o-enumerable extension. We then extract from the complete extension an o-enumerable model A. It remains to be checked that A is o-saturated. For, if r = {&(x): n E IV} is an w-enumerable class of formulas consistent with for some finite subset B of A, then we can extend it to a complete Th(A> C&R, type r* in Lg. By construction a constant was added to witness r*. Thus since r is included in r*, that constant also satisfies r in A. This concludes the proof of the theorem. 0
Definition 3.3.30.

o-enumerable

An w-enumerable model A is said to be universal iff for all models B such that A = B we have B <A.
Let A be o-enumerable. Zf A is o-saturated, then A is

Theorem 3.3.31. o-universal.

Proof. Since A

is w-enumerable, by Theorem 3.3.1 it is also o-valuated. Moreover, it is also uniformly saturated by Lemma 3.3.25. Now we can apply the Cl technique of Theorem 3.3.26 by using only the forth direction.

4. Generalizing

admissible

and classical versions

of L(Q)-completeness

In [19] Feferman introduced a theory of operations and classes, Tn, with the aim of providing a unified framework suitable for generalizing portions of classical model theory dealing with models of cardinality &r and an analogue theory on admissible sets developed by Cutland. Cutland worked with admissible sets which satisfy a property called &-global well ordering (&-GWO). He then considered structures A = (A, . . .) such that A EM for which the satisfaction relation Sat, is E,(M). When M is locally countable, one obtains an analogue for classical results where elements of M correspond to countable sets and the &(M)-subsets of M correspond to sets of cardinality SK,. Feferman outlined how to develop this part of model theory for first-order logic abstractly in Ta, with special emphasis on saturated models. I will extend this approach here to show how to deal with extensions of first-order logic such as L(Q), where Q is the quantifier whose intended interpretation is there exist uncountably many.

294

P. Mancosu

tthe axioms for L(Q) are: (1) the universal closure of all first-order schemas; (2) lQx(x=y vx=z); (3) if_x (@-+ V)-+ <Qx$+ Qxq); (4) Q@(x)c*Qu@(~); (5) QY~X 9+ 3~ QY# v Qxgr 9. The rule of inference is modus ponens. These axioms have been shown sound and complete for standard models (see below) by Keisler [28]. The aim in this section is to generalize the soundness and the completeness theorem for L(Q) whose classical versions can be found in [27-291, and whose admissible versions were given in [4,41]. In the classical case the main notion is that of a standard model for L(Q). A model A for L(Q) is said to be standard iff AkQxq(x) iff ~X~A(~X]~N,AVXEX(A~~[X])).

It is convenient to take A = {a: a < wl} when IAl = N1. By L(Q)(r) we mean the logic L(Q) in a fixed countable vocabulary r. (I follow here the notation used in [27].) The completeness theorem for L(Q) asserts that if T is a countable consistent set of sentences, then T has a standard model of cardinality Ki. The idea of the proof is to obtain a standard model for T as a union of an elementary chain of so-called weak models. The latter are introduced as a handy tool to study logics like L(Q) by reducing them to first-order logic. The reduction consists in expanding the vocabulary r to a vocabulary t+ which contains new predicates R+(,,,...,~) which are surrogates for Qx@(x, yi.. .y,,). Thus weak models are special kinds of first-order structures. A standard model for L(Q) is obtained by first finding a weak countable model for T. Then one proves a main lemma which allows one to pass from a weak model A, to a weak model A,,, and which insures that uncountable sets in A, are enlarged by new elements in A,+1 while countable sets are kept fixed. Iterating this process w1 times we obtain a chain of o1 models whose union is the standard model sought for T, since the uncountable sets are really uncountable. Bruce and Keisler [4] developed an admissible interpretation for the logic L(Q) by working with locally countable admissible sets M with o(M) > o and satisfying ZI-GWO. A model for L(Q) in this framework has domain o(M) and is such that the satisfaction relation on it is A,(M). Furthermore, if such a model, call it A, is endowed with an M-recursive function f which gives a bound on {q: A k #(q, y)} whenever A kiQx$(x, y), then Bruce and Keisler call A a recursive model. The interpretation of Qx in this context is there exist unboundedly many. Bruce and Keisler proved a soundness and a completeness theorem for such models by using their technique of forcing for languages with extra quantifiers. Wimmers [41] modified their approach by assuming that the admissible set M satisfies &-collection. This assumption gives enough functions as to avoid the need for an explicit appeal to a bounding function in the definition of recursive model.

Generalizing classical and effective model theory

295

(Wimmers [41] extended the Bruce-Keisler results to L(Q) and L(U).) It should be remarked that the extra assumption of a bounding function in the definition of recursive model is necessary only for soundness and not for the completeness theorem for L(Q). The Bruce-Keisler approach is the more appropriate one to be adapted in our framework. The first part of this section is devoted to introducing the theory FMTQ, which shares many of the features of TQ In particular, all the ordinal axioms of FMTS2 are taken from TO We then give two paradigm interpretations for FMTra which justify the claim that FMT, provides an abstract setting adequate to generalize results which have classical and admissible versions. Finally, we sketch the model theory for so called weak models for L(Q) which will be used to prove the completeness theorem for L(Q). I already remarked in the introduction that the guiding aim is to produce a generalization which looks as much as possible like the standard development. Accordingly, I will follow here the exposition of L(Q)-completeness found in [27] modifying it slightly to fit our framework. 4.1 The theory FMTn The theory FMTn is obtained by extending the language and axioms of FMT by suitable individual and class constants in order to be able to have an abstract theory of ordinals.
Language

of FMTn

Individual constants. We add o, sn, in, q, c, u, to the individual constants of FMT. w stands for the ordinal o, sn stands for successor on the ordinals, q for an operation deciding bounded quantification on the ordinals (so q is a generalized e,), c for choice or selection and u is used to uniformly w-enumerate all the ordinals. Class constants. We add class constants Sz, era. Conventions. Lower-case Greek letters a; p, y, . . . range by convention over elements of 52. LY /3 stands for (CX, E <a [0, (u) stands for the elementary < /?) class {g: 5 < CX}. We write f : a+- 8 for f : [0, (Y)+ 52. The class of limit ordinals is defined as Lim={cuI LY#OAV~(~<(Y *so(g) < a}. We write e! C#3 for cu<pvcu=/3. Axiom for FMTn. We add to the axioms of FMT the following axioms. (1) xlzN*x<w; (2) x<,y-,x<y; (3) (linear order) ~~aA(a~gvBaa)A(a~BABsv (4) (least element)
O E ~ A v( Y ( O S c Y ); ~( Y ~ y) A (( Y ~ ~ A ~ ~( Y +( Y = j?);

296

P. Mancosu

(5) (successor) s&!(a) E 52 A LYuss,(cr) A vg ((UC C+s*(cu) (6) (limit)

wELiiAVcx((YELim-+o==cu); (7) (induction on 52) for each formula

< Q;

q(a),

Va ](VE< a)+(S)+ (8) (regularity of Q) (f:cu-,Q)+3/3(f:a+@;

$441-+V~ v(4;

(9) (decidability of <a in initial segments) (ZffX~OvI~=l)A(I~~~Ot,x<a); (10) (bounded quantification)

~ Z [~ ~ = Z-, Z = ~ V Z = ~] A [~ ~ ~ ~ ~ t , v ~ < c U (f ~ ~ ~)] A [% f = 1 + + 3@~(f ~ f 0)];

(11) (selection)
f ~ = O-,[ C f E i 2 A f( C f)= o];

(12) EOC (Every Ordinal is Countable) v&, (UN: 0 = [O, (u)).

This concludes the description of FMTn.

Remark.

The previous theory differs from Fefermans

Tn + EOC in two main

respects. First, we are not treating classes as individuals. Hence, we have dropped the so-called ontological axiom VX 3x (x = X) which allows one to act on classes as if they were individuals. Secondly, as a consequence of the previous decision, we cannot have the join axiom which is an infinitary principle of class construction. Again, this creates no problem since I will be interested in w-enumerated or Q-enumerated models. Thus, we can act on the enumerations instead of acting on the classes. (For proofs see [18, pp. 182-1841.) (1) (successor) sn( (u) = s&3) + a = /3. (2) (predecessor) 3f (f : &2+ 52) A (I@ (s & 3) = a)+sn(f (s&a)) = a)). We write pd for the predecessor function. (3) (least element) 3a $((u) += 3a {#(a) A Vg < CL-+(~)} for every formula (4) (supremum) (f : a ~ Q )~ 3!8[f: c u ~ P A v r < P l(f: c u ~ y)]. We write /I = sup5<nfS when (YE Lim. (5) (Lim is a D-class) 3f [f : Si2+(0, l} h fa = 0~ (YE Lim]. #.
Some useful consequences.

Generalizing

classical and effective model theory

297

(6) (recursion on the ordinals) from CQ, g we can find f uniformly satisfying
f0 = ffo, f (s&x) = ga(fa), (YE Lii + fc&! supa<W(fg). =

Using the above results ordinal arithmetic can be developed. In particular it can be shown that every ordinal (Y# 0 can be uniquely represented in the form a = 25(2r] + 1) with ,$ < a; r~< a. Thus, we have a natural pairing function n : Q2+ Q and projections n,, nz. As in the case of FMT we now relate the APP-axioms and the class axioms by looking at special kinds of classes like o-enumerable and Q-enumerable classes.
Definition 4.1.1. A class A

is said to be w-enumerable

iff A is empty

or

3f (f :[O, o)*A). Definition 4.1.2. A class A is said to be S2-enumerable

iff A is empty

or

If (f :@=+A). Definition 4.1.3. A

Q-enumerable
Example 4.1.4. Closure

class A is said to be strictly Q-enumerable but not w-enumerable.

w is Q-enumerable enumerations.

iff A

is

but not strictly Q-enumerable. are easily proved, as in [19,

under

The following

pp. 184,185].
Lemma 4.1.5. Zf A, A U B, A x B, A<. Lemma
is

B are w-enumerable

(or Q-enumerable),

so are A II B,

4.1.6. Zf for each (Y E w, fa: w %

A,,

then U,,,

A, = {faj:

(Y, j E W}

w-enumerable.

Lemma 4.1.7. Same as Lemma 4.1.6 with Sz substituted for w throughout. Proofs of Lemmas 4.1.6 and 4.1.7.

By using a pairing function on w or Q which 0

gives the required enumeration.

Uniformization and choice

Lemma 4.1.8. Suppose R is (w-) Q-enumerable, (1) 3f V~PY (JGY)ER+(~,~~)ER); (2) if B is (w-) Q-enumerable, then

where R E A x B. Then,

3fVx{3yEB(x,y)ER+fxEB~

(x,fx) ER); (3) with the same assumptions as in (2), (VxEA3yEB(x,y)ER)-,@f Proof. As in Theorem (f:A+B)r\VxEA(x,fx)ER).

298

P. Mancosu

4.2. Interpretations of FMTn

The general strategy for building interpretations of FMT, is the same as that for interpretations of FMT. The only new aspect to be dealt with lies in arranging that the ordinal axioms are satisfied. We have two paradigm types of structures, namely interpretations for FMTo arising from admissible set theory and those arising from models for ZFC. Since I will give only a sketchy overview the reader is referred to [19, pp. 178-1811 for more details. The basic idea is that we can select a class of interpretations for FMTo from admissible set-theoretical and classical set-theoretical structures by suitably defining the interpretation for L(FMT,).
Interpretations arising from admissible set theory

Let (M, E) be a pure admissible set such that o(M) > o and such that M k&-GWO and M is locally countable. We know that for such M we can enumerate the class of &-partial recursive functions. We interpret App(f, x, z) to mean that the fth function at x has value z. This is a &-relation on M. We let the class collection be given by all the subsets of M. 52 is interpreted as o(M) and < is interpreted as < on o(M). N is interpreted as { cr:M k cx < o}. One can now check that the ordinal axioms hold in the model for suitable interpretations of the individual constants. In particular the choice function c is &-definable, and the uniform countability of the ordinals follows from the assumption that M is locally countable. It turns out in this interpretation that the Q-enumerable classes are exactly the &(M)-classes while the o-enumerable classes are just the classes which are countable in M, hence, up to extensional equivalence, just the elements of M. Then the strictly Q-enumerable classes are exactly the &(M)classes which are not elements of M.
Interpretations arising from models of ZFC Let (M, Ed) be a model of ZFC and assume P, P,, P2 are standard pairing and projection functions on M. Let F be the class containing (1) the collection of partial unary functions whose graph is a set in M together with PI, P2 and the successor operation; (2) the pairing function P, and the characteristic function of E,,.,; (3) the ternary function Sep with Sep(a, b, 6) = {x EMa: (M, Ed) k @(x, b)}. We now generate a ternary relation fx = y as described in Section 2.3 with the

clauses for all the constants k, s, u, etc., and such that for every nary function F(x,...x,) mentioned above there exists an element f EM such that fxl...x,_li and fxI...x, = F(x,.. .x,). In particular, the inductive clause for q is as follows. VxEMa (fx -0)
+ qaf =O, VxEMa3y#O(fx=y) + qaf =l.

We let the classes be just the collection of subsets of M. We let Sz denote the class of ordinals less than K,. < is simply < on K1. Let <,,, be < restricted to o and interpret N as w. One can check that the rest of the ordinal axioms hold in

Generalizing classicaland effective model theory

299

this model. In particular, selection is proved by exploiting the inductive clause for q. Let ,U be .the function which given any nonempty subset a of Hi, outputs its minimum element, denoted by ~(a). p sends the power set of K, into M and its graph is in M. Let @(x, f) be the formula Ord(x) A fx = 0. Then by the inductive clause for q take cf=p(Sep(K,,f, $J)), i.e., cf=~({~:f~=O}). In this interpretation the o-enumerable classes on M are simply the countable subsets of M, the a-enumerable classes are the subsets of M of cardinality SK,(M) and the strictly a-enumerable classes are exactly the subsets of cardinality Xi (up to extensional equivalence).
Remark 4.2.1. Let B be w-enumerable. In classical set theory a subset of a countable set is countable. But in FMTn we cannot prove that if A G B and B is o-enumerable, then A is o-enumerable. For a counterexample consider the model obtained from the admissible set (L,,, E) with o1 being the least nonrecursive ordinal. We let B = o. We know that for A c o, A is o-enumerable iff A is hyperarithmetic and A is Q-enumerable iff A is II:. We take A to be a Ui-A:-subset of o. This class is D-enumerable but not o-enumerable. We can show that if B is an a-enumerable class and A c B, it does not follow that A is Q-enumerable. Let B = 8. Choose a subset A of B whose complexity in terms of the analytical hierarchy is greater than KI:. Then A cannot be Q-enumerated by a partial I7:-function. 4.3. Model theory in FMTn Languages, structures and satisfaction

As in the case of FMT we assume we have coded a universal language

L UN
= {tcd7 (rn,d7

(fn,n))nsR, nEO

by use of Q. Languages are D-subclasses of LUN. For simplicity, and without loss of generality, we will work with languages in which function symbols do not appear. We assume we have codes for the variables, connectives, quantifiers and the extra quantifier Q. By L(Q)( z ) we mean the logic L(Q) restricted to the vocabulary t. t is usually taken to be an o-enumerable subclass of LUN. A structure A = A @ C @ R for an w-enumerable language L(Q)(t) = {co, m,,} is given by the disjoint union of a class A E 52, a class C in ConstL x A, and a class R in Rel, x A, whose elements satisfy Vc E Const, 3!x E A ((c, x) E C),
Vr E Rel, ((r, s) E R --, lb(s) = m).

A satisfaction relation for a structure A is a subclass SatA of Formt(o)(,) x A< which satisfies the standard first-order satisfaction clauses plus the following

300

P. Mancosu

condition for Qx: (Qu,#, s) E Sat, iff 3xG52(vxEL23yEx(x<y) A Vs*(Vz <lb(s) ((i # zts*z=sz)hs*iEX)+(#,s*)ESat,)).
Definition

4.3.1. A structure A is said to be L&enumerable iff A, C and R are S2-enumerable.

Definition 4.3.2. A structure A is said to be strictly L&enumerable iff A is strictly

L&enumerable.
Definition 4.3.3. A structure A is said to be G-valuated iff A is &?-enumerable

and Sat, is Q-enumerable. We already know, by Theorem 3.3.1 that if A is an o-enumerable then A is o-valuated. This does not hold for Q-valuated structures.
Theorem 4.3.4. The statement if A is L&enumerable,

structure,

then A is L&valuated

is

independent from FMTa. Proof. The statement

is clearly true in the interpretations obtained from models of ZFC. For a counterexample consider the model obtained from Lo5k by letting the classes be arbitrary subclasses of LwTk.Choose a theory in one predicate R. Define a structure with domain Sz and interpret R as a &-subset of L2 whose complement is not 2i. If A were G-valuated, then we could Q-enumerate {(u (A bR[a]>. 0
4.3.5. An G-valuated model A for L(Q)(t) the domain of A is strictly Q-enumerable. Definition Remark 4.3.6. When A is Q-valuated, (Qv&, s) E Sat, iff 3XGS-22f ((f:S-2 %XAf:Qi,X) ((i f z +s*z =sz) r\s*i EX)+ (#, s*) E Sat,)).

is said to be standard iff

we have the following

equivalence:

A Vs* (Vz <lb(s)

Definition 4.3.7. A standard model A is said to be uniformly standard iff there exists a function f such that whenever A i=-Qx#(x, y), then f (lQx+(x, y)) = /3 (E Sz) gives an upper bound for { cr: A k @[a, y]}. Remark 4.3.8. Classically, every standard model is uniformly standard. In the admissible interpretation the Q-valuated uniformly standard structures for L(Q) are simply the recursive structures of Bruce and Keisler.

Generalizing

classical and effective model theory

301

Theorem 4.3.9 (Soundness for L(Q)). ZfA ISa uniformly standard model, then A . is a model for all the axioms of L(Q)(z). Proof. Let ~Qx be denoted

by Fx (few x). The crucial axiom to check is (5)

which can be written as

VxFy$(x, Y) A

8 3~ 44~ Y)+~'Y

3.x@(x, Y)-

Thus, we want to show that if A is a uniformly standard structure, then for any @, A ~V.rFy+(x, First assume
Y) A Fx 3~ $6 Y)+FY 3~ 44~ Y).

(*) A kvsx FY%

and

Y>

(**)

A LFx 3~ $4~ Y).

Using (**) we can define Say rp= {/3: A k 3y @(/3, y)}. If &, + is empty, then we S,, + are done. If it is not empty, then Say+ can be w-enumerated by a g : o % because A is Q-valuated, and the search is bounded by f (1Qx 3y$) (where f is the bounding function for A). Let 6 = sup{gn},<,. By (**) we know that there are only few xs such that 3y #(x, y) and these xs are bounded by 6. Now given any x, A, = { y : A k @(x, y)} is empty when x > 6. Thus in order to o-enumerate {x: A, #$3} we simply have to w-enumerate {x < 6: A k 3y +(x, y)}. Let g: w % {x < 6: A k 3y @(x, y)}. Define f * : w+ 52 by f*(n) = f(lQy#(g(n), y)). Thus, by regularity of &2,3/3(f*:w-,j3). Let S={y:AL3x#(x, y)}. S is bounded by /I. Thus A b Fy 3x #(x, y). This concludes the proof of soundness. 0 4.4. Weak w-enumerable model theory and L(Q)completeness
in FMTn

Kaufmanns completeness proof for L(Q) reduces the completeness problem for L(Q) to model theory for so-called weak models which are special kinds of first-order structures. Accordingly our approach will proceed in two stages. (1) We show how to deal with model theory for weak models in FMTa. (2) We show how to prove the L(Q)-completeness theorem in FMTn. Assume that we have a notion of finitary proof with a deduction theorem for L(Q), a function giving the complexity of formulas in L(Q) (r(G)) and the usual apparatus of functions for developing syntax for L(Q). In the following let r be an w-enumerable language. We now define a translation * from L(Q)(z) formulas to L(Q)(t) formulas where t+ = t U {R+: 41 is an L(Q)(z) formula of the form Qxc$(x)}.

302

P. Mancosu

The arity of R, is Ifree(Qx#)l. Define * as follows: if r#~ atomic, then $I* = @; is if$=qr\x, then#*=$*Ax*; if 9 =-u,IJ, then $* =1$1*; if # =3x I/J, then $J* =3x (rj~*); if 9 = Qxq(x, u), then $* = R+(u). Our aim is to prove the following completeness theorem for L(Q).
Theorem 4.4.1 (Completeness theorem for L(Q)). Let T be an o-enumerable Zf T is consistent, then T has a uniformly f or t w-enumerable.

theory in L(Q)(z) standard model.

The proof of the completeness theorem is much longer than the proof of soundness and hinges on the development of weak w-enumerable model theory in FMT,.
Definition 4.4.2 (Weak models). A*=A@C@R*

A weak model for L(Q)(t)

is a r+-structure

such that R* gives the interpretation for every R, E z+ and such that if $I is an L(Q)(r)-axiom, then (@*, 0) is in Sat,.. When talking about weak models, A* b @[s] interested in o-enumerable weak models.
Definition

means

A* b $*[s].

We are

4.4.3. Let A* and B* be weak o-enumerable

We write A* <B*
Theorem

models for L(Q)(t). iff A c B and A* k $[a] iff B* I=$[a] whenever a E A. and soundness).
Let T be an w-enumerable weak model.

4.4.4 (Weak completeness

Th en T is consistent

class of L(Q)(z).

iff T has an o-enumerable

Proof. As in Theorem

3.3.5.

0 class 2(x) iff

Definition 4.4.5. We say T L(Q)(z)-focally omits an w-enumerable whenever 3x 4 is consistent, so is 3x (@ A la) for some o E 2.

Theorem 4.4.6 (Weak omitting types). Let T be an w-enumerable consistent set of L(Q)(t) sentences. Let {on,m(x): n, m E o} be a fumiZy of o-enumerable L(Q)(z) formulas in a free variable, say x. Zf T locally omits En = {a,,,: m E o} for each n E o, then T has an o-valuated weak model omitting each 2,,. Proof. As in Theorem

3.3.10.

Cl

Generalizing classicaland effective model theory

303

Assume A* is an o-enumerable weak model be a consistent o-enumerable extension of for L(Q)(t). T~lW4*,a),,~ Let WA*, a)aeA which locally omits, for each n E o, o-enumerable classes &(x) of wh ere the Z,,s are given by a double enumeration. Then formulas in L(Q)(t), there exists, uniformly in A* and the enumeration of the Z,,)s, an o-enumerable weak model B* which omits each class Z,, and such that A* <B* where the elementary extension is with respect co z+. Proof. Combine Theorems Elementary chains

Theorem

4.4.7 (Weak extension).

4.4.4 and 4.4.6.

Cl

Since we do not have infinitary class construction, we are able to construct infinite unions of classes only when these classes are given uniformly. Assume fE : w % A,. Then define U 5EaAg = {f&: E E Sz, n E o}. The same applies to enumeration of structures A, = A, G3 C, @ R,.
Definition 4.4.8. We are given a uniform sequence of o-enumerable there exists an f such that fE : o % A, (5 E a). Theorem
structures if

(A&n L(Q)(zz) structure for all LYE B such that cy< p+ z, E ri and Az<A[T, 1 r,. Then A* = IJ SERA,$ = A* @ C* @ R* is an S&valuated weak structure for UrrsR tz such that for all w E Sz, Az<A* 1t,.

4.4.9. Suppose we are given a chain A,* <AT < - . - <AZ < - . . where is a uniform sequence of o-enumerable structures such that AZ in an

structure for U t,. It is G-valuated because Sat,, is also given uniformly (exploit Theorem 3.3.1). Thus Sat,. = UsEnSatAe. The proof that AZ <A* 1zz is as in the standard case. Cl
Definition 4.4.10. Let A* and B* be o-enumerable weak models for L(Q)(t). We say that B* is a precise extension of A* relative to # if G(x) is a formula of L(Q) with parameters in A and (1) A* <B*; (2) A* k Qx@(x) 3 36 E B -A (B* b $[b]); (3) whenever A* ~~QxI,!J for Qxv a sentence B* klq[b] for all b E B -A.

Proof. It is clear that A* is an a-enumerable

with parameters

in A, then

Lemma 4.4.11 (Main lemma). Let A* be an w-enumerable weak model for L(Q)(t) and suppose @(x, p) is a formula of L(Q)(z) with parameters p EA. Then there is a precise extension of A* relative to #. Furthermore, the extension is obtained uniformly in $I and the w-valuation of A*.

304

P. Mancosu

Proof (sketch). There are two cases. Case I. A* klQx#(x, p). Then let B* = A*. Case II. A* k Qx@(x, p). Introduce constants

c, (for each a E A) and a fresh

c a ): A* klQxq(x,

constant c. Define
T,(A*) = {O(c,): A* k O[a]} U {@( c , c ,)} U { T #( c , a)}.

Define for each V(X, a) a class &, such that E,,, = {I/+,
C,)} u {X # Cb:

A* k $J(b, a)}. q which

Each &, is clearly w-enumerable.

Claim 4.4.12. T,(A*) is a consistent w-enumerable class of sentences L(Q)-locally omits &,, for each I/J(X, a) such that A* klQxq(x, a).

Proof. The proof of this claim, although not trivial, makes use only of standard first-order syntactic and semantic manipulations (see [27, pp. 134-1361). 0 Proof of the main lemma. First of all we can doubly o-enumerate {&,: A* L ~QxI+!J(x, a)}. By the extension lemma there is an w-enumerable B* such that B*>A* and B* omits each .Z,,,, where the &,s are given by the double enumeration. Thus, there exists an e E B* (corresponding to c) such that for all

0(c, c,) E &(A*), B* k f3[e, a]. Now, #(c, c,) E T,(A*). Thus B* k $(e, p). Moreover, axioms (1) and (2) insure that A* klQx(x = a) and consequently ~(c =c,) E T,(A*) for all u EA. Thus, B* kl(e =a) for all a EA which in turn implies e E B -A. This shows (2) in the definition of precise extension; (3) is verified by using the fact that B* omits the relevant &s. It is clear from the proof that the construction is uniform in A* and #. q
Uniformity for elementary chains

Our construction of a standard model will proceed by constructing a uniform Q-chain of weak w-enumerable models whose union is a standard model. We think of a structure A, as given by a function fa: w onto\ A,. Each w-enumerable model A, will have domain bounded by ~(1 +/I) (this insures the uniformity of the final model). In the first step of the construction we simply take an o-enumerable weak model for the consistent class of sentences T. At successor stages we use the uniformity of the main lemma to pass from an o-enumerable weak structure AZ to a structure Az+1 satisfying the conditions of the main lemma. Finally at each limit stage il, we take A,* to be the union of the A;T_ for a<il. The following lemma translates our talk of weak models into statements about their enumerations and insures that we will be able to obtain the chain of weak models as a uniform chain. This exploits a form of the recursion theorem.

Generalizing classical and effective model theory

305

Assume we have a function fO: o % A,* and g such that if fWw-enumerates a model AZ, then g(fa, (u) gives an enumeration of a (Uniformity lemma). structure A z+ 1 as in the main lemma. Then there exists an f such that fa! : w % for all a E G. Proof. First notice with hZj: w onto\ A: To obtain Recall function may take A:

Lemma 4.43

that there exists a function (where the uniform

1 such that whenever lh3L enumerates

h is a function lJsCn A; = A:. as follows. Then we to find a

E < A and A E Lii), o-enumerability

1, we exploit

of the ordinals, theorem

that for all (YE S2, ucy: w % 1hAn = h(u(n)(n,))(n,). f such that fo: o % fo(n), fan= g(f (pd a), pd o)n, tfon,

(Y. Let n E w be given as (no, n,). W e now use the recursion

AZ for all a, E G. Define if (Y= 0, if cx = pd(a) + 1, if de Lim. and fo: o % AZ. 0

One finally proves

by induction

on (YE !Z that fly

Lemma

4.4.14. Assume

that fa : w onto\ AZ enumerates a chain of w-enumerable

weak models for L(Q) with the following properties: (1) for all CYE 4 AZ,, is a precise extension of AZ relative to 4 for some @; (2) for each formula @I(X) with parameters in some AZ, {/3 E Sz: A$+, is a precise extension of Al*, relative to c$} is strictly Q-enumerable; (3) A.E Lim-+A,* = U,,&:; (4) each A, is a subset of o(1 + a). Then A = Uas&z is such that A b C#iff A: k $J for C$a sentence with parameters in AZ, and (Y E G. Moreover, A is uniformly standard. Proof. By induction

on C#A The only interesting

case is C#J QXI/J. If AZ b QXI/J, =

then by (2) there exists an Q-enumerable but not o-enumerable subset X of & such that for all p E X, A;,, F ~[y] for some y E AB+l -A,. This implies A k ~[y] for some y EA~+~ -A,. Thus X = {y 136 (y EA~+~ -A, AA~+~ k ~[y])} is unbounded in !Z. Hence A b Qxq(x). To prove the other direction assume AEFlQxq. By definition of precise extension for p > LY,A; k +[y] + y E A,. By the induction hypothesis A k q!~[y]+ y E A,. Thus the class of {y: A t=~[y]} is bounded by any p greater than all y E A,. Thus A LlQxq. SZ-valuation comes from Theorem 4.4.9 and uniformity in the sense of Definition 4.3.7 is a consequence of the fact that each A, had domain bounded by o(l+ Ly). 0

306

P. Mancosu

Theorem 4.4.15 (Completeness

theorem for L(Q)).

Assume T is an w-enumerable

consistent set of sentences in L(Q)(z). Proof.

Then T has a uniformly standard model.

We define a uniform chain (AZ: (Y E 52) such that each AZ is a subset of Sz and UAZ is a strictly G-enumerable subset of Q. We use the pairing function on 52 in order to partition a into &J disjoint many classes X,, where $(x) ranges over formulas with parameters in Sz. Let A,* be given by the weak completeness theorem (in particular we have a function fO: w % A,*). (Assume A,* = [0, w).) Assume we are given an wenumerable structure AZ. By the main lemma we obtain g(Az, (u) =AE+l, a precise extension of AZ relative to # where (YE X,. (If the parameters of 9 do not lie in AZ, let AZ,, =A:.) This step can be performed in such a way as to obtain a domain for A,+1 to be a subset of ~(1 + a). Let A: = IJA: for limit il E 9. By the uniformity lemma we get a fcx:o%Az. By Lemma 4.4.14, Al=@[y] iff Azk@[y] for all (YE Qand YEA:. In particular, since A,* k # for all @ E T, A I=T. A is uniformly standard and S&valuated. 0
Remark 4.4.16. It would be interesting to extend the approach to L(Q) L(w) (for definitions see [27]). In the L(Q) one should try to find a reasonable abstract statement

and

that captures the role played by the hypothesis diamond in the classical proof and by nl-collection in the admissible case. In the L(aa) case one runs against the fact that Ulams partition theorem, which is the cornerstone of the classical proof, is proved by contradiction and uses in an essential way the axiom of choice. This situation is interesting in that Wimmers [41] was able to find a constructive analogue of Ulams partition theorem in the context of admissible set theory, by means of a proof which only seems to work for special kinds of admissible sets and does not generalize to the classical case. Is it possible to find an interesting (i.e., non ad hoc) abstract development in a theory of operations and classes which encompasses the classical and the admissible L(Q) and L( au ) soundness and completeness theorems?

Acknowledgement

The material presented in this article constitutes the main bulk of the authors doctoral dissertation written at Stanford under the guidance of Professor Solomon Feferman. The author would like to express his profound gratitude to Professor Feferman for his constant advice and encouragement.

Generalizing

classical and effective model theory

307

References
[l] J. Barwise, Admissible Sets and Structures (Springer, Berlin, 1975). [2] J. Barwise and J. Schlipf, An introduction to recursively saturated and resplendent models, J. Symbolic Logic 41 (1976) 531-536. [3] M. Beeson, Foundations of Constructive Mathematics (Springer, Berlin, 1984). [4] K.B. Bruce and H.J. Keisler, LA( ), J. Symbolic Logic 44 (1979) 15-28. [5] W. Buchholz, S. Feferman, W. Pohlers and W. Sieg, Iterated Inductive Definitions and Subsystems of Analysis: Recent Proof Theoretical Studies, Lecture Notes in Math. 897 (Springer, Berlin, 1981). [6] A. Cantini, Proprieta e Operazioni (Bibliopolis, Napels, 1983). [7] C.C. Chang and H.J. Keisler, Model Theory, Stud. Logic Found. Math. 73 (North-Holland, Amsterdam, 1973). [8] J.P. Cleave, Hyperarithmetic ultrafilters, in: M.H. Lob, ed., Proc. Summer School in Logic, Leeds 1967, Lecture Notes in Math. 70 (Springer, Berlin, 1968) 223-240. [9] J.P. Cleave, Hyperarithmetic model theory, Unpublished typescript. [lo] J.N. Crossley, A.B. Manaster and M.F. Moses, Recursive categoricity and recursive stability, Ann. Pure Appl. Logic 31 (2,3) (1986) 191-204. [ll] C.W. Culmer, Definability problems in model theory, Ph.D. Thesis, Stanford Univ., CA (1979). [12] N. Cutland, The theory of hyperarithmetic and II:-models. Ph.D. Thesis, Bristol Univ. (1970). [13] N. Cutland, fli-models and II:-categoricity, in: W. Hodges, ed., Conference in Mathematical Logic, London 1970, Lecture Notes in Math. 255 (Springer, Berlin, 1972) 42-62. [14] N. Cutland, Model theory on admissible sets, Ann. Math. Logic 5 (4) (1973) 257-289. [15] Yu.L. Ershov, Decidable Problems and Constructible Models (in Russian) (Nauka, Moscow, 1980). [16] S. Feferman, A language and axioms for explicit mathematics, in: J.N. Crossley, ed., Model Theory and Algebra, Lecture Notes in Math. 450 (Springer, Berlin, 1975) 87-139. [17] S. Feferman, Recursion theory and set theory: a marriage of convenience, in: J.E. Fenstad, R.O. Gandy and G.E. Sacks, eds., Generalized Recursion Theory II, Stud. Logic Found. Math. 94 (North-Holland, Amsterdam, 1978) 55-98. [18] S. Feferman, Constructive theories of functions and classes, in: M. Boffa, D. van Dalen and K. McAloon, eds., Logic Colloquium 78, Stud. Logic Found. Math. 97 (North-Holland, Amsterdam, 1979) 159-224. [19] S. Feferman, Generalizing set theoretical model theory and an analogue theory on admissible sets, in: J. Hintikka, I. Niilinuoto and E. Saarinen, eds., Essays in Mathematical and Philosophical Logic (Reidel, Dordrecht, 1979) 171-195. [20] S. Feferman, Inductively presented systems and the formalization of meta-mathematics, in: D. van Dalen, D. Lascar and T.J. Smiley, eds., Logic Colloquium 80 , Stud. Logic Found. Math. 108 (North-Holland, Amsterdam, 1982) 95-128. [21] S. Feferman, Intensionality in mathematics, J. Philos. Logic 14 (1985) 41-55. [22] S. Feferman, Finitary inductively presented logics, in: R. Ferro, C. Bonotto, S. Valentini and A. Zanardo, eds., Logic Colloquium 88, Stud. Logic Found. Math. 127 (North-Holland, Amsterdam, 1989) 191-220. [23] H.M. Friedman, S.G. Simpson and R.L. Smith, Countable algebra and set existence axioms, Ann. Pure Appl. Logic 25 (2) (1983) 141-181. [24] V. Harnik, Stability theory and set existence axioms, J. Symbolic Logic 50 (1985) 123-137. (251 V. Harnik, Set existence axioms for general (not necessarily countable) stability theory, Ann. Pure Appl. Logic 34 (3) (1987) 231-243. [26] L. Harrington, Recursively presentable prime models, J. Symbolic Logic 39 (1974) 305-309. [27] M. Kaufmann, The quantifier there exist uncountably many and some of its relatives, in: J. Barwise and S. Feferman, eds., Model Theoretical Logics (Springer, Berlin, 1985) 122-176. [28] H.J. Keisler, Logic with the quantifier there exist uncountably many, Ann. Math. Logic 1 (1) (1970) l-93. [29] H.J. Keisler, Model Theory for Infinitary Logic, Stud. Logic Found. Math. 62 (North-Holland, Amsterdam, 1971).

308

P. Mancosu

[30] P. Mancosu, Generalizing classical and effective model theory in theories of operations and classes, Ph.D. Thesis, Stanford Univ., CA (1989). [31] T.S. Millar, Foundations of recursive model theory, Ann. Math. Logic 13 (1) (1978) 45-72. [32] D. Monk, Mathematical Logic (Springer, Berlin, 1976). [33] M. Morley, Decidable model theory, Israel J. Math. 25 (1976) 233-240. [34] C. Parsons, On a number theoretic choice schema and its relation to induction, in: J. Myhill, A. Kino and R.E. Vesley, eds., Intuitionism and Proof Theory, Stud. Logic Found. Math. (North-Holland, Amsterdam, 1970) 459-473. [35] H. Rogers, Theory of Recursive Functions and Effective Computability (McGraw-Hill, New York, 1967). [36] J. Schlipf, Towards model theory through recursive saturation, J. Symbolic Logic 43 (1978) 183-206. [37] S.G. Simpson, Reverse mathematics, in: A. Nerode and R. Shore, eds., Recursion Theory, Proc. Sympos. Pure Math. 42 (Amer. Mathematical Sot., Providence, RI, 1985) 461-471. [38] S.G. Simpson, Subsystems of Second Order Arithmetic, to appear. [39] C. Smorynski, The incompleteness theorems, in: J. Barwise, ed., Handbook of Mathematical Logic, Stud. Logic Found. Math. 90 (North-Holland, Amsterdam, 1977) 821-865. [40] A. Tarski, A. Mostowski and R. Robinson, Undecidable Theories (North-Holland, Amsterdam, 1953). [41] E. Wimmers, Interactions between quantifiers and admissible sets, Ph.D. Thesis, Univ. Wisconsin (1982).