In [2] Vaught showed that if T is a complete theory formalized in the first-order predicate calculus, then it is not possible for T to have exactly (up to isomorphism) two countable models. In this note we extend his methods to obtain a theorem which implies the above.

First some definitions. We define Fn(T) to be the set of well-formed formulas (wffs) in the language of T whose free variables are among x1 x2, …, xn. An n-type of T is a maximal consistent set of wffs of Fn(T); equivalently, a subset P of Fn(T) is an n-type of T if there is a model M of T and elements a1, a2, …, an of M such that M ⊧ ϕ(a1, a2, …, an) for every ϕ ∈ P. In the latter case we say that 〈a1, a2, …, an〉 ony realizes P in M. Every set of wffs of Fn(T) which is consistent with T can be extended to an n-type of T.

This paper resolves 3 problems left open by R. M. Robinson in [3].

We recall that the set of primitive recursive functions is the closure under (i) substitution (or “composition”), and (ii) recursion, of the set P consisting of the zero, successor and projection functions (see any textbook, for instance p. 120 of [2]).

In spite of the work of Gödel and Cohen, which showed the undecidability of the Generalized Continuum Hypothesis (GCH) from the axioms of set theory, the problem still remains to decide GCH on the basis of new axioms. It is almost 100 years since Cantor first conjectured the Continuum Hypothesis, yet we seem to be no closer to determining its truth (or falsity). Nevertheless, it is a sound methodological principle that given any undecidable set-theoretical statement, we should search for “other (hitherto unknown) axioms of set theory which a more profound understanding of the concepts underlying logic and mathematics would enable us to recognize as implied by these concepts” (see Gödel [7, p. 265]).

A theory T is said to be categorical in power κ iff T has a model of power κ and any two models of power κ are isomorphic.

It was conjectured by Morley [4] that if T is a theory in a language with κ > ω symbols and T is categorical in power κ, then T has a model of power < κ. The aim of this paper is to prove the following theorem.

Theorem A. Let κ be a regular cardinal such that ω < κ < 2ω. Let T be a theory in a language with κ symbols such that T is categorical in power κ. Then:

(a) T has a model of power < κ.

(b) T is categorical in all powers μ ≥ κ.

The notion of a recursive function with type-2 arguments was introduced by Kleene [4]. Soon E, the type-2 object that introduces numerical quantification, began to play a central role in the development of the theory. First, Kleene [4, XLVIII] proved that the hyperarithmetical functions are exactly the functions recursive in E. Later, Gandy [1, p. 14] proved the existence of a selection operator recursive in E (that is, some ψ(х, ), partial recursive in E, having the property that, if {х}(y, ) converges for some y, then ψ(х, ) converges and is such a y).

The notion of algebraic closedness plays an important part in the theory of commutative fields. The corresponding notion in the theory of ordered fields is (not only intuitively but in a sense which can be made precise in a metamathematical framework, compare [4]) that of a real closed ordered field. Several suggestions have been made (see [2] and [8]) for the formulation of corresponding concepts in the theory of groups and in the theory of skew fields (division rings, noncommutative fields). Here we present a concept of this kind, which preserves the principal metamathematical properties of algebraically closed commutative fields and which applies to a wide class of first order theories K, including the theories of commutative and of skew fields and the theories of commutative and of general groups.

Let ε stand for the set of nonnegative integers (numbers), V for the class of all subcollections of ε (sets), Λ for the set of isols, and for the set of mappings from a subset of ε into ε (functions). I f is a function we write δf and ρf for its domain and range respectively. The relation of inclusion is denoted by ⊂ and that of proper inclusion by ⊊. The sets α and β are recursively equivalent [written: α ≃ β], if δf = α and ρf = β for some function f with a one-to-one partial recursive extension f. We denote the recursive equivalence type of α, {σ ∈ V ∣ ≃ α}, by Req(α). Also R stands for Req(ε), while ΛR denotes the collection of all regressive isols. The reader is assumed to be familiar with the contents of [1] and [6].

A pair of sets (A0, A1) forms a minimal pair if A0 and A1 are nonrecursive, and if whenever a set B is recursive both in A0 and in A1 then B is recursive. C. E. M. Yates [8] and independently A. H. Lachlan [4] proved the existence of a minima] pair of recursively enumerable (r.e.) sets thereby establishing a conjecture of G. E. Sacks [6]. We simplify Lachlan's construction, and then generalize this result by constructing two disjoint pairs of r.e. sets (A0, B0) and (A1B1) such that if C0 separates (A0, A1 and C1 separates (B0, B1), then C0 and C1 form a minimal pair. (We say that C separates (A0, A1) if A0 ⊂ C and C ∩ = ∅.) The question arose in our study of (Turing) degrees of members of certain classes, where we proved the weaker result [2, Theorem 4.1] that the above pairs may be chosen so that C0 and C2 are merely Turing incomparable. (There we used a variation of the weaker result to improve a result of Scott and Tennenbaum that no complete extension of Peano arithmetic has minimal degree.)

