This paper deals with Hilbert's substitution method for eliminating bound variables from first order proofs. With a first order system S framed in the ε-calculus [2] the problem is to associate a system S' without bound variables and an effective procedure for transforming derivations in S into derivations in S′. The transform of a formula A derived in S is to be an “ε-substitution instance” of A, i.e. it is obtained by replacing terms εxB(x) in A by terms of S′. In general the choice of these terms will depend on the particular derivation of A, and not on A alone. Cf. [4]. The present formulation sharpens Hilbert's original statement of the problem, i.e. that the transform of A should be finitistically verifiable, by making explicit the methods of verification used, namely those formalized in S′; on the other hand, it generalizes Hilbert's formulation since S′ need not be restricted to finitist systems.

The bound variable elimination procedure can always be taken to be primitive recursive in (the Gödel number of) the derivation of A. Constructions which transcend primitive recursion can simply be built into S′.

In this paper we show that if S′ is taken to be a second order system with constants for functionals, then the existence of suitable ε-substitution instances can be expressed by the solvability of certain functional equations in S′. We deal with two cases here. If S is number theory without induction, i.e. essentially predicate calculus with identity, then we can solve the equations in question by taking for S′ the free variable part S* of S with an added rule of definition of functionals by cases (recursive definition on finite ordinals), which is a conservative extension of S*.

A class of problems is called decidable if there is an algorithm which will give the answer to any problem of the class after a finite length of time. The purpose of this paper is to discuss the classes of problems that can be solved by infinitely long decision procedures in the following sense: An algorithm is given which, for any problem of the class, generates an infinitely long sequence of guesses. The problem will be said to be solved in the limit if, after some finite point in the sequence, all the guesses are correct and the same (in case there is more than one correct answer). Functions, sets, and functionals which are decidable by such infinite algorithms will be called limiting recursive. These, together with classes of objects which can be identified in the limit, are the subjects of this report.

Without qualification, set will mean set of numbers; function will mean number-theoretic function of 1 variable, possibly partial; functionals will take numerical values and have any number of numerical and/or function variables, the latter ranging solely over total functions of 1 variable. Thus a function is a special case of a functional, x will invariably stand for a numerical variable; φ for a function variable; g for a guess (a number); n for the numerical variable which indexes the guesses, referred to as the time.

Kleene [5] mentions two ways of extending the constructive ordinals. The first is by relativizing the set O of notations for the constructive ordinals, using fundamental sequences which are partial recursive in O. In this way we obtain the set OO which provides notations for the ordinals less than ω1O. Continuing the process, the sequence O, OO, , … and the corresponding ordinals are obtained. A second possibility is to define (constructive) higher number classes in which partial recursive functions are used at limit ordinals to provide an “accessibility” mapping from a previously defined number class. The relationship between the ordinals obtained by the two methods of extension has been an open problem. Methods developed in this article are used to show that the two ways of extending the constructive ordinals are equivalent, provided the sets of notations for the higher number classes satisfy certain natural conditions. Equivalence is obtained, not only with respect to ordinals, but also with respect to the forms of the sets of notations for the higher number classes. Specifically, the fundamental fact that the sets of notations for the constructive ordinals are complete Π11 sets generalizes to suitably defined higher number classes. As an application we prove that the ordinals of the Addison and Kleene [1] constructive third number class are exactly the ordinals less than ω1O and the set of notations for their third number class is recursively isomorphic to OO.

