One might fairly say that the very meaning of our subject has changed since Hilbert introduced it under the name Beweistheorie (it was meant to be the principal tool for formulating Hubert's general conception of how to analyze mathematical reasoning). Specifically, the roles of the two principal elements of proof theory, namely the intuitive proofs accepted and the formal proofs (or derivations) studied, have turned out to be quite different from what Hilbert thought. In his view the hard work had been done in the discovery of formalization, and what remained was the study of certain given formal systems.

With all seven of ‘∼’, ‘⊃’, ‘&’, ‘ν’, ‘≡’, ‘∀’, and ‘∃’ understood to serve as primitive signs, let an expression of the sort

A1, A2, … , An → B1, B2, … , Bm,

where A1, A2, …, Aη (η≥ 0), B1, B2, …, and Bm (m > 0 if n = 0, otherwise m ≥ 0) are wffs of the first-order quantificational calculus (QC), count as an L-sequent of QC; let an L-sequent of QC of the sort

A1, A2, … , An → B

count as an N-sequent of QC;2 and let an L-sequent S of QC count as a Gentzen L-sequent of QC if no individual variable of QC occurs both bound and free in S.

Why the Post-Kleene arithmetical hierarchy of degrees of (recursive) unsolvability was extended into the transfinite is not clear. Perhaps it was thought that if a hierarchy of sufficiently fine structure could be described that would include all sets of integers, some light might be thrown on the Continuum Hypothesis, and its truth or falsity possibly even ascertained. There is also some evidence in the 1955 papers of Kleene (cf. Kleene [2], [3], [4]) that it was once hoped that a theorem for the analytical hierarchy analogous to the result of Post and Kleene

In Kripke [8] the first-order intuitionjstic predicate calculus (without identity) is proved semantically complete with respect to a certain model theory, in the sense that every formula of this calculus is shown to be provable if and only if it is valid. Metatheorems of this sort are frequently called weak completeness theorems—the object of the present paper is to extend Kripke's result to obtain a strong completeness theorem for the intuitionistic predicate calculus of first order; i.e., we will show that a formula A of this calculus can be deduced from a set Γ of formulas if and only if Γ implies A. In notes 3 and 5, below, we will indicate how to account for identity, as well. Our proof of the completeness theorem employs techniques adapted from Henkin [6], and makes no use of semantic tableaux; this proof will also yield a Löwenheim-Skolem theorem for the modeling.

In [3], [4], and [5] Joyce Friedman formulated and investigated certain rules which constitute a semi-decision procedure for wffs of first order predicate calculus in closed prenex normal form with prefixes of the form ∀x1 … ∀xκ∃y1 … ∃ym∀z1 … ∀zn. Given such a wff QM, where Q is the prefix and M is the matrix in conjunctive normal form, Friedman's rules can be used, in effect, to construct a matrix M* which is obtained from M by deleting certain conjuncts of M.

Metarecursion theory is an analogue of recursion theory which deals with sets of recursive, or constructive, ordinals rather than of natural numbers. It was originated by Kreisel and Sacks [3], who make extensive use of an equation calculus developed by Kripke. We assume that the reader is acquainted with the outline of it given in [3], and especially in [3, §3].

Let E be a set of expressions representing real, single valued, partially defined functions of one real variable. E* will be the set of functions represented by expressions in E.

If A is an expression in E, A(x) is the function denoted by A.

It is assumed that E* contains the identity function and the rational numbers as constant functions and that E* is closed under addition, subtraction, multiplication and composition.

Interest has steadily increased among logicians and philosophers in versions of quantification theory which meet the following criteria: (1) no existence assumptions are made with respect to individual constants, and (2) theorems are valid in every domain including the empty domain. Logics meeting the former of these criteria are called free logics by Lambert and have been investigated in a series of papers by him and by van Fraassen, and by Leblanc and Thomason.1

Although it is natural to impose (2) in the presence of (1), the criteria are independent.2 Hence we baptize logics which meet both criteria universally free.

The eventual purpose of this paper is to provide certain specific representations of ordinals and develop their basic properties as needed for the proofs of the results announced in [3]. Since the choice of these representations is really intelligible only if the general principles involved are made explicit, we devote the first half of this paper (§§1 and 2) to such questions. The entire treatment is self-contained.

In [2] Prior puts forward a tense logic, GH1, which is intended to axiomatise tense logic with time linear and rational; he also contemplates the tense logic with time linear and real. The purpose of this paper is to give completeness proofs for three axiom systems, GH1, GHlr, GHli, with respect to tense logic with time linear and rational, real, and integral, respectively.1 In a fourth section I show that GH1 and GHlr have the finite model property, but that GHli lacks it.

GH1 has the operators of the classical propositional calculus, together with operators P, H, F, G for ‘It has been the case that’, ‘It has always been the case that’, ‘It will be the case that’, ‘It will always be the case that’, respectively.

Retraceable sets were denned in Dekker and Myhill [5]. In that paper it was pointed out that if A is a retraceable set, then A is recursive in each of its infinite subsets, i.e. A is introreducible. We would like to know to what extent theorems on retraceable sets also hold for introreducible sets; however, we have made very little progress in this direction. On the other hand, “uniformly introreducible” sets (which will be defined in §2) are more tractable, and it turns out that some results on retraceable sets extend to uniformly introreducible sets while others fail.

In intuitionistic mathematics one distinguishes between sets with a constructive character and sets in a more general sense. The first kind consists of spreads and the latter of species. The definition of a spread utilizes so-called choice sequences (in [5] infinitely proceeding sequence or ips), i.e., sequences of well-determined mathematical objects which are chosen more or less freely. One can restrict the choices by some law, which, however, need not be predetermined (changing one's mind is allowed).

The correspondence decision problem was first formulated and shown to be recursively unsolvable in Post (1946). The method of proof was to reduce the known unsolvable decision problem for the class of normal systems on a, b to the correspondence decision problem. In the present paper the concept of a standard Post normal system is used so as to obtain some equivalence reductions of combinatorial systems. In particular the following main result is obtained.

Remark 1. Finite sums and products of recursive equivalence types have been defined (see [1, p. 73 for sums and p. 130 for products]) and many of their algebraic properties revealed. It seems natural to ask if infinite sums and products can be defined in a natural manner and an algebra of such sums and products developed. The initial work in this direction is to be found in [2], [3] and [4]. In this paper we extend the above studies, concentrating for the most part on products.

In a paper that was written some time ago but appeared only recently [1], I indicated that Quine's system of quantification in [2], as well as his inclusive system of [3] can be modified so as to make it possible to prove *119 of [2] by another method than the one discovered by Berry. The reason originally given in [1, p. 136] for preferring the modified systems was wrong. (See [1, p. 158] for correction of previous remark.) But, at the cost of a slight complication of one of the axiom schemata, a considerable simplification of the proof of *119 is achieved in the modified systems, by dispensing with the use of *115 and *117 as intermediaries.

The purpose of this paper is to present a very versatile family of logical systems of positional or topological logic. These systems—obtained by generalizing the existing systems of chronological logic—are to have a very general nature, capable of reflecting the characteristics of a wide range of logical systems, including not only chronological (also temporal or tense) logic, but also what we may call locative or place logic, and even a logic of “possible worlds”.