In [1], various formal proof systems for infinitary formulas were defined. The formal proof system is the result of extending the basic predicate calculus by adding a collection Σ of axiom schemes and a collection Ω of rules of inference. Let Taut be the collection of all infinitary prepositional tautologies, considered as axiom schemes. Let ΩI consist of all the quantificational rules of independent choices. We will show, in §2 (see Theorem 2.1), that (Taut; 0) is not complete for L∞ω (i.e., infinitary finite-quantifier) sentences; that is, we will exhibit an L∞ω sentence ϕ such that ¬ϕ is true in all models, but ¬ϕ is not provable in (Taut; 0). (The unprovability is shown by a weak forcing version of Boolean general models.) This answers a question of Karp in [1,12.1(i)]. In §4, we will show that our ϕ is “ complete for L∞ω ) sentences.”

S. A. Kripke has given [6] a very simple notion of model for intuitionistic predicate logic. Kripke's models consist of a quasi-ordering (C, ≤) and a function ψ which assigns to every c ∈ C a model of classical logic such that, if c ≤ c′, ψ(c′) is greater or equal to ψ(c). Grzegorczyk [3] described a class of models which is still simpler: he takes, for every ψ(c), the same universe. Grzegorczyk's semantics is not adequate for intuitionistic logic, since the formula

where х is not free in α. holds in his models but is not intuitionistically provable. It is a conjecture of D. Klemke that intuitionistic predicate calculus, strengthened by the axiom scheme (D), is correct and complete with respect to Grzegorczyk's semantics. This has been proved independently by D. Klemke [5] by a Henkinlike method and me; another proof has been given by D. Gabbay [1]. Our proof uses lattice-theoretical methods.

The purpose of this paper is twofold. In §1 and §2 which are largely expository we develop the known theory of ℵ1-categoricity in terms of strongly minimal sets. In §3 we settle affirmatively Vaught's conjecture that a complete ℵ1-categorical theory has either just one or just ℵ0 countable models, and in §4 we present an example which serves to illustrate the ideas of §3.

As far as we know the only work published on strongly minimal sets is that of Marsh [3]. The present exposition goes beyond [3] in showing that any ℵ-categorical theory has a principal extension in which some formula is strongly minimal.

A second order formula is called Π1 if, in its prenex normal form, all second order quantifiers are universal. A sequent F1, … Fm → G1 …, Gn is called Π1 if a formula

is Π1

If we consider only Π1 sequents, then we can easily generalize the completeness theorem for the cut-free first order predicate calculus to a cut-free Π1 predicate calculus.

In this paper, we shall prove two interpolation theorems on the Π1 sequent, and show that Chang's theorem in [2] is a corollary of our theorem. This further supports our belief that any form of the interpolation theorem is a corollary of a cut-elimination theorem. We shall also show how to generalize our results for an infinitary language. Our method is proof-theoretic and an extension of a method introduced in Maehara [5]. The latter has been used frequently to prove the several forms of the interpolation theorem.

It is natural, given the usual iterative description of the universe of sets, to investigate set theories which in some way take account of the unfinished character of the universe. We do not here consider any arguments aimed at justifying one system over another, or at clarifying the basic philosophy. Rather, we look at an obvious candidate which is similar to a system discussed by L. Pozsgay in [1]. Pozsgay sketched the development of the ordinary theorems in such a system and attempted to show it equiconsistent with ZF. In this paper we show that the consistency of the system we call IZF can be proved in the usual ZF set theory.

In his paper [1] Chang provides among other things answers to questions of the following type: Given two models and of powers α and β, respectively, what is the least λ such that implies His proofs are by induction on the quantifier rank of formulas and they use an idea which in the case of ordinary first-order language goes back to Ehrenfeucht and Fraïssé. But, as we show, one can easily prove that if λ is big compared with κ and with the cardinality of the universe of the structure , then every L∞κ-formula is equivalent modulo the set of all Lλκ-sentences which hold in to a Lλκ-formula. From this, Chang's results follow immediately. The same method can be applied to similar problems concerning generalized languages.

Let W0, W1 … be one of the usual enumerations of recursively enumerable (r.e.) subsets of the set N of nonnegative integers. (Background information will be given later.) Suggestions of Anil Nerode led to the following

Definitions. Let B be a subset of N and let ψ be a partial recursive function.

In Chapter XIII of [4], Prior discusses a system QKt, designed to stand to the “minimal” tense logic Kt as the modal system Q of [3] stands to S5. In this paper I provide semantics for a similar system, slightly weaker than QKt: the weakening is due to the fact that Prior's axioms are slightly too strong for a “minimal” system. An extended post-Henkin style completeness proof for the axiomatization with respect to the semantics provided is then given: the underlying three-valued nature of the semantics requires a twist in the proof which is new to its author at least, and also results in some details being set out which could well be glossed over in the two-valued case.