The usual formulations of combinatory logic, as in Church [1] or Curry and Feys [2], have no straightforward semantics. This lack complicates the proofs of basic metasystematic results, prevents the perspicuous formalization of combinatory logic as a deductive theory, and makes the combinators unnecessarily difficult to apply to recursion theory or to the foundations of mathematics. In the present paper we shall give a new formulation of combinatory logic, thought of as an abstract theory of rules. At each stage in the development we shall give a precise semantic interpretation for our axioms. We begin with an abstract treatment of the syntax and semantics of a theory of rules. We then specialize to the theory of the combinators and prove a completeness theorem connecting our axioms with our semantics. On this basis we treat functional abstraction, truth-functions, and the representation of partial recursive functions. In the spirit of Church [1, pp. 62–71], we conclude by extending our methods to the treatment of intensional identity.

The theories developed here are part of a simplification of the theory of constructions described in [3]. Their semantics are motivated by the intended interpretation of the theory of constructions. The present paper is selfcontained and can be read without any familiarity with the theory of constructions, although the motivation of several of the notions considered here is given in [3]. In a future publication we will use the results of the present paper as the basis for a detailed study of a simplified form of the theory in [3].

We prove here theorems of the form: if T has a model M in which P1(M) is κ1-like ordered, P2(M) is κ2-like ordered …, and Q1(M) is of power λ1, …, then T has a model N in which P1(M) is κ1′-like ordered …, Q1(N) is of power λ1′, …. (In this article κ is a strong-limit singular cardinal, and κ′ is a singular cardinal.)

We also sometimes add the condition that M, N omits some types. The results are seemingly the best possible, i.e. according to our knowledge about n-cardinal problems (or, more precisely, a certain variant of them).

Let N be the set of natural numbers. If A ⊆ N, let [A]n denote the class of all n-element subsets of A. If P is a partition of [N]n into finitely many classes C1, …, Cp, let H(P) denote the class of those infinite sets A ⊆ N such that [A]n ⊆ Ci for some i. Ramsey's theorem [8, Theorem A] asserts that H(P) is nonempty for any such partition P. Our purpose here is to study what can be said about H(P) when P is recursive, i.e. each Ci, is recursive under a suitable coding of [N]n. We show that if P is such a recursive partition of [N]n, then H(P) contains a set which is Πn0 in the arithmetical hierarchy. In the other direction we prove that for each n ≥ 2 there is a recursive partition P of [N]n into two classes such that H(P) contains no Σn0 set. These results answer a question raised by Specker [12].

A basic partition is a partition of [N]2 into two classes. In §§2, 3, and 4 we concentrate on basic partitions and in so doing prepare the way for the general results mentioned above. These are proved in §5. Our “positive” results are obtained by effectivizing proofs of Ramsey's theorem which differ from the original proof in [8]. We present these proofs (of which one is a generalization of the other) in §§4 and 5 in order to clarify the motivation of the effective versions.

It is well known that iteration of any number-theoretic function f, which grows at least exponentially, produces a new function f′ such that f is elementary-recursive in f′ (in the Csillag-Kalmar sense), but not conversely (since f′ majorizes every function elementary-recursive in f). This device was first used by Grzegorczyk [3] in the construction of a properly expanding hierarchy {ℰn: n = 0, 1, 2, …} which provided a classification of the primitive recursive functions. More recently it was shown in [7] how, by iterating at successor stages and diagonalizing over fundamental sequences at limit stages, the Grzegorczyk hierarchy can be extended through Cantor's second number-class. A problem which immediately arises is that of classifying all recursive functions, and an answer to this problem is to be found in the general results of Feferman [1]. These results show that although hierarchies of various types (including the above extensions of Grzegorczyk's hierarchy) can be produced, which range over initial segments of the constructive ordinals and which do provide complete classifications of the recursive functions, these cannot be regarded as classifications “from below”, since the method of assigning fundamental sequences at limit stages must be highly noneffective. We therefore adopt the more modest aim here (as in [7], [12], [14]) of characterising certain well-known (effectively generated) subclasses of the recursive functions, by means of hierarchies generated in a natural manner, “from below”.

One of the major problems of model theory is the spectrum problem, i.e. the development of structure theorems for the spectrum of models of a given theory. I hope that this paper will make a (small) contribution to the solution of this problem.

Broadly speaking, in this paper we take a fixed (but arbitrary) theory T and consider a particular class ℰ of models of T. The structures in ℰ (which are known as existentially closed structures) are connected with the model complete extensions of T. These structures have already appeared several times in the literature.

