Every system of signs that is defined in logical syntax may be called a formal language. It need not always be a language in the ordinary sense of the word. The rules of chess, e.g., can be expressed in the terminology of the syntax, but it would not occur to anybody to call chess a language.

A language in the ordinary sense has a meaning. That is to say that certain words in it are names of things or states or properties or relationships. In general it can be said that in any language having meaning all words subject to the rule of types are names. (Even sentences might be called names, i.e. names of facts, but we will not go so far.)

A syntax of a language L is a language with meaning, for the words of a definite type (in this paper of the type of individuals) contained in it are names of expressions of L.

If to a language we add its syntax, we get a language containing the syntax of one of its parts. If we formulate the syntax of a language L, in so far as its means allow, in the language L itself, we get a language containing a part of its syntax. We call such languages autosyntactic. It is well known that languages containing the whole of their own syntax do not exist.

Our method is based on the same principles which we have assumed in a paper about the foundations of metamathematics which we published in collaboration with J. Herzberg some years ago. Nevertheless we have introduced some important modifications which enable us to use a very restricted preliminary language and to avoid any artificial construction.

The problem of a restricted language in mathematics appears to be a very important one, as our ordinary language is really ambiguous and obscure. On the other hand there is the problem of restricting the intuitive logic to be used in our construction. We shall see that for this purpose we need only substitutions and modus ponens.

If we avoided any abbreviation, we could reduce our preliminary language to propositions of the following forms:

X is a theorem.

If P, then Q.

But we have to do with very long symbolic expressions and as there is not yet any machine to build up such expressions we must use abbreviations. For this purpose we shall use propositions of the following forms in the preliminary language:

X is an expression.

X is an abbreviation of Y.

Any proposition which does not belong to one of our four forms will be excluded from our construction.

Zu jedem Zählausdruck A in der allgemeinen pränexen Normalform

kann man bekanntlich einen, in bezug auf die Erfüllbarkeit, gleichwertigen Zählausdruck B in der spezielleren Normalform (Skolemsche Nonnalfonn)

konstruieren, indem man auf A mehrmals (n–1 Mal) das sogenannte Skolemsche Verfahren anwendet. Dieses Verfahren hat nämlich die Eigenschaft, daß es auf einen Zählausdruck in der pränexen Normalform n-ten Grades (n > 1) angewandt zu einem gleichwertigen Zählausdruck in der pränexen Normalform (n–1)-ten Grades führt, wobei unter “Grad eines Zählausdrucks in der pränexen Normalform, die ein mit einem Allzeichen beginnendes und mit einem Seinszeichen endendes Präfix hat” die Anzahl der durch Seinszeichen voneinander getrennten Komplexe von Allzeichen dieses Präfixes zu verstehen ist. Da nun A—wie aus (1) ersichtlich ist—ein Zählausdruck n-ten Grades ist, so kommt man nach (n–1)-maliger Anwendung des Skolemschen Verfahrens tatsächlich zu einem gleichwertigen Zählausdruck ersten Grades, also zu einem gleichwertigen Zählausdruck der Form (2).

Two errors have appeared in my dissertation. First, in the symbolic statement of Theorem (14.1), “r i ≁∧” should be “r i ≁∨.” Second, as J. C. C. McKinsey points out in his review, Theorem (10.8) is not correct. The error in the proof enters in the last application of Theorem (10.7), for which the hypothesis would be needed. The construction given at the bottom of page 35 is valid, however.

To state the correct theorem to replace Theorem (10.8), adopt the notation sylc (p) for any one of the mutually congruent polynomials resulting from the adjunction to p of all σ-terms informally included in p which are obtainable by eliminating c from pairs of terms of p.Then:

Theorem. .

In this paper the theory of logical types will be examined, and certain departures from it will be suggested. Though the purpose of the paper is not primarily expository, an approach has been possible which presupposes no familiarity with special literature. Matters at variance with such an approach have been confined to appendices and footnotes.

In the early pages the logical paradoxes will be considered—an infinite series of them, of which Russell's paradox is the first. Then Russell's simple theory of types will be formulated, in adaptation to a minimal set of logical primitives: inclusion and abstraction. Two aspects of the theory will be distinguished: an ontological doctrine and a formal restriction. It will be found that by repudiating the former we can avoid certain unnatural effects of the type theory—notably the reduplication of logical constants from type to type, and the apparent dependence of finite arithmetic upon an axiom of infinity. But the formal restriction itself has unnatural effects, which survive, even in an aggravated form, after the type ontology has been dropped. A liberalization of the formal restriction will be proposed which removes the more irksome of these anomalies.

