The central notion of this paper is that of a (conjunctive) game-sentence, i.e., a sentence of the form

where the indices ki, ji range over given countable sets and the matrix conjuncts are, say, open -formulas. Such game sentences were first considered, independently, by Svenonius [19], Moschovakis [13]—[15] and Vaught [20]. Other references are [1], [3]—[5], [10]—[12]. The following normal form theorem was proved by Vaught (and, in less general forms, by his predecessors).

Theorem 0.1. Let L = L0(R). For every -sentence ϕ there is an L0-game sentence Θ such that ⊨′ ∃Rϕ ↔ Θ.

(A word about the notations: L0(R) denotes the language obtained from L0 by adding to it the sequence R of logical symbols which do not belong to L0; “⊨′α” means that α is true in all countable models.)

0.1 can be restated as follows.

Theorem 0.1′. For every-sentence ϕ there is an L0-game sentence Θ such that ⊨ϕ → Θ and for any-sentence ϕ if ⊨ϕ → ϕ and L′ ⋂ L ⊆ L0, then ⊨ Θ → ϕ.

(We sketch the proof of the equivalence between 0.1 and 0.1′.

0.1 implies 0.1′. This is obvious once we realize that game sentences and their negations satisfy the downward Löwenheim-Skolem theorem and hence, ⊨′α is equivalent to ⊨α whenever α is a boolean combination of and game sentences.

A well-known result of Vaught's is that no complete theory has exactly two nonisomorphic countable models. The main result of this paper is that there is a complete decidable theory with exactly two nonisomorphic decidable models.

A model is decidable if it has a decidable satisfaction predicate. To be more precise, let T be a decidable theory, let {θn∣n < ω} be an effective enumeration of all formulas in L(T), and let be a countable model of T. For any indexing E = {ai∣ i < ω} of ∣∣, and any formula ϕ ∈ L(T), let ‘ϕE’ denote the result of substituting ‘ai’ for every free occurrence of ‘xi’ in ϕ, i < ω. Then is decidable just in case, for some indexing E of ∣∣, {n ∣ ⊨ θnE} is a recursive set of integers. It is easy to show that the decidability of a model does not depend on the choice of the effective enumeration of the formulas in L(T); we omit details. By a simple ‘effectivization’ of Henkin's proof of the completeness theorem (see Chang [1]) we have

Fact 1. Every decidable consistent theory has a decidable model.

Assume next that T is a complete decidable theory and {θn ∣ n < ω} is an effective enumeration of all formulas of L(T).

We present a number of results involving almost disjoint sets and Martin's axiom. Included is an example, due to K. Kunen, of a c.c.c. partial order without property K whose product with every c.c.c. partial order is c.c.c.

Let T be a complete countable first-order theory such that every ultrapower of a model of T is saturated. If T has a model omitting a type p in every cardinality < ℶ′, then T has a model omitting p in every cardinality. There is also a related theorem, and an example showing the ℶ′ cannot be improved.

For general information on bar recursion the reader should consult the papers of Spector [8], where it was introduced, Howard [2] and Tait [11]. In this note we shall prove that the terms of Gödel's theory T(in its extensional version of Spector [8]) are closed under the rule BR0,1 of bar recursion of types 0 and 1. Our method of proof is based on the notion of an infinite term introduced by Tait [9]. The main tools of the proof are (i) the normalization theorem for (notations for) infinite terms and (ii) valuation functionals. Both are elaborated in [6]; for brevity some familiarity with this paper is assumed here. Using (i) and (ii) we reduce BR0,1 to ξ-recursion with ξ < ε0. From this the result follows by work of Tait [10], who gave a reduction of 2ξ-recursion to ξ-recursion at a higher type. At the end of the paper we discuss a perhaps more natural variant of bar recursion introduced by Kreisel in [4].

Related results are due to Kreisel (in his appendix to [8]), who obtains results which imply, using the reduction given by Howard [2] of the constant of bar recursion of type τ to the rule of bar recursion of type (0 → τ) → τ, that T is not closed under the rule of bar recursion of a type of level ≥ 2, to Diller [1], who gave a reduction of BR0,1 to ξ-recursion with ξ bounded by the least ω-critical number, and to Howard [3], who gave an ordinal analysis of the constant of bar recursion of type 0. I am grateful to H. Barendregt, W. Howard and G. Kreisel for many useful comments and discussions.

The notion of forking has been introduced by Shelah, and a full treatment of it will appear in his book on stability [S1]. The principal aim of this paper is to show that it is an easy and natural notion.

Consider some well-known examples of ℵ0-stable theories: vector spaces over Q, algebraically closed fields, differentially closed fields of characteristic 0; in each of these cases, we have a natural notion of independence: linear, algebraic and differential independence respectively. Forking gives a generalization of these notions. More precisely, if are subsets of some model and c a point of this model, the fact that the type of c over does not fork over means that there are no more relations of dependence between c and than there already existed between c and . In the case of the vector spaces, this means that c is in the space generated by only if it is already in the space generated by . In the case of differentially closed fields, this means that the minimal differential equations of c with coefficient respectively in and have the same order. Of course, these notions of dependence are essential for the study of the above mentioned structures. Forking is no less important for stable theories. A glance at Shelah's book will convince the reader that this is the case.

What we have to do is the following. Assuming T stable and given and p a type on , we want to distinguish among the extensions of p to some of them that we shall call the nonforking extensions of p.

We are often told, correctly, that modern logic originated with Frege. For Frege clearly depicted polyadic predication, negation, the conditional, and the quantifier as the bases of logic; moreover, he introduced the idea of a formal system, and argued that mathematical demonstrations, to be fully precise, must be carried out within a formal language by means of explicitly formulated syntactic rules.

Consequently Frege has often been read as providing all the central notions that constitute our current understanding of quantification. For example, in his recent book on Frege [1973], Michael Dummett speaks of ”the semantics which [Frege] introduced for formulas of the language of predicate logic.” That is, “An interpretation of such a formula … is obtained by assigning entities of suitable kinds to the primitive nonlogical constants occurring in the formula … [T]his procedure is exactly the same as the modern semantic treatment of predicate logic” (pp. 89–90). Indeed, “Frege would therefore have had within his grasp the concepts necessary to frame the notion of the completeness of a formalization of logic as well as its soundness … but he did not do so” (p. 82).

This common appraisal of Frege's work is, I think, quite misleading. Even given Frege's tremendous achievements, the road to an understanding of quantification theory was an arduous one. Obtaining such understanding and formulating those notions which are now common coin in the discussion of logical systems were the tasks of much of the work in logic during the nineteen-twenties.

With PC understood to be the propositional calculus of [3], call a binary function Pr from the wffs of PC to the reals a Carnap (probability) function if it meets requirements A1—A5 in Table I (with ‘⊢…’ short in A3—A4 for ‘… is a tautology’), and call the function a Popper (probability) function if it meets requirements Bl—B6 there:

Leblanc established in [3] that every Carnap function is a Popper one, and he tendered proof of the converse. As reported by Stalnaker in [5], the proof unfortunately was incomplete, a mishap due to Leblanc's abbreviating ‘Pr(A, ∼ A) = 1’ as ‘⊢ A’ when Pr is a Popper function. Borrowing from [4], Leblanc did show, as Harper notes in [2, footnote 17], that

(1) If Pr is a Popper function and A is a tautology, then Pr(A, ∼ A) = 1. He did not, however, show that

(2) If Pr is a Popper function and Pr(A, ∼ A) = 1, then A is a tautology.

Nor could he have done so: (2) is false, as the simplest of counterexamples shows. Denied (2), Leblanc had no hope of proving that every Popper function is a Carnap one: of a Popper function Pr it is easily ascertained that Pr meets requirement A4 if and only if Pr(A, ∼ A) = 1 just in case A is a tautology.

Let A be a standard transitive admissible set. Σ1-separation is the principle that whenever X and Y are disjoint Σ1A subsets of A then there is a ⊿1A subset S of A such that X ⊆ S and Y ∩ S = ∅.

Theorem. If satisfies Σ-separation, then

(1) If 〈Tn∣n < ω) ϵ A is a sequence of trees on ω each of which has at most finitely many infinite paths in A then the function n ↦ (set of infinite paths in A through Tn) is in A.