The purpose of this paper is to present two groups of results which have turned out to have a surprisingly close interconnection. The first two results (Theorems 1 and 2) were inspired by the following question: we know what sets are “decidable” — namely, the recursive sets (according to Church's Thesis). But what happens if we modify the notion of a decision procedure by (1) allowing the procedure to “change its mind” any finite number of times (in terms of Turing Machines: we visualize the machine as being given an integer (or an n-tuple of integers) as input. The machine then “prints out” a finite sequence of “yesses” and “nos”. The last “yes” or “no” is always to be the correct answer.); and (2) we give up the requirement that it be possible to tell (effectively) if the computation has terminated? I.e., if the machine has most recently printed “yes”, then we know that the integer put in as input must be in the set unless the machine is going to change its mind; but we have no procedure for telling whether the machine will change its mind or not.

The sets for which there exist decision procedures in this widened sense are decidable by “empirical” means — for, if we always “posit” that the most recently generated answer is correct, we will make a finite number of mistakes, but we will eventually get the correct answer. (Note, however, that even if we have gotten to the correct answer (the end of the finite sequence) we are never sure that we have the correct answer.)

Attention was directed to modal systems in which ‘necessarily α’ is interpreted as ‘α. is and always will be the case’ by Prior in his John Locke Lectures of 1956. The present paper shows that S4.3, the extension of S4 with

ALCLpLqLCLqLp,

is complete with respect to this interpretation when time is taken to be continuous, and that D, the extension of S4.3 with

ALNLpLCLCLCpLpLpLp,

is complete with respect to this interpretation when time is taken to be discrete. The method employed depends upon the application of an algebraic result of Garrett Birkhoff's to the models for these systems, in the sense of Tarski.

A considerable amount of work on S4.3 and D precedes this paper. The original model with discrete time is given in Prior's [7] (p. 23, but note the correction in [8]); that taking time to be continuous yields a weaker system is pointed out by him in [9]. S4.3 and D are studied in [3] of Dummett and Lemmon, where it is shown that D includes S4.3 and

CLCLCpLpLpCMLpLp.

While in Oxford in 1963, Kripke proved that these were in fact sufficient for D, using semantic tableaux. A decision procedure for S4.3, using Birkhoff's result, is given in my [2]. Dummett conjectured, in a conversation, that taking time to be continuous yielded S4.3. Thus the originality of this paper lies in giving a suitable completeness proof for S4.3, and in the unified algebraic treatment of the systems. It should be emphasised that the credit for first axiomatising D belongs to Kripke.

This paper is a sequel to our earlier paper, “Limit Ultrapowers”, [6]. In that paper we introduced the limit ultrapower construction and proved that is isomorphic to a limit ultrapower of if and only if every PCΔ class which contains also contains . In Section 1 of this paper we introduce the more general limit ultraproduct construction, and in Section 2 we prove that, for any class K of relational systems, a relational system is isomorphic to a limit ultraproduct of members of K if and only if every PCΔ class which includes K also contains . As a consequence, the property of K being an intersection of PCΔ classes is characterized purely set-theoretically by the property of K being closed under isomorphisms and limit ultraproducts.

In Section 3 we apply limit ultraproducts to obtain model-theoretic conditions equivalent to the set-theoretic condition that every α-complete ultrafilter is γ+-complete. The first result, Theorem 3.7, was announced in the abstract [8], and it is also closely related to a result which was stated without proof in [10], namely Theorem 2 of that paper.

In Sections 4 and 5 we apply our results in order to improve a theorem of Craig in [2]. Craig considered the logic L(Q), where Q is a set of cardinals, obtained from ordinary first order logic by adding for each α ϵ Q the quantifier “there exist at least α”.

I have argued in [1] that a concept bearing some resemblance to ‘p is the answer to d’ (p a proposition and d a question) can be defined wherever d has the form,

‘For which a's is it the case that A (a)?’ (Qa)A(a)

where a is a variable and A a wff containing a. To say that p is the true and complete answer to (Qa)A(a) is expressed as saying that p is logically equivalent to the true conjunction of A(a) or ~A(a) for each a. It is defined as;

Such a concept of answer is like Belnap's [2] direct true answer to a complete list question, or like Harrah's use [3] (p. 43) of the notion of a state description. The main difference between my approach and that of Belnap and Harrah is that while they are concerned to develop a formal metalanguage for discussion of questions and answers I am concerned to express, as far as possible in existing systems, certain interrogative statements; in particular statements of the form ‘— is the (an) answer to —’.

While the account in [1] does give a formal analysis of one ‘answer’ concept there are respects in which it is inadequate.

1. Since it uses entailment (or strict implication) to define the relation between p the answer and d the question we can shew that if p is the answer to d and q is logically equivalent to p then q is the answer to d.

From the work of Kleene, Post and Davis it is well-known that the arithmetic sets can be characterized as those sets recursive in ∅(n) for some natural number n, where ∅(0) = ∅ and . Actually the arithmetic sets which can be expressed in prenex form with n alternating quantifiers (applied to recursive predicates) are recursive in ∅(n). Hence, starting with ∅, the “jump operation”, which takes a set A into the set , serves to increase the “complexity” of sets in a uniform way.

As far as extending the ω-sequence of degrees of unsolvability (i.e. the degrees represented by the ∅(n)) into the 2nd number class, there is an immediate problem. One knows from Spector [17], corollary 2, p. 585, that there is no l.u.b. for the ω-sequence. So, at ω one must pick a degree in some other “natural” way. Unfortunately, what has seemed “natural” to some mathematicians has not seemed natural to others. Kleene and Davis (cf. [10] and [3] respectively) extended this arithmetic hierarchy of degrees of unsolvability by making use of natural number notations for a certain segment of ordinals of the 1st and 2nd number classes, the “constructive” ordinals. Using the Church-Kleene system S3, one can “sum up” previously obtained sets at the limit notations in a way that is certainly natural from a notational point of view.