This paper is divided into two parts. Part I provides a resumé of the evolution of the notion of predicativity. Part II describes our own work on the subject.

Part I

§1. Conceptions of sets. Statements about sets lie at the heart of most modern attempts to systematize all (or, at least, all known) mathematics. Technical and philosophical discussions concerning such systematizations and the underlying conceptions have thus occupied a considerable portion of the literature on the foundations of mathematics.

It is well-known that a Boolean algebra (B, +, ., ‐) may be defined as an algebraic system with at least two elements such that (for all x, y, z ε B):

These axioms or equations are not independent, in the sense that some of them are logical consequences of the others. B. A. Bernstein [1] thought that the first three and their duals form an independent dual-symmetric definition of a Boolean algebra, but R. Montague and J. Tarski [3] proved later that B1 (or B̅1) follows from B2, B3, B̅1, B̅2, B̅3 (from B1, B2, B3, B̅2, B̅3).

In a previous paper [1] Chang and the present author presented a system of infinite valued predicate logic, the truth values being the closed interval [0, 1] of real numbers. That paper was the result of an investigation attempting to establish the completeness of the system using the real number 1 as the sole designated value. In fact, we fell short of our mark and proved a weakened form of completeness utilizing positive segments, [0, a], of linearly ordered abelian groups as admissible truth values. A result of Scarpellini [8], however, showing that the set of well-formed formulas of infinite valued logic valid (with respect to the sole designated real number 1) is not recursively enumerable indicates the above mentioned result is the best possible.

We consider the results of adding to a basic modal system T0 the axioms G1. CLpp; Pn. CLnpLn+1p; Bn. CpLnMp, where n ≧ 11, in all combinations. The method of Meredith's [7] will be extended to get models of these systems in lower predicate calculus (LPC) with a constant binary relation, U. Most of the results were already obtained in [1]–[6], though systems as in (i) and (ii) below were not investigated, except that S40 in (ii) was mentioned in [1]. However some repetition may be excused in view of the simplicity with which the results are obtained by the present method.

Let LIC be the implicational fragment of Dummett's LC, axiomatised by Bull in [1] by adding the axiom (L) CCCpqrCCCqprr to positive implication. The system which Bull in [2] calls OIC, i.e. positive implication plus (0) CCCCpqqrCCCpqrr, is contained in LIC (it is thesis 34 in [1], p. 193); but it does not contain it, as the following matrix (due to Bull)

verifies OIC but not (L) (CCC342CCC4322 = 2). Nor is (L) deducible in OIC supplemented by intuitionist axioms for negation, since the latter are all verified by the above matrix with Cp5 for Np.

There are essentially two ‘positive’ results concerning the extension of effective operations to partial recursive functionals. The first proved by Myhill and Shepherdson in [9] states that any effective operation whose domain is the set of all partial recursive (p.r.) functions is potentially p.r. The second proved originally by Kreisel, Lacombe, and Shoenfield in [5] states: Let F be an effective operation mapping a set of recursive functions into the natural numbers; if has a recursively dense base, then F is potentially p.r. The main objective of this paper is to present these two theorems in a general setting.

It is well known that if a postulate LLCpp or a rule of procedure ├α→├Lα (from a thesis α of a considered system to infer a thesis Lα of that system) is added to Lewis's modal system S3, we get his system S4 (see [7], p. 148). It is also known that the addition of this rule to S2 and SI has the effect of converting these systems into the Gödel-Feys-von Wright system T (M). My purpose in this paper is first to draw attention to some other ways of converting S3 and S2 into S4 and T respectively, as well as to extend a theorem of Halldén on S3, S4 and S7 to S2, T and S6. The results reached will also apply to the systems S3.5, S5 and S7.5, where S3.5 and S7.5 are obtained, respectively, from S3 and S7 by the addition of the postulate CNLpLNLp; an answer will be given to the question of irreducible modalities in S3.5. Moreover, two results will be proved that bear on the problem whether the systems S2 and T can be axiomatized by means of a finite number of axiom schemata and material detachment as the only primitive rule of inference.

In this note we point out a limitation of the treatment of transfinite recursion in Quine's Set Theory and its Logic2 and develop a method for overcoming it. We shall also mention and indicate how to overcome a second more trivial limitation. We assume familiarity with Set Theory and its Logic and use its notation and terminology. Numbered references are to Quine's numbered formulae. In our work we continue the numbering of § 26.

The first difficulty is that the theorems which show that his device for defining functions by transfinite recursion (§ 25) accomplishes its purpose do not apply to functions defined by recursion over all the ordinals. Let γ be the function which gives the value of the function we want for an ordinal y from the sequence of its values for ordinals less than y.

I shall refer to the implicational fragment of intuitionist logic, and its extension with the further axiom

CCCCpqqrCCCpqrr

as IIC and OIC, respectively. The purpose of this paper is to apply a result due to Garrett Birkhoff to the extensions of IIC, and to the extensions of OIC in particular. The main result obtained is that every extension of OIC is characterised by finite models.

In the original example of a transfinite hierarchy of degrees of unsolvability, a predicate Ha is associated with each a in the set 0 of ordinal notations. (See Kleene [K1], Spector [S1], and the references there to Davis and Mostowski.) The predicates are defined by means of induction over the partial well-ordering relation ≤0 on the set 0 of notations for the recursive ordinals. The usefulness of this hierarchy of predicates is enhanced by Spector's proof [S1] of the “uniqueness” property: viz. that the degree of Ha depends only on the ordinal |a| for which a is a notation.

This is really a note to Wajsberg's [4].

In [3] J. C. C. McKinsey proved the following two completeness theorems: (1) theorem 6: If A is a wff of S2 with just r (proper or improper) sub-wffs, then A is provable in S2 iff A is satisfied by every normal S2-matrix with no more than 22r+1 elements; (2) theorem 13: if A is a wff of S4 with just r sub-wffs, then A is provable in S4 iff A is satisfied by every normal S4-matrix with no more than 22r elements. Now, a similar theorem has not been explicitly formulated for S5, even though a similar, even simpler, theorem has been almost at hand since Wajsberg's [4] was published in 1933, namely:

Theorem. If A is a wff of S5 with just n propositional variables, then A is provable in S5 iff A is satisfied by a normal SS-matrix with 22n elements.