The original aim of this paper was to show that forcing provided a useful and unifying tool in the model theory of finite and admissible languages. Roughly speaking, any result obtained by a Henkin proof, by Makkai's method or by an omitting type argument can be given an alternative proof via forcing. Finally, instead of giving new proofs of a number of known theorems, we have chosen to focus on the interpolation theorem for many-sorted languages. The main result of this paper is thus a generalization of Feferman's theorems ([2], [3]) with a completely different proof; this was announced in [8] and [9].

For more on forcing techniques in model theory the reader should consult [4] as well as [5]. He should also compare forcing and boolean-valued models developed in [6] for the classical case and in [7] for admissible languages. Throughout the paper familiarity with the standard concepts of model theory is assumed.

The author wishes to express his gratitude to J. L. Krivine and K. McAloon for supervising his work. Thanks are also due to J. P. Ressayre for helpful suggestions and to R. L. Vaught for an interesting discussion on forcing in model theory. Finally, an interesting application has been pointed out by S. Feferman and has been included with his permission.

It is long known that Lawvere's theory in The category of categories as foundations of mathematics A[1] does not work, as indicated in Ishell's review [0]. Isbell there gives a counterexample that CDT—Category Description Theorem—[1, p. 15] is in fact not a theorem of BT (the Basic Theory of [1]) and suggests adding CDT to the axioms.

Our starting point was the claim in [1] that “the basic theory needs no explicit axiom of infinity.” We define a model ℳ of BT in which all categories are finite. In particular, the “monoid of nonnegative integers N” coincides in ℳ with the terminal object 1. We study ℳ in some detail in order to establish the true status of various “theorems” or “metatheorems” of BT: The metatheorem of [1, p. 11] saying that the discrete categories form a category of sets, CDT, the theorem on p. 15, and the theorem on p. 16 of [1] are all nontheorems. The remaining results indicated in [1] concerning BT are provable. However, as the Predicative Functor Construction Schema—PFCS—are justified in [1] by using the “metatheorem” and CDT, we provide a proof of these two schemata by showing that the discrete categories of BT (or of convenient extensions of BT) form a two-valued Boolean topos.

We study in this paper characterizations of various interesting classes of relations arising in recursion theory. We first determine which Spector classes on the structure of arithmetic arise from recursion in normal type 2 objects, giving a partial answer to a problem raised by Moschovakis [8], where the notion of Spector class was first essentially introduced. Our result here was independently discovered by S. G. Simpson (see [3]). We conclude our study of Spector classes by examining two simple relations between them and a natural hierarchy to which they give rise.

The second part of our paper is concerned with finding structural characterizations of classes of relations on the reals in the spirit of Moschovakis [7]. Our main result provides a single abstract characterization for the class of relations on the reals and the 2-envelope of 3E, the first one being valid if projective determinacy is true, the second if V = L is true.

The usual semantics for the modal systems T, S4, and S5 assumes that the set of possible worlds contains at least one member. Recently versions of these modal systems have been developed in which this assumption is dropped. The systems discussed here are obtained by slightly weakening the liberated versions of T and S4. The semantics does not assume the existence of possible worlds, and the accessibility relation between worlds is only required to be quasi-reflexive instead of reflexive. Completeness and independence results are established.

In [7] we proved that (I) if T is a countable ℵ0-categorical theory without finite models then T has a model companion; and several people have observed that (II) if T is a countable theory without finite models which is ℵ1-categorical and forcingcomplete for infinite forcing (i.e., T= TF) then T is model-complete. It is natural to ask (1) whether in (I) we can replace ℵ0 by ℵ1; (2) whether in (II) we can replace TF by Tf; and (3) in connection with (II), whether the categoricity of the class of infinitely generic structures for a theory K in some or all infinite powers implies the existence of a model companion for K. The purpose of this note is to provide negative answers to (1), (2), and (3). Specifically, we will prove:

Theorem. There exists a countable theory T such that

(i) T has no finite models and is ℵ-categorical;

(ii) T is forcing-complete for finite forcing, i.e., T = Tf;

(iii) T has no model companion (i.e., in light of (ii), T is not model-complete);

(iv) the class of infinitely generic structures for T is categorical in every infinite power;

(v) every uncountable existentially complete structure for T is infinitely generic;

(vi) there is, up to isomorphism, precisely one countable existentially complete model of Tf, and there are no uncountable e.c. models of Tf (in particular, there is just one countable finitely generic structure and there are no uncountable ones);

