In this paper we continue the study of inner models of the type studied in Inner models for set theory—Part I. The present paper is concerned exclusively with a particular kind of model, the ‘super-complete models’ defined in section 2.4 of I (page 186). The condition (c) of 2.4 and the completeness condition 1.42 imply that such a model is uniquely determined when its universal class Vm is given. Writing condition (c) and the completeness conditions 1.41, 1.42 in terms of Vm , we may state the definition in the form:

3.1. Dfn. A class Vm is said to determine a super-complete model if the model whose basic notions are defined by, satisfies axioms A, B, C.

N. B. This definition is not necessarily metamathematical in nature. If desired, it could be written out quite formally as the definition of a notion ‘SCM(U)’ (‘U determines a super-complete model’) thus:

where ψ(U) is the propositional function expressing in terms of U the fact that the model determined by U according to 3.1 satisfies the relativization of axioms A, B, C. E.g. corresponding to axiom A1m , i.e., , ψ(U) contains the equivalent term . All the relativized axioms can be similarly expressed in this way by first writing out the relativized form (after having replaced all defined symbols which occur by the corresponding formulae in primitive notation) and then replacing ‘(A m )ϕ(A m ) by which is in turn replaced by , and similarly replacing ‘(xm )ϕ(xm )’ by ‘(x m )ϕ(x m )’ by ‘(X)(X ϵ U ▪ ⊃ ▪ ϕ (X)), and Thus ψ(U) is obtained in primitive notation.

We use NF to designate the system known as Quine's New Foundations (see [1] and [2]), and NF + AF to designate the same system with a suitable axiom of infinity adjoined. We use ML to designate the revised system appearing in the third printing of Quine's “Mathematical Logic” (see [3]). This system ML is just the system P proposed by Wang in [4], and essentially includes NF as a part.

The pripcipal results of the present paper are:

A. In NF the axiom of infinity is equivalent to the definability of an ordered pair having the same type as its constituents.

B. Considering the formulas of NF as having translations in the formalism of ML in the sense defined in [4], we find that a formula of NF is provable in NF if and only if its translation is provable in ML. From the fact that the axiom of infinity is provable in ML, one might be tempted to conclude that the axiom of infinity is provable in NF. It is explained why this is not a valid inference. Consequently, it would appear that there is a sense in which NF + AF is stronger than ML.

In the paper On the logic of quantification Prof. W. V. Quine showed that for the theory of quantification we have a mechanical process to determine whether or not a monadic expression is a valid logical formula, and that to deduce the polyadic theory from the monadic theory we need only the generalized modus ponens, which reads:

If a conditional is valid, and its antecedent consists of zero or more quantifiers followed by a valid schema, then its consequent is valid, i.e.:

That we have a mechanical process to determine the validity of a monadic expression was pointed out by Löwenheim long ago; Quine's method, however, has the merit that it is very simple and hence practical. The present paper is to show that we may deduce the polyadic theory by means of only a mechanical process and the ordinary modus ponens alone, i.e., the schema,

or even by means of only the weakened modus ponens, i.e., the schema,

For, if an expression becomes monadic when we omit the initial all-quantifiers (i.e., those preceding every existence-quantifier) and regard the corresponding variables as constants, then evidently we may determine by a mechanical process whether or not it is a valid formula by examining the resulting monadic expression. For example, the expression

is of the same validity as the expression

and hence as the expression

We consider any set of Gentzen-type rules in a formal system of the following sort. The terms of the system are propositions, generally to be thought of as the propositions of some underlying theory. The elementary statements are of the form

where and are finite sequences of propositions and (1) expresses a relation, called entailment, between such sequences. These sequences will be called prosequences; they may be void, or consist of a single proposition; and they may contain repetitions of the same proposition. The members of a prosequence will be called its constituents. Two prosequences which are permutations of one another will be regarded as the same. Prosequences will be designated by German letters, single propositions by Latin ones.

The rules of the system are to be of the following form:

This notation is to be understood as indicating p premises and a conclusion, each of the form (1). The constituents of and occur in all premises and conclusion; they are called the parametric constituents, or simply the parameters, of the inference.

The present paper contains an emendation to the theory of formal deducibility which was presented in lectures at the University of Notre Dame in the spring of 1948 [4]. The method of proof developed in these lectures for the elimination theorem, which corresponds to the “Hauptsatz” of Gentzen's thesis [6], failed when modal connectives were present. This deficiency was remedied soon thereafter; but it was not possible to include the new proof in those lectures. This new proof is presented below.

Before proceeding to this proof, the elimination theorem will be formulated, and its proof outlined, in an abstract form. Certain general conditions on the rules are formulated in §1; then, in §2, it is shown that the first two stages of the elimination theorem go through for any rules satisfying the conditions. The modifications necessary to extend this proof to cases where modal rules are present will then be taken care of in the later sections. A section on the extension of the elimination theorem to the singular form of LC is added at the end.