(2) If A is not closed under hyperjump and α = OnA then A has in it a nonstandard model of V = L whose ordinal standard part is α.

Theorem. Let α be any countable admissible ordinal greater than ω. Then there is a model of Σ1-separation whose height is α.

In [6], Metakides and Nerode introduced the study of the lattice of recursively enumerable substructures of a recursively presented model as a means to understand the recursive content of certain algebraic constructions. For example, the lattice of recursively enumerable subspaces, , of a recursively presented vector space V∞ has been studied by Kalantari, Metakides and Nerode, Retzlaff, Remmel and Shore. Similar studies have been done by Remmel [12], [13] for Boolean algebras and by Metakides and Nerode [9] for algebraically closed fields. In all of these models, the algebraic closure of a set is nontrivial. (The formal definition of the algebraic closure of a set S, denoted cl(S), is given in §1, however in vector spaces, cl(S) is just the subspace generated by S, in Boolean algebras, cl(S) is just the subalgebra generated by S, and in algebraically closed fields, cl(S) is just the algebraically closed subfield generated by S.)

In this paper, we give a general model theoretic setting (whose precise definition will be given in §1) in which we are able to give constructions which generalize many of the constructions of classical recursion theory. One of the main features of the models which we study is that the algebraic closure of set is just itself, i.e., cl(S) = S. Examples of such models include the natural numbers under equality 〈N, = 〉, the rational numbers under the usual ordering 〈Q, ≤〉, and a large class of n-dimensional partial orderings.

