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.

It is shown that the first-order theory ThR(A) of a countable module over an arbitrary countable ring R is ℵ0-categorical if and only if Ai finite, n ∈ ω, κi ≤ ω. Furthermore, ThR(A) is ℵ0-categorical for all R-modules A if and only if R is finite and there exist only finitely many isomorphism classes of indecomposable R-modules.

The study of countable theories categorical in some uncountable power was initiated by Łoś and Vaught and developed in two stages. First, Morley proved (1962) that a countable theory categorical in some uncountable power is categorical in every uncountable power, a conjecture of Łoś. Second, Baldwin and Lachlan confirmed (1969) Vaught's conjecture that a countable theory categorical in some uncountable power has either one or countably many isomorphism types of countable models. That result was obtained by pursuing a line of research developed by Marsh (1966). For certain well-behaved theories, which he called strongly minimal, Marsh's method yielded a simple proof of Łoś's conjecture and settled Vaught's conjecture.

In recent years efforts have been made to extend these results to uncountable theories. The generalized Łoś conjecture states that a theory T categorical in some power greater than ∣T∣ is categorical in every such power. It was settled by Shelah (1970). Shelah then raised the question of the models in power ∣T∣ = ℵα of a theory T categorical in ∣T∣+, conjecturing in [S3] that there are exactly ∣α∣ + ℵ0 such models, up to isomorphism. This conjecture provided the initial motivation for the present work. We define and study semi-minimal theories analogous in some ways to Marsh's strongly minimal (countable) theories. We describe the models of a semi-minimal theory T which contain an infinite indiscernible set. Besides throwing some light on Shelah's conjecture, our method gives simple proofs of the Łoś conjecture and of the Morley conjecture on categoricity in ∣T∣, in the case of a semi-minimal theory T. Other results as well as some examples are provided.

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.

In [5] Gödel interpreted Peano arithmetic in Heyting arithmetic. In [8, p. 153], and [7, p. 344, (iii)], Kreisel observed that Gödel's interpretation extended to second order arithmetic. In [11] (see [4, p. 92] for a correction) and [10] Myhill extended the interpretation to type theory. We will show that Gödel's negative interpretation can be extended to Zermelo-Fraenkel set theory. We consider a set theory T formulated in the minimal predicate calculus, which in the presence of the full law of excluded middle is the same as the classical theory of Zermelo and Fraenkel. Then, following Myhill, we define an inner model S in which the axioms of Zermelo-Fraenkel set theory are true.

More generally we show that any class X that is (i) transitive in the negative sense, ∀x ∈ X∀y ∈ x ¬ ¬ x ∈ X, (ii) contained in the class St = {x: ∀u(¬ ¬ u ∈ x→ u ∈ x)} of stable sets, and (iii) closed in the sense that ∀x(x ⊆ X ∼ ∼ x ∈ X), is a standard model of Zermelo-Fraenkel set theory. The class S is simply the ⊆-least such class, and, hence, could be defined by S = ⋂{X: ∀x(x ⊆ ∼ ∼ X→ ∼ ∼ x ∈ X)}. However, since we can only conservatively extend T to a class theory with Δ01-comprehension, but not with Δ11-comprehension, we will give a Δ01-definition of S within T.

§1. A complete atomic modal algebra (CAMA) is a complete atomic Boolean algebra with an additional completely additive unary operator. A (Kripke) frame is just a binary relation on a nonempty set. If is a frame, then is a CAMA, where mX = {y ∣ (∃x)(y < x Є X)}; and if is a CAMA then is a frame, where is the set of atoms of and b1 < b2 ⇔ b1 ∩ mb2 ≠∅.

Now , and the validity of a modal formula on is equivalent to the satisfaction of a modal algebra polynomial identity by and conversely, so the validity-preserving constructions on frames ought to be in some sense equivalent to the identity-preserving constructions on CAMA's. The former are important for modal logic, and many of the results of universal algebra apply to the latter, so it is worthwhile to fix precisely the sense of the equivalence.

The most important identity-preserving constructions on CAMA's can be described in terms of homomorphisms and complete homomorphisms. Let and be the categories of CAMA's with homomorphisms and complete homomorphisms, respectively. We shall define categories and of frames with appropriate morphisms, and show them to be dual respectively to and . Then we shall consider certain identity-preserving constructions on CAMA's and attempt to describe the corresponding validity-preserving constructions on frames.

The proofs of duality involve some rather detailed calculations, which have been omitted. All the category theory a reader needs to know is in the first twenty pages of [7].

Although a variety of proofs are available for the Craig-Lyndon Interpolation Lemma, they all seem to make essential use of negation, with the result that they are inapplicable to deductive theories in which negation cannot be expressed. It is here shown that this use of negation can be avoided by extending the Interpolation Lemma to the pure implicational calculus PCI.

Determinate Parameter Lemma. For each formula A, ⊨PA ⊃ A for some sentence parameter PA occurring in A.

Proof. By induction on the construction of A.

Interpolation Lemma For PCI. Let Γ be the set of sentence parameters common to A and C.If ⊨A ⊃ and C is not valid, then there is a formula B containing no sentence parameter not in Y such that ⊨A ⊃ B and ⊨B ⊃ C.

Proof. Since ⊨PA ⊃ A by the Determinate Parameter Lemma and ⊨A ⊃ C, ⊨PA ⊃ C. But C is by hypothesis an invalid formula, so PA must occur in C as well as in A. Thus PA Є Γ.

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λ.