(vii) there are precisely ℵ0isomorphism types of countable existentially complete structures for T.

In the early days of the development of Kripke-style semantics for modal logic a great deal of effort was devoted to showing that particular axiom systems were characterised by a class of models describable by a first-order condition on a binary relation. For a time the approach seemed all encompassing, but recent work by Thomason [6] and Fine [2] has shown it to be somewhat limited—there are logics not determined by any class of Kripke models at all. In fact it now seems that modal logic is basically second-order in nature, in that any system may be analysed in terms of structures having a nominated class of second-order individuals (subsets) that serve as interpretations of propositional variables (cf. [7]). The question has thus arisen as to how much of modal logic can be handled in a first-order way, and precisely which modal sentences are determined by first-order conditions on their models. In this paper we present a model-theoretic characterisation of this class of sentences, and show that it does not include the much discussed LMp → MLp.

Definition 1. A modal frame ℱ = 〈W, R〉 consists of a set W on which a binary relation R is defined. A valuation V on ℱ is a function that associates with each propositional variable p a subset V(p) of W (the set of points at which p is “true”).

In a recent paper [3] H. Gaifman investigated some model theoretic consequences of Matijasevič's theorem [5], and posed some further problems which naturally arise. We provide here partial answers to two of these problems, the results having been previously announced in the postscript of [3].

Firstly, it is shown in [3] that if M1 and M2 are models of the Peano axioms P and M1 ⊆ M2, then M1 is closed under the recursive functions of M2. The converse of this statement is false. Moreover, Gaifman asks: Is every initial segment of a model M of P which is closed under the recursive functions of M (or the ∑n-definable functions) also a model of P? We show that this is false and our method gives, en route, another proof of a theorem of Rabin [7] stating the P is not implied by any consistent set of ∑n sentences for any n.

Secondly, we partially answer a question posed on p. 129 of [3] by proving (some-what more than) every countable nonstandard model of P has an end extension in which a diophantine equation, not solvable in the original model, has a solution. We can, in fact, take the new model to be isomorphic to the original one. This generalises (apart from the countability restriction) a theorem of Rabin [6].

Takeuti [6] has suggested the need for higher axioms for set theory which are analogous to higher axioms of infinity, but which claim that power sets are in some sense large. In this paper we investigate a reflection axiom of this sort (Axiom T).

In §1, we introduce Axiom T and explore some related axioms. A technical lemma involving an elementary embedding is developed in §2 which allows us, in §3, to prove the relative consistency of Axiom T.

The reader is assumed to be familiar with ramified forcing languages and the usual techniques of forcing. A suitable treatment of these subjects is given by Takeuti and Zaring [7].

ZFC, GBC, ZF and GB are the set theories of Zermelo-Fraenkel and of Gödel-Bernays, with and without the axiom of choice (AC). CH is the continuum hypothesis.

For α an ordinal, define

For p1, p2 ∈ pα let p1 ≤ p2 mean that p1 ⊇ p2 (thus p1 is the stronger forcing condition). It is well known that Pα satisfies the countable chain condition [5].

Consider modal propositional formulae, constructed using proposition-letters, connectives and the modal operators □ and ⋄. The semantic structures are frames, i.e., pairs <W, R> with R ⊆ W2. Let F, V be variables ranging respectively over frames and functions from the set of proposition-letters into the powerset of W. Then the relation

may be defined, for arbitrary formulae α, following the Kripke truth-definition. From this relation we may further define

Now, to every modal formula α there corresponds some property Pα of R. A particular example is obtained by considering the well-known translation of modal formulae into formulae of monadic second-order logic with a single binary first-order predicate. For these particular Pα we have

for all F and w ∈ W. These formulae Pα are, however, rather intractable and more convenient ones can often be found. An especially interesting case occurs when Pα may be taken to be some first-order formula. For example, it can be seen that

for all F and w ∈ W. It is customary to talk about a related correspondence, namely when for all F we have

Note that this correspondence holds whenever the first one above holds.

Our unexplained notation is that of Rogers [4]. Let P ⊆ 2N × 2N. We call a sequence <An: n ∈ N> of subsets of N a P-sequence iff ∀n(An+1 = the unique B such that P(An, B)).

Theorem. Let P ⊆ 2N × 2N be arithmetical. Then there is no P-sequence <An: n ∈ N> such that ∀n(A′n+1 ≤T An).