When the axioms of infinity and choice are added to the system of logic of the second edition of Whitehead and Russell's Principia mathematica, and when, as in the second edition, the axiom of reducibility is omitted (so that the ramified nature of Russell's theory of types, especially his distinction between “orders,” is not in effect obliterated), the resulting system will hereafter be referred to as “the ramified Principia.” It will be shown that a certain system S, slightly stronger than the ramified Principia, is consistent, so that the ramified Principia itself is consistent. From Gödel's theorem it will then follow that the sort of mathematical induction employed in the consistency proof of S cannot be adequately handled within S or within the ramified Principia.

The method of proving the consistency of S will be roughly as follows: A consistent non-constructive system S′ will be defined by means of induction with respect to a serial well-ordering of all the propositions of S. It will then be shown that every true proposition of S is a true proposition of S′, so that S must also be consistent.

1. Preliminary conventions.

1.1. Definition. By a “symbol” is to be understood any typographical expression which does not consist of a horizontal collinear sequence of expressions. Expressions formed by adding indices to either of the two upper or two lower corners of a symbol will also be considered symbols.

The completeness of the prepositional calculus was first proved by Post. His somewhat condensed proof has been succeeded by more detailed presentations of substantially the same argument, and also by several proofs of radically different forms. The present paper contains still another proof, offered because of its relative simplicity. In part this proof follows a plan which was sketched by Wajsberg for another purpose, viz. for proving the completeness of the sub-calculus involving only the material conditional.

For the present proof a systematization of the propositional calculus will be used which is due to Tarski, Bernays, and Wajsberg. It involves the material conditional “⊃” and the falsehood “F” as primitive; thus the formulae are recursively describable as comprising “F”, the variables “p”, “q”, “r”, …, and all results of putting formulae for “p” and “q” in “(p⊃q)”. The denial “˜p” is definable as “(p⊃F)”, and all other truth functions are then definable in familiar fashion. (Conversely, in a system admitting “˜” instead of “F” as primitive, “F” might be explained as an abbreviation of “˜(P⊃P)”.) The postulates are four:

(1) ((p⊃q)⊃((q⊃r)⊃ (p⊃ r)))

(2) (((p⊃(q⊃p)⊃p)

(3) (p⊃(q⊃p))

(4) (F⊃p).

In Oskar Becker's Zur Logik der Modalitäten four systems of modal logic are considered. Two of these are mentioned in Appendix II of Lewis and Langford's Symbolic logic. The first system is based on A1–8 plus the postulate,

From A7: ∼◊p⊰∼p we can prove the converse of C11 by writing ∼◊p for p, and hence derive

The addition of this postulate to A1–8, as Becker points out, allows us to “reduce” all complex modal functions to six, and these six are precisely those which Lewis mentions in his postulates and theorems: p, ∼p, ◊p, ∼◊p, ∼◊∼p, and ◊∼p This reduction is accomplished by showing

where ◊n means that the modal operator ◊ is repeated n times; e.g., ◊3p = ◊◊◊p. Then it is shown that

By means of (1), (2), and (3) any complex modal function whatsoever may be reduced to one of the six “simple” modals mentioned above.

It might be asked whether this reduction could be carried out still further, i.e., whether two of the six “irreducible” modals could not be equated. But such a reduction would have to be based on the fact that ◊p = p which is inconsistent with the set B1–9 of Lewis and Langford's Symbolic logic and independent of the set A1–8. Hence for neither set would such a reduction be possible.

Consider a system of formal notations for ordinal numbers in the first and second number classes, with the following properties. Given a notation for an ordinal, it can be decided effectively whether the ordinal is zero, or the successor of an ordinal, or the limit of an increasing sequence of ordinals. In the second case, a notation for the preceding ordinal can be determined effectively. In the third case, notations for the ordinals of an increasing sequence of type ω with the given ordinal as limit can be determined effectively.

Are there systems of this sort which extend farthest into the second number class? When the conditions for the systems have been made precise, the question will be answered in the affirmative. There is an ordinal ω1 in the second number class such that there are systems of notations of the sort described which extend to all ordinals less than ω1, but none in which ω1 itself is assigned a notation.

1. An effective or constructive operation on the objects of an enumerable class is one for which a fixed set of instructions can be chosen such that, for each of the infinitely many objects (or n-tuples of objects), the operation can be completed by a finite process in accordance with the instructions. This notion is made exact by specifying the nature of the process and set of instructions. It appears possible to do so without loss of generality.