In §1 we survey the notation and terminology that we use, as well as the well known facts that we require. We also consider several concepts which are not new here but which may not be well known.

In §2 we define, and give the basic results concerning existentially closed structures. For most theories, T, the class ℰ is not elementary and hence is not directly amenable to a model theoretic study. Because of this we consider a smaller class of structures—the uniformly existentially closed structures. These are discussed in §3.

In §4 we look at model complete theories via existentially closed structures. This section is essentially a refinement of parts of [6].

In §5 we look at model companions of theories via existentially closed structures.

Finally, in §6 we make some remarks on the relevance of existentially closed structures to the spectrum problem.

This note is an addendum to an incompleteness result of Feferman and Spector [1]: for any such progression satisfying the (natural) conditions listed in [1] there is a true Π10-formula which cannot be derived in the progression. The idea of their proof yields a stronger result.

If each numerical instance A[x/n] of the formula A (with the free numerical variable x) is decided in a recursive progression along a Π11-path then the set {n: ⊦ A[x/n]} is recursive.

In other words, only recursively solvable problems are decidable in such progressions. This yields the incompleteness result of [1] when specialized to some Π10 formula A which defines a nonrecursive set, since then some instance A[x/n] must be undecided and A[x/n] is a closed Π10 formula. The stronger result is needed to extend Church's thesis for total functions reckonable in formal systems to (total) functions reckonable in recursive progressions on Π11-paths. A partially reckonable function always has a Π11 graph (and if its graph is Δ11 then it is by C. Jockusch, r.e.; so some Π11 sets are not partially reckonable). The relevance of these facts for the model of mathematical reasoning provided by (variants of) Turing's ordinal logics is analyzed in (b) (ii) of Part II, which goes into our current knowledge about Church's thesis.

We study the relations between abelian groups B and C that every universal (resp. universal-existential) sentence true in B is also true in C, and give algebraic criteria for these relations to hold. As a consequence we characterize the inductive complete theories of abelian groups and prove that they are exactly the model-complete theories.

Chang [1], [2] has proved the following generalization of the Craig interpolation theorem [3]: For any first-order formulas φ and ψ with free first- and second-order variables among ν1, …, νn, R and ν1, …, νn, S respectively, and for any sequence Q1, …, Qn of quantifiers such that Q1 is universal whenever ν1 is a second-order variable, if

then there is a first-order formula θ with free variables among ν1, …, νn such that

