This expository paper contains a list of 102 problems which, at the time of publication, are unsolved. These problems are distributed in four subdivisions of logic: model theory, proof theory and intuitionism, recursion theory, and set theory. They are written in the form of statements which we believe to be at least as likely as their negations. These should not be viewed as conjectures since, in some cases, we had no opinion as to which way the problem would go.

In each case where we believe a problem did not originate with us, we made an effort to pinpoint a source. Often this was a difficult matter, based on subjective judgments. When we were unable to pinpoint a source, we left a question mark. No inference should be drawn concerning the beliefs of the originator of a problem as to which way it will go (lest the originator be us).

The choice of these problems was based on five criteria. Firstly, we are only including problems which call for the truth value of a particular mathematical statement. A second criterion is the extent to which the concepts involved in the statements are concepts that are well known, well denned, and well understood, as well as having been extensively considered in the literature. A third criterion is the extent to which these problems have natural, simple and attractive formulations. A fourth criterion is the extent to which there is evidence that a real difficulty exists in finding a solution. Lastly and unavoidably, the extent to which these problems are connected with the author's research interests in mathematical logic.

Whenever particular ordinals are used as tools in a proof or a definition, it is necessary to find a way of representing them. If the ordinals are sufficiently small, there is a standard way (e.g. Cantor normal forms for ordinals less than ε0); in general, representations are often found by using functions on initial segments of the ordinals: Each term which can be obtained from by applications of a function symbol is regarded as a notation for the ordinal obtained by the same applications of the function f to the ordinal 0. In this way, f provides representations for all the ordinals in Clf(0), the closure set of f (se e §1). (For an introduction to and development of this principle, see Feferman [F1]; and for a discussion of the significance of such representations in proof theory, see Kreisel [K1, pp. 22–34].) Thus it is natural to ask whether there are connections between frequently encountered properties of ordinal functions and the size of the ordinals for which they can provide representations.

The purpose of this paper is to show that, for any integer n, the ordinal (see §2) is a bound for the closure ordinals of replete monotonic increasing n-place functions. This result is optimal for n > 2 (the bound is attained by where θα = 1 + α) but not for n < 2. D. H. de Jongh has recently proved, using a completely different method, that the (least possible) bound for n = 2 is ε0. (Trivially, that for n = 1 is φ.)

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.

Partial degrees are equivalence classes of partial natural number functions under some suitable extension of relative recursiveness to partial functions. The usual definitions of relative recursiveness, equivalent in the context of total functions, are distinct when extended to partial functions. The purpose of this paper is to compare the upper semilattice structures of the resulting degrees.

Relative partial recursiveness of partial functions was first introduced in Kleene [2] as an extension of the definition by means of systems of equations of relative recursiveness of total functions. Kleene's relative partial recursiveness is equivalent to the relation between the graphs of partial functions induced by Rogers' [10] relation of relative enumerability (called enumeration reducibility) between sets. The resulting degrees are hence called enumeration degrees. In [2] Davis introduces completely computable or compact functionals of partial functions and uses these to define relative partial recursiveness of partial functions. Davis' functionals are equivalent to the recursive operators introduced in Rogers [10] where a theorem of Myhill and Shepherdson is used to show that the resulting reducibility, here called weak Turing reducibility, is stronger than (i.e., implies, but is not implied by) enumeration reducibility. As in Davis [2], relative recursiveness of total functions with range ⊆{0, 1} may be defined by means of Turing machines with oracles or equivalently as the closure of initial functions under composition, primitive re-cursion, and minimalization (i.e., relative μ-recursiveness). Extending either of these definitions yields a relation between partial functions, here called Turing reducibility, which is stronger still.

In [4] it is shown that if the structure omits a type Σ, and Σ is complete with respect to Th(), then there is a proper elementary extension of which omits Σ. This result is extended in the present paper. It is shown that Th() has models omitting Σ in all infinite powers.

A type is a countable set of formulas with just the variable ν occurring free. A structure is said to omit the type Σ if no element of satisfies all of the formulas of Σ. A type Σ, in the same language as a theory T, is said to be complete with respect to T if (1) T ∪ Σ is consistent, and (2) for every formula φ(ν) of the language of T (with just ν free), either φ or ¬φ is in Σ.

The proof of the result of this paper resembles Morley's proof [5] that the Hanf number for omitting types is . It is shown that there is a model of Th() which omits Σ and contains an infinite set of indiscernibles. Where Morley used the Erdös-Rado generalization of Ramsey's theorem, a definable version of the ordinary Ramsey's theorem is used here.

The “omitting types” version of the ω-completeness theorem ([1], [3], [6]) is used, as it was in Morley's proof and in [4]. In [4], satisfaction of the hypotheses of the ω-completeness theorem followed from the fact that, in , any infinite, definable set can be split into two infinite, definable sets.

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.