The relation ≪ (is a homomorphic image of) between (linear) order types has properties similar to those of the better known relation ≤ (is embeddable in). For example, the order type η of the rationals not only embeds every countable order type but also maps homomorphically onto . If is scattered, then can be embedded in (ω* + ω)α for some α < ω1. In that case, is also a homomorphic image of (ω* + ω)α [Lan 2]. If is uncountable, then for some uncountable ordinal α, α ≪, α* ≪, or η ≪. Proofs of these facts are much the same for ≤ and ≪.

The main theorem of [Lav 1] implies that the embedding relation better-quasiorders the set of countable order types. Our main theorem (§3) states the analogous result for the homomorphism relation. As a consequence, if 0, 1, … is an infinite sequence of countable order types, then there are i, j, i < j, such that i, is a homomorphic image of j. We observed in [Lan 1] that if this is true, then for each countable order type there is a sentence of Lω1ω such that if is a countable order type, then satisfies if and only if is a homomorphic image of . In fact, the motivation for the work leading to this paper came from this observation.

On the negative side, it is pointed out (§3) that our theorem cannot be extended as far as that of [Lav 1].

The stability of each of the theories of separably closed fields is proved, in the manner of Shelah's proof of the corresponding result for differentially closed fields. These are at present the only known stable but not superstable theories of fields. We indicate in §3 how each of the theories of separably closed fields can be associated with a model complete theory in the language of differential algebra. We assume familiarity with some basic facts about model completeness [4], stability [7], separably closed fields [2] or [3], and (for §3 only) differential fields [8].

Let G be a locally compact abelian group, Γ its dual group, and μ its Haar measure. For a function f: G → C, the Fourier transform of f is defined by

for every γ ∈ Γ.

We extend this definition for a function f on G, whose values are pairwise commutable normal operators in a Hilbert space. Then we study harmonic analysis for this extended Fourier transform.

Our method is Boolean valued analysis as introduced in [11] and [12]. Instead of developing the theory in a step-by-step manner, we shall develop a general machinery showing how to transform classical theorems to theorems in our situation.

In Chapter 1, we summarize the basic knowledge on Hilbert space, on Boolean valued model of set theory, and on Boolean valued analysis. In Chapter 2, we develop the theory of integration. Since we deal with unbounded operators as well as bounded operators, we need a new theory of integration. For a separable Hilbert space, the value of our integration coincides with the value of the usual integration with an adequate generalization for unbounded operators.

In Chapter 3, we establish machinery for our transfer principle and carry out the transformation of many classical theorems to theorems for our case.