(Note that the Craig interpolation theorem is the special case of Chang's theorem in which Q1, …, Qn are all universal quantifiers.) Chang also raised the question [2, Remark (k)] as to whether the Lopez-Escobar interpolation theorem [6] for the infinitary language Lω1ω possesses a similar generalization. In this paper, we show that the answer to Chang's question is affirmative and, moreover, that several interpolation theorems for applied second-order languages for number theory also possess such generalizations.

Maehara and Takeuti [7] have established independently proof-theoretic interpolation theorems for first-order logic and Lω1ω which have as corollaries both Chang's theorem and its analog for Lω1ω. Our proofs are quite different from theirs and rely on model-theoretic techniques stemming from the analogy between the theory of definability in Lω1ω and the theory of Borel and analytic sets of real numbers, rather than the technique of cut-elimination.

It is well known that in prepositional logic not every propositional connective is definable in terms of equivalence nor indeed in terms of equivalence together with negation. It is the purpose of this note to show that in a certain sense this is, however, possible within predicate logic.

Let F1 be the class of predicate logical formulae containing only the logical connectives ¬ (not), ∨ (or), E (exists), and F2 the class of predicate logical formulae containing only the logical connectives ≡ (if and only if) and E.

Our object will be to find a method for reducing any formulae ϕ of F1 to a formula ψ of F2 such that ϕ is valid if and only if ψ is valid.

Note first that for every domain D containing at least two individuals we can for every n-place relation R defined over D find an n + 1-place relation S defined over D such that for all x1, …, xn ∈ D,

holds. For instance, let S(y, x1, …, xn) be the relation y = x1 & R(x1, …, xn).

Now let ϕ be an arbitrary formula of F1 and A1, …, A3 a complete list of predicate letters occurring in ϕ of degree g1, …, gi, respectively. Let ϕ′ be the formula obtained from ϕ by replacing every prime formula Ai(x1, …, xgi) by

Then it follows immediately from the previous observation that (a) ϕ is satisfiable in D if and only if ϕ′ is satisfiable in D.

As Gödel [6] has pointed out, there is a certain interchangeability between the intuitionistic notion of proof and the notion of constructive functional of finite type. He achieves this interchange in the direction from logic to functionals by his functional interpretation of Heyting arithmetic H in a free variable theory T of primitive recursive functionals of finite type. In the present paper we shall extend Gödel's functional interpretation to the case in which H and T are extended by adding an abstract notion of constructive ordinal. In other words, we obtain the Gödel functional interpretation of an intuitionistic theory U of numbers (i.e., nonnegative integers) and constructive ordinals in a free variable theory V of finite type over both numbers and constructive ordinals. This allows us to obtain an analysis of noniterated positive inductive definitions [8].

The notion of constructive ordinal to be treated is as follows. There is given a function J which embeds the nonnegative integers in the constructive ordinals. A constructive ordinal of the form Jn is said to be minimal. There is also given a function δ which associates to each constructive ordinal Z and number n a constructive ordinal δZn which we denote by Zn. When Z is nonminimal, each Zn is called an immediate predecessor of Z. The basic principle for forming constructive ordinals says: for every function f from numbers n to constructive ordinals, there exists a constructive ordinal Z such that Zn = fn for all n. The principle of transfinite induction with respect to constructive ordinals says: if a property Q(Z) of constructive ordinals Z holds for minimal Z, and if ∀nQ(Zn) → Q(Z) holds for all Z, then Q(Z) holds for all Z.

Let Δ be a set of axioms of a theory Tc(Δ) of classical predicate calculus (CPC); Δ may also be considered as a set of axioms of a theory TH(Δ) of Heyting's predicate calculus (HPC). Our aim is to investigate the decision problem of TH(Δ) in HPC for various known theories Δ of CPC.

Theorem I(a) of §1 states that if Δ is a finitely axiomatizable and undecidable theory of CPC then TH(Δ) is undecidable in HPC. Furthermore, the relations between theorems of HPC are more complicated and so two CPC-equivalent axiomatizations of the same theory may give rise to two different HPC theories, in fact, one decidable and the other not.

Semantically, the Kripke models (for which HPC is complete) are partially ordered families of classical models. Thus a formula expresses a property of a family of classical models (i.e. of a Kripke model). A theory Θ expresses a set of such properties. It may happen that a class of Kripke models defined by a set of formulas Θ is also definable in CPC (in a possibly richer language) by a CPC-theory Θ′! This establishes a connection between the decision problem of Θ in HPC and that of Θ′ in CPC. In particular if Θ′ is undecidable, so is Θ. Theorems II and III of §1 give sufficient conditions on Θ to be such that the corresponding Θ′ is undecidable. Θ′ is shown undecidable by interpreting the CPC theory of a reflexive and symmetric relation in Θ′.

In [4] Alonzo Church introduced an elegant and expressive formulation of type theory with λ-conversion. In [8] Henkin introduced the concept of a general model for this system, such that a sentence A is a theorem if and only if it is true in all general models. The crucial clause in Henkin's definition of a general model ℳ is that for each assignment φ of values in ℳ to variables and for each wff A, there must be an appropriate value of A in ℳ. Hintikka points out in [10, p. 3] that this constitutes a rather strong requirement concerning the structure of a general model. Henkin draws attention to the problem of constructing nonstandard models for the theory of types in [9, p. 324].

We shall use a simple idea of combinatory logic to find a characterization of general models which does not directly refer to wffs, and which is easier to work with in certain contexts. This characterization can be applied, with appropriate minor and obvious modifications, to a variety of formulations of type theory with λ-conversion. We shall be concerned with a language ℒ with extensionality in which there is no description or selection operator, and in which (for convenience) the sole primitive logical constants are the equality symbols Qoαα for each type α.

It is well known that equality is definable in type theory. Thus, in the language of [2], the equality relation between elements of type α is definable as , i.e., xα = yα iff every set which contains xα also contains yα. However, in a nonstandard model of type theory, the sets may be so sparse that the wff above does not denote the true equality relation. We shall use this observation to construct a general model in the sense of [2] in which the Axiom of Extensionality is not valid. Thus Theorem 2 of [2] is technically incorrect. However, it is easy to remedy the situation by slightly modifying the definition of general model.

Our construction will show that the Axiom Schema of Extensionality is independent even if one takes as an axiom schema.

We shall assume familiarity with, and use the notation of, [2] and §§2–3 of [1].