This theorem improves a result of Friedman [2] who showed that for no arithmetical P is there a P-sequence <An: n ∈ N> such that An + 1 is a code for an ω-model of the relative arithmetic comprehension schema, and An + 1 is present in the model coded by An, for all n. Other related results are those of Harrison [3], who showed there is a sequence <An: n ∈ N> such that ∀n<A′n + 1 ≤T An>, and of Enderton and Putnam [1], who showed there is no sequence <An: n ∈ N> with ∀n(A′n + 1 ≤T An) and A0 hyperarithmetic.

Our theorem is closely connected to Gödel's second incompleteness theorem. Its proof is a recursion theoretic parallel to the proof of Gödel's theorem. In §2 we draw a version of Gödel's theorem as a corollary to ours.

Among the earliest and best-known theorems on the decision problem is Skolem's result [7] that the class of all closed formulas with prefixes of the form ∀···∀∃···∃ is a reduction class for satisfiability for the whole of quantification theory. This result can be refined in various ways. If the Skolem prefix alone is considered, the best result [8] is that the ∀∀∀∃ class is a reduction class, for Gödel [3], Kalmár [4], and Schütte [6] showed the ∀∀∃···∃ class to be solvable. The purpose of this paper is to describe the more complex situation that arises when (Skolem) formulas are restricted with respect to the arguments of their atomic subformulas. Before stating our theorem, we must introduce some notation.

Let x, y1, y2, be distinct variables (we shall use v1, v2, ··· and w1, w2, ··· as metavariables ranging over these variables), and for each i ≥ 1 let Y(i) be the set {y1, ···, yi}. An atomic formula Pv1 ··· vk will be said to be {v1, ···, vk}-based. For any n ≥ 1, p ≥ 1, and any subsets Y1, ··· Yp of Y(n), let C(n, Y1, ···, Yp) be the class of all those closed formulas with prefix ∀y1 ··· ∀yn∃x such that each atomic subformula not containing the variable x is Yi-based for some i, 1 ≤ i ≤ p.

In [1] it was claimed that the word problem for free fields with infinite centre can be solved. In fact it was asserted that if K is a skew field with infinite central subfield C, then the word problem in the free field on a set X over K can be solved, relative to the word problem in K.

As G. M. Bergman has pointed out (in a letter to the author), it is necessary to specify rather more precisely what type of problem we assume to be soluble for K: We must be able to decide whether or not a given finite set in K is linearly dependent over its centre. This makes it desirable to prove that the free field has a corresponding property (and not merely a soluble word problem). This is done in §2; interestingly enough it depends only on the solubility of the word problem in the free field (cf. Lemma 2 and Theorem 1′ below).

Bergman also notes that the proof given in [1] does not apply when K is finite-dimensional over its centre; this oversight is rectified in §4, while §3 lifts the restriction on C (to be infinite). However, we have to assume C to be the precise centre of K, and not merely a central subfield, as claimed in [1].

I am grateful to G. M. Bergman for pointing out the various inaccuracies as well as suggesting remedies.

We shall apply some of the results of Jensen [4] to deduce new combinatorial consequences of the axiom of constructibility, V = L. We shall show, among other things, that if V = L then for each cardinal λ there is a set A ⊆ λ such that neither A nor λ – A contain a closed set of type ω1. This is an extension of a result of Silver who proved it for λ = ω2, providing a partial answer to Problem 68 of Friedman [2].

The main results of this paper were obtained independently by both authors.

If λ is an ordinal, E is said to be Mahlo (or stationary) in λ, if λ – E does not contain a closed cofinal subset of λ.

Consider the statements:

(J1) There is a class E of limit ordinals and a sequence Cλ defined on singular limit ordinals λ such that

(i) E ⋂ μ is Mahlo in μ for all regular > ω;

(ii) Cλ is closed and unbounded in λ;

(iii) if γ < is a limit point of Cλ, then γ is singular, γ ∉ E and Cγ = γ ⋂ Cλ.

For each infinite cardinal κ:

(J2,κ) There is a set E ⊂ κ+ and a sequence Cλ(Lim(λ), λ < κ+) such that

(i) E is Mahlo in κ+;

(ii) Cλ is closed and unbounded in λ;

(iii) if cf(λ) < κ, then card Cλ < κ;

(iv) if γ < λ is a limit point of Cλ then γ ∉ E and Cγ = ϣ ⋂ Cλ.