The first order functional calculus was proved complete by Gödel in 1930. Roughly speaking, this proof demonstrates that each formula of the calculus is a formal theorem which becomes a true sentence under every one of a certain intended class of interpretations of the formal system.

For the functional calculus of second order, in which predicate variables may be bound, a very different kind of result is known: no matter what (recursive) set of axioms are chosen, the system will contain a formula which is valid but not a formal theorem. This follows from results of Gödel concerning systems containing a theory of natural numbers, because a finite categorical set of axioms for the positive integers can be formulated within a second order calculus to which a functional constant has been added.

By a valid formula of the second order calculus is meant one which expresses a true proposition whenever the individual variables are interpreted as ranging over an (arbitrary) domain of elements while the functional variables of degree n range over all sets of ordered n-tuples of individuals. Under this definition of validity, we must conclude from Gödel's results that the calculus is essentially incomplete.

It happens, however, that there is a wider class of models which furnish an interpretation for the symbolism of the calculus consistent with the usual axioms and formal rules of inference. Roughly, these models consist of an arbitrary domain of individuals, as before, but now an arbitrary class of sets of ordered n-tuples of individuals as the range for functional variables of degree n. If we redefine the notion of valid formula to mean one which expresses a true proposition with respect to every one of these models, we can then prove that the usual axiom system for the second order calculus is complete: a formula is valid if and only if it is a formal theorem.

In a recent note Bergmann states that “nonextensional languages may contain sentences from which contextually denned predicates are not eliminable.” A restatement of his argument is as follows. Suppose L is a functional calculus of fourth order. Included among the definitions occurring in L is

Let ϕ occur in A (where A represents a well-formed formula of L) without an argument. The elimination of ϕ from A in accordance with (1) requires

The proof of (2) depends on the principle of extensionality

Hence Bergmann's conclusion “no such general elimination rule can be constructed for nonextensional languages.”

For Gentzen's natural deduction, a formalized method of deduction in quantification theory dating from 1934, these important advantages may be claimed: it corresponds more closely than other methods of formalized quantification theory to habitual unformalized modes of reasoning, and it consequently tends to minimize the false moves involved in seeking to construct proofs. The object of this paper is to present and justify a simplification of Gentzen's method, to the end of enhancing the advantages just claimed. No acquaintance with Gentzen's work will be presupposed.

A further advantage of Gentzen's method, also somewhat enhanced in my revision of the method, is relative brevity of proofs. In the more usual systematizations of quantification theory, theorems are derived from axiom schemata by proofs which, if rendered in full, would quickly run to unwieldy lengths. Consequently an abbreviative expedient is usually adopted which consists in preserving and numbering theorems for reference in proofs of subsequent theorems. Further brevity is commonly gained by establishing metatheorems, or derived rules, for reference in proving subsequent theorems. In natural deduction, on the other hand, proofs tend to be so short that the abbreviative expedients just now mentioned may conveniently be dispensed with—at least until theorems of extraordinary complexity are embarked upon. In natural deduction accordingly it is customary to start each argument from scratch, without benefit of accumulated theorems or derived rules.

In mathematics, when we want to introduce classes which fulfill certain conditions, we usually prove beforehand that classes fulfilling such conditions do exist, and that such classes are uniquely determined by the conditions. The statements which state such unicity and existence of classes are in mathematical logic consequences of the principles of extensionality and class existence. In order to illustrate how these principles enable us to introduce classes into systems of mathematical logic, let us consider the manner in which Gödel introduces classes in his book on set theory.

For instance, before introducing the definition of the non-ordered pair of two classes

Gödel puts down as its justification the following two axioms:

By A4, for every two classes y and z there exists at least one non-ordered pair w of them; and by A3, w is uniquely determined in A4.

In his doctor's thesis [1], Henkin has shown that if a formal logic is consistent, and sufficiently complex (for instance, if it is adequate for number theory), then it must admit a non-standard model. In particular, he showed that there must be a model in which that portion of the model which is supposed to represent the positive integers of the formal logic is not in fact isomorphic to the positive integers; indeed it is not even well ordered by what is supposed to be the relation of ≦.

For the purposes of the present paper, we do not need a precise definition of what is meant by a standard model of a formal logic. The non-standard models which we shall discuss will be flagrantly non-standard, as for instance a model of the sort whose existence is proved by Henkin. It will suffice if we and our readers are in agreement that a model of a formal logic is not a standard model if either:

(a) The relation in the model which represents the equality relation in the formal logic is not the equality relation for objects of the model.

(b) That portion of the model which is supposed to represent the positive integers of the formal logic is not well ordered by the relation ≦.

(c) That portion of the model which is supposed to represent the ordinal numbers of the formal logic is not well ordered by the relation ≦.

Let

We shall show that every formula in the elementary arithmetic of positive integers may be constructed out of matrices of the form ϕ(x, y) by means of quantifiers and the stroke. For Julia Robinson has shown that the successor function and the relation of divisibility are sufficient to define addition and multiplication; but from elementary considerations

and

In a simple, applied functional calculus of first order (i.e., one admitting no functional variables but at least one functional constant), abstracts or schematic expressions may be introduced to play the role of variables over designatable sets or classes. The entities or quasi-entities designated or quasi-designated by such abstracts may be called, following Quine, virtual classes and relations. The notion of virtual class is always relative to a given formalism and depends upon what functional constants are taken as primitive. The first explicit introduction of a general notation for virtual classes (relative to a given formalism) appears to be D4.1 of the author's A homogeneous system for formal logic. That paper develops a system admitting only individuals as values for variables and is adequate for the theory of general recursive functions of natural numbers. Numbers and functions are in fact identified with certain kinds of virtual classes and relations.

In the present paper it will be shown how certain portions of the theory of real numbers can be constructed upon the basis of the theory of virtual classes and relations of H.L.

The method of building up the real numbers to be employed is essentially an adaptation of standard procedure. Although the main ideas underlying this method are well known, the mirroring of these ideas within the framework of the restricted concepts admitted here presents possibly some novelty. In particular, a basis for the real numbers is provided which in no way admits classes or relations or other "abstract" objects as values for variables. Presupposing the natural numbers, the essential steps are to construct the simple rationals as virtual dyadic relations between natural numbers, to construct the generalized or signed rationals as virtual tetradic relations among natural numbers, and then to formulate a notation for real numbers as virtual classes (of a certain kind) of generalized rationals. Of course, there are several alternative methods. This procedure, however, appears to correspond more to the usual one.