In this paper we present two theorems concerning relationships between degrees of unsolvability of recursively enumerable sets and their complexity properties.

The first theorem asserts that there are nonspeedable recursively enumerable sets in every recursively enumerable Turing degree. This theorem disproves the conjecture that all Turing complete sets are speedable, which arose from the fact that a rather inclusive subclass of the Turing complete sets, namely, the subcreative sets, consists solely of effectively speedable sets [2]. Furthermore, the natural construction to produce a nonspeedable set seems to lower the degree of the resulting set.

The second theorem says that every speedable set has jump strictly above the jump of the recursive sets. This theorem is an expected one in view of the fact that all sets which are known to be speedable jump to the double jump of the recursive sets [4].

After this paper was written, R. Soare [8] found a very useful characterization of the speedable sets which greatly facilitated the proofs of the results presented here. In addition his characterization implies that an r.e. degree a contains a speed-able set iff a′ > 0′.

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.

Several canonical partition theorems are obtained, including a simultaneous generalization of Neumer's lemma and the Erdös-Rado theorem. The canonical partition relation for infinite cardinals is completely determined, answering a question of Erdös and Rado. Counterexamples are given showing that in several ways these results cannot be improved.

The primary purpose of this work is to analyze the constructive interpretations of classical theorems concerning the continuity of effective operations. These theorems are the “recursivizations” of the statements that all functions (on various spaces) are continuous. To discuss the question whether these statements are constructively valid, it would be necessary to analyze the notion of “constructively valid,” which is beyond the scope of this paper. We now proceed to describe our results. We deal with two kinds of effective operations: (i) partial operations on indices of partial functions, and (ii) total operations on indices of total functions. The two principal theorems of the subject assert that each such operation is continuous; for (i) this is due to Myhill-Shepherdson [7] and called MS here; for (ii) it is due to Kreisel, Lacombe, and Shoenfield [5] and called KLS. (Explicit formulations of these and other principles mentioned in the introduction will be given in §1 below.)

Several interpretations (of, e.g., Heyting's arithmetic HA) in the literature satisfy Markov's principle MP, and for these MS and KLS are valid, since a close inspection of the classical proofs of MS and KLS shows that they are derivable in HA + MP. But we also find an interpretation in the literature under which MS and KLS are valid while MP is not (hence MS and KLS do not imply MP in systems for which this interpretation is sound). This work is in §2.

We present two finitely axiomatized modal propositional logics, one between T and S4 and the other an extension of S4, which are incomplete with respect to the neighbourhood or Scott-Montague semantics.

Throughout this paper we are referring to logics which contain all the classical connectives and only one modal connective □ (unary), no propositional constants, all classical tautologies, and which are closed under the rules of modus ponens (MP), substitution, and the rule RE (from A ↔ B infer αA ↔ □B). Such logics are called classical by Segerberg [6]. Classical logics which contain the formula □p ∧ □q → □(p ∧ q) (denoted by K) and its “converse,” □{p ∧ q)→ □p ∧ □q (denoted by R) are called regular; regular logics which are closed under the rule of necessitation, RN (from A infer □A), are called normal. The logics that we are particularly concerned with are all normal, although some of our results will be true for all regular or all classical logics. It is well known that K and R and closure under RN imply closure under RE and also that normal logics are also those logics closed under RN and containing □{p → q) → {□p → □q).

This paper is the third in a series collectively entitled Formal systems of intuitionistic analysis. The first two are [4] and [5] in the bibliography; in them I attempted to codify Brouwer's mathematical practice. In the present paper, which is independent of [4] and [5], I shall do the same for Bishop's book [1]. There is a widespread current impression, due partly to Bishop himself (see [2]) and partly to Goodman and the author (see [3]) that the theory of Gödel functionals, with quantifiers and choice, is the appropriate formalism for [1]. That this is not so is seen as soon as one really tries to formalize the mathematics of [1] in detail. Even so simple a matter as the definition of the partial function 1/x on the nonzero reals is quite a headache, unless one is prepared either to distinguish nonzero reals from reals (a nonzero real being a pair consisting of a real x and an integer n with ∣x∣ > 1/n) or, to take the Dialectica interpretation seriously, by adjoining to the Gödel system an axiom saying that every formula is equivalent to its Dialectica interpretation. (See [1, p. 19], [2, pp. 57–60] respectively for these two methods.) In more advanced mathematics the complexities become intolerable.

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 this note we define a class of properties for which the following holds: If we can prove in NF that the property holds for the universe V, then we can prove in NF that it holds for every set equipollent to its power set.

Definition. For any stratified formula A and any variable υ which does not occur in A, let Aυ be the formula obtained by replacing in A each quantifier (Qx) by the bounded quantifier (Qx ∈ SCi(υ)), where i is the type of x in A. We will say that a property P(υ) is typed when there is a stratified sentence S such that P(υ) ↔ Sυ holds in NF.

Examples of typed properties are: “υ is Dedekind-infinite”, “υ is not well-orderable”. Specker [3] proved that these typed properties hold for the universe V, and C. Ward Henson [1] extended this result to any set equipollent to its power set. We will show that such an extension holds for any typed property.

Theorem. For any typed property P(υ):

Proof. Fix a bijective map h: υ → SC(υ) and define for i = 0, 1, 2, …, n, … a bijective map hi: υ → SCi(υ) as follows:

For every formula A, let A(h) be obtained by replacing in A each atomic part (x ∈ y) by (x ∈ h(y)) and each quantifier (Qx) by (Qx ∈ υ).

Much recent work in the theory of computational complexity ([Me], [FR]. [SI]) is concerned with establishing “the complexity” of various recursive functions, as measured by the time or space requirements of Turing machines which compute them. In the above work, we also observe another phenomenon: knowing the values of certain functions makes certain other functions easier to compute than they would be without this knowledge. We could say that the auxiliary functions “help” the computation of the other functions.

For example, we may conjecture that the “polynomial-complete” problems of Cook [C] and Karp [K] and Stockmeyer [S2], such as satisfiability of propositional formulas or 3-colorability of planar graphs, in fact require time proportional to nlog2n to be computed on a deterministic Turing machine. Then since the time required to decide if a planar graph with n nodes is 3-colorable can be lowered to a polynomial in n if we have a precomputed table of the satisfiable formulas in the propositional calculus, it is natural to say that the satisfiability problem “helps” the computation of the answers to the 3-coloring problem. Similar remarks may be made for any pair of polynomial-complete problems.

As a further illustration, Meyer and Stockmeyer [MS] have shown that, for a certain alphabet Σ, recognition of the set of regular expressions with squaring which are equivalent to Σ* requires Turing machine space cn for some constant c, on an infinite set of arguments. We also know that this set of regular expressions, which we call RSQ, may actually be recognized in space dn for some other constant d. Theorem 6.2 in [LMF] implies that there is some problem (not necessarily an interesting one) of complexity approximately equal to that of RSQ, which does not reduce the complexity of RSQ below cn. It does not “help” the computation of RSQ.

Our results concern the natural models of Ackermann-type set theories, but they can also be viewed as results about the definability of ordinals in certain sets.

Ackermann's set theory A was introduced in [1] and it is now formulated in the first order predicate calculus with identity, using ∈ for membership and an individual constant V for the class of all sets. We use the letters ϕ, χ, θ, and χ to stand for formulae which do not contain V and capital Greek letters to stand for any formulae. Then, the axioms of A* are the universal closures of

where all the free variables are shown in A4 and z does not occur in the Θ of A2. A is the theory A* − A5.

Most of our notation is standard (for instance, α, β, γ, δ, κ, λ, ξ are variables ranging over ordinals) and, in general, we follow the notation of [7]. When x ⊆ Rα, we use Df(Rα, x) for the set of those elements of Rα which are definable in 〈Rα, ∈〉, using a first order ∈-formula and parameters from x.

We refer the reader to [7] for an outline of the results which are known about A, but we shall summarise those facts which are frequently used in this paper.

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 [3] we have associated to a structure an ordinal which gives us information about elementary substructures of the structure. For example a structure whose ascending chain number (as we call the ordinal) is ω could be called Noetherian since all ascending elementary chains inside it are finite (and there are arbitrarily large finite chains). Theorem 2 shows that such structures exist. In fact we prove that for any α < ω1 there is a structure whose ascending chain number is α. The construction is based on the existence of a certain group of permutations of ω (see Theorem 1). The second part of this paper deals with the relevance of the chain number to the study of Jonsson algebras.

Let L be a first order logic and the infinitary logic (as described in [K, p. 6] over L. Suslin logic is obtained from by adjoining new propositional operators and . Let f range over elements of ωω and n range over elements of ω. Seq is the set of all finite sequences of elements of ω. If θ: Seq → is a mapping into formulas of then and are formulas of LA. If is a structure in which we can interpret and h is an -assignment then we extend the notion of satisfaction from to by defining

where f ∣ n is the finite sequence consisting of the first n values of f. We assume that has ω symbols for relations, functions, constants, and ω1 variables. θ is valid if θ ⊧ [h] for every h and is valid if -valid for every . We address ourselves to the problem of finding syntactical rules (or nearly so) which characterize validity .