592 Mathematical Logic

Some metamathematical results on completeness and consistency, On formally undecidable propositions of Principia mathematica and related systems I, and On completeness and consistency

KURT GÖDEL n/a

(1930b, 1931, and 1931a)

1930b *Einige metamathematische Resultate über Entscheidungsdefinitheit und Widerspruchsfreiheit, Anzeiger der Akademie der Wissenschaften in Wien, Mathematisch-naturwissenschaftliche Klasse 67, 214–215 (communicated on 23 October 1930 by Hans Hahn; 595–596 of the present volume).

1931 *Über formal unentscheidbare Sätze der Principia mathematica und verwandter Systeme I, Monatshefte für Mathematik und Physik 38, 173–198 (596–616 of the present volume); English translations in Gödel 1962, 35–72, and in Davis 1965, 5–38 (but see Bauer-Mengelberg 1965 and 1966).

1931a *Über Vollständigkeit und Widerspruchsfreiheit, Ergebnisse eines mathematischen Kolloquiums 3 (1932), 12–13 (616–617 of the present volume).

The main paper below (1931), which was to have such an impact on modern logic, was received for publication on 17 November 1930 and published early in 1931. An abstract (1930b) had been presented on 23 October 1930 to the Vienna Academy of Sciences by Hans Hahn.

Gödel’s results are now accessible in many publications, but his original paper has not lost any of its value as a guide. It is clearly written and does not assume any previous result for its main line of argument. It is, moreover, rich in interesting details. We now give some indications of its contents and structure.

Section 1 is an informal presentation of the main argument and can be read by the nonmathematician; it shows how the argument, by dealing with the proposition that states of itself "I am not provable", instead of the proposition that states of itself "I am not true", skirts the Liar paradox, without falling into it. Gödel also brings to light the relation that his argument bears to Cantor’s diagonal procedure and Richard’s paradox (Herbrand, on pages 626–628 below, and Weyl (1949, pp. 219–235) particularly stress this aspect of Gödel’s argument; see also above, p. 439).

Section 2, the longest, is the proof of Theorem VI. The theorem states that in a formal system satisfying certain precise conditions there is an undecidable proposition, that is, a proposition such that neither the proposition itself nor its negation is provable in the system. Before coming to the core of the argument, Gödel takes a number of preparatory steps:

(1) A precise description of the system P with which he is going to work. The variables are distinguished as to their types and they range over the natural numbers (type 1), classes of natural numbers (type 2), classes of classes of natural numbers (type 3), and so forth. The logical axioms are equivalent to the logic of Principia mathematica without the ramified theory of types. The arithmetic axioms are Peano’s, properly transcribed. The identification of the individuals with the natural numbers and 593 the adjunction of Peano’s axioms (instead of their derivation, as in Principia) have the effect that every formula has an interpretation in classical mathematics and, if closed, is either true or false in that interpretation; moreover, proofs are considerably shortened.

(2) An assignment of natural numbers to sequences of signs of P and a similar assignment to sequences of sequences of signs of P. The first assignment is such that, given a sequence, the number assigned to it can be effectively calculated, and, given a number, we can effectively decide whether the number is assigned to a sequence and, if it is, actually write down the sequence; similarly for the second assignment. By means of these assignments we can correlate number-theoretic predicates with metamathematical notions used in the description of the system; for example, to the notion "axiom" corresponds the predicate Ax(x), which holds precisely of the numbers x that are assigned to axioms (the "Gödel numbers" of axioms, we would say today).

(3) A definition of primitive recursive functions (Gödel calls them recursive functions) and the derivation of a few theorems about them. These functions had already been used in foundational research (for example, by Dedekind (1888), Skolem (1923), Hilbert (1925, 1927), and Ackermann (1928)); Gödel gives a precise definition of them, which has become standard.

(4) The proof that forty-five number-theoretic predicates, forty of them associated with metamathematical notions, are primitive recursive.

(5) The proof that every primitive recursive number-theoretic predicate is numeralwise representable in P. That is, the predicate holds of some given numbers if and only if a definite formula of P is provable whenever its free variables are replaced by the symbols that represent these numbers in P.

(6) The definition of ω-consistency.

Gödel can then undertake to prove Theorem VI. The scope of the theorem is enlarged by the addition of any ω-consistent primitive recursive class κ of formulas to the axioms of P. For each such κ a different system is thus obtained (in the present note, a notation not used by Gödel, will denote the system corresponding to a given κ). After the proof Gödel makes a number of important remarks:

(a) He points out the constructive content of Theorem VI.

(b) He introduces predicates that are entscheidungsdefinit (in the translation below these are called decidable predicates, at the author’s suggestion). If we take into account the few lines added in proof at the end of a later note of Gödel’s (1934a), these predicates are in fact those that today we call recursive (that is, general recursive) predicates. Gödel somewhat extends the result of Theorem VI by assuming only that κ is decidable, and not that it is primitive recursive.

(c) If κ is assumed to be merely consistent, instead of ω-consistent, the proof yields the existence of a predicate whose universalization is not provable but for which no counterexample can be given; is ω-incomplete, as we would say today.

(d) The adjunction of the undecidable formula Neg(17 Gen r) to κ yields a consistent but ω-inconsistent system.

(e) Even with the adjunction of the axiom of choice or the continuum hypothesis the system contains undecidable propositions.

The section ends with a review of the properties of P that are actually used in the proof and the remark that all known axiom systems of mathematics, or of any substantial part of it, have these properties.

Section 3 presents two supplementary undecidability results. Gödel establishes (Theorem VII) that a primitive recursive number-theoretic predicate is arithmetic, 594 that is, can be expressed as a formula of first-order number theory (this yields a stronger result than the numeralwise representability of such predicates, as it was introduced and used in Section 2). Hence every formula of the form (x)F(x), with F(x) primitive recursive, is equivalent to an arithmetic formula; moreover, this equivalence is provable in one can review the informal proof presented by Gödel and check that is strong enough to express and justify each of its steps. Since the proposition that was proved to be undecidable in Theorem VI is of the form (x)F(x), with F(x) primitive recursive, contains undecidable arithmetic propositions (Theorem VIII). For all its strength, the system cannot decide every first-order number-theoretic proposition. Theorem X states that, given a formula (x)F(x), with F(x) primitive recursive, one can exhibit a formula of the pure first-order predicate calculus, say A, that is satisfiable if and only if (x)F(x) holds. Moreover, since contains a set theory, the equivalence

is expressible in and, as one can verify by reviewing Gödel’s informal argument, provable in Therefore (Theorem IX) there are formulas of the pure first-order predicate calculus whose validity is undecidable in

In Section 4 an important consequence of Theorem VI is derived. The statement "there exists in an unprovable for-mula", which expresses the consistency of , can be written as a formula of but this formula is not provable in (Theorem XI). The main step in the demonstration of this result consists in reviewing the proof of the first half of Theorem VI and checking that all the statements made in that proof can be expressed and proved in It is clear that this is the case, and Gödel does not go through the details of the demonstration. The section ends with various remarks on Theorem XI (its constructive character, its applicability to set theory and ordinary analysis, its effect upon Hilbert’s conception of mathematics).

Gödel’s paper immediately attracted the interest of logicians and, although it caused some momentary surprise, its results were soon widely accepted. A number of studies were directly inspired by it. By using a somewhat more complicated predicate than "is provable in P", Rosser (1936) was able to weaken the assumption of ω-consistency in Theorem VI to that of ordinary consistency. Hilbert and Bernays (1939, pp. 283–340) carried out in all details the proof of the analogue of Theorem XI for two standard systems of number theory, and Z, and this proof can be transferred almost literally to any system containing Z. As Gödel indicates in a note appended to the present translation of his paper, Turing’s work (1937) gave to the notion of formal system its full generality. The notes of Gödel’s Princeton lectures (1934) contain the most important results of the present paper, in a more succinct form; they also make precise the notion of (general) recursive function, already suggested by Herbrand (see below, p. 618). In developing the theory of these functions, Kleene (1936) obtained undecidability results of a somewhat different character from those presented here. Gödel’s work led to Church’s negative solution (1936) of the decision problem for the predicate calculus of first order. Tarski (1953) developed a general theory of undecidability. The device of the "arithmetization" of metamathematics became an everyday tool of the research worker in foundations. Gödel’s results, finally, led to a profound revision of Hilbert’s program (on that point see, among other texts, Bernays 1938, 1954 and Gödel 1958).

These indications are far from giving a full account of the deep influence exerted in the field of foundations of mathematics by the results presented in the paper below and the methods used to 595 obtain them. There is not one branch of research, except perhaps intuitionism, that has not been pervaded by this influence.

The translation of the paper is by the editor, and it is printed here with the kind permission of Professor Gödel and Springer Verlag. Professor Gödel approved the translation, which in many places was accommodated to his wishes. He suggested, in particular, the various phrases used to render the word "inhalt-lich". He also proposed a number of short interpolations to help the reader, and these have been introduced in the text below between square brackets.

Below, on page 601, the author shows how a number-theoretic predicate can be associated with a given metamathematical notion and then used to represent the notion. In the German text such a predicate is denoted by the same word as the original notion, except that the word is printed in italics. Since in English italics are used for emphasis (while the German text uses letter spacing for that purpose), the translation below uses SMALL CAPITALS for the names of these predicates. This scheme of italicization (or small capitalization), however, is used for only some of the number-theoretic predicates in question. According to Professor Gödel, "the idea was to use the notation only for those metamathematical notions that had been defined in their usual sense before, namely, those defined on pp. 599–601. From p. 607 up to the general considerations at the end of Section 2, and again in Section 4, every metamathe-matical term referring to the system P is supposed to denote the corresponding arithmetic one. But, of course, because of the complete isomorphism the distinction in many cases is entirely irrelevant".

Before the main text the reader will find a translation, by Stefan Bauer-Mengelberg, of its abstract (1930b); in that translation, at the author’s suggestion, "entscheidungsdefinit", when referring to an axiom system, has been translated by "complete", and "Entscheidungsdefinitheit" by "completeness". A translation, by the editor, of 1931a, a note dated 22 January 1931 and closely connected with 1931, follows the main text. Both translations are printed here with the kind permission of Professor Gödel.

SOME METAMATHEMATICAL RESULTS ON COMPLETENESS AND CONSISTENCY

KURT GÖDEL n/a

(1930b)

If to the Peano axioms we add the logic of Principia mathematica¹ (with the natural numbers as the individuals) together with the axiom of choice (for all types), we obtain a formal system S, for which the following theorems hold:

I. The system S is not complete [entscheidungsdefinit]; that is, it contains propositions A (and we can in fact exhibit such propositions) for which neither A nor is provable and, in particular, it contains (even for decidable properties F of natural numbers) undecidable problems of the simple structure (Ex)F(x), where x ranges over the natural numbers.²

II. Even if we admit all the logical devices of Principia mathematica (hence in particular the extended functional calculus¹ and the axiom of choice) in metamathe-matics, there does not exist a consistency proof for the system S (still less so if we 596 restrict the means of proof in any way). Hence a consistency proof for the system S can be carried out only by means of modes of inference that are not formalized in the system S itself, and analogous results hold for other formal systems as well, such as the Zermelo-Fraenkel axiom system of set theory.³

III. Theorem I can be sharpened to the effect that, even if we add finitely many axioms to the system S (or infinitely many that result from a finite number of them by "type elevation"), we do not obtain a complete system, provided the extended system is ω-consistent. Here a system is said to be ω-consistent if, for no property F(x) of natural numbers,

ad infinitum

as well as

are provable. (There are extensions of the system S that, while consistent, are not ω-consistent.)

IV. Theorem I still holds for all ω-consistent extensions of the system S that are obtained by the addition of infinitely many axioms, provided the added class of axioms is decidable [entscheidungsdefinit], that is, provided it is metamathematically decidable [entscheidbar] for every formula whether it is an axiom or not (here again we suppose that the logic used in metamathematics is that of Principia mathematica).

Theorems I, III, and IV can be extended also to other formal systems, for example, to the Zermelo-Fraenkel axiom system of set theory, provided the systems in question are ω-consistent.

The proofs of these theorems will appear in Monatshefte für Mathematik und Physik.

ON FORMALLY UNDECIDABLE PROPOSITIONS OF PRINCIPIA MATHEMATICA AND RELATED SYSTEMS I

KURT GÖDEL n/a

(1931)

1

The development of mathematics toward greater precision has led, as is well known, to the formalization of large tracts of it, so that one can prove any theorem using nothing but a few mechanical rules. The most comprehensive formal systems that have been set up hitherto are the system of Principia mathematica (PM)² on the one hand and the Zermelo-Fraenkel axiom system of set theory (further developed by J. von Neumann)³ on the other. These two systems are so comprehensive that in 597 them all methods of proof today used in mathematics are formalized, that is, reduced to a few axioms and rules of inference. One might therefore conjecture that these axioms and rules of inference are sufficient to decide any mathematical question that can at all be formally expressed in these systems. It will be shown below that this is not the case, that on the contrary there are in the two systems mentioned relatively simple problems in the theory of integers⁴ that cannot be decided on the basis of the axioms. This situation is not in any way due to the special nature of the systems that have been set up but holds for a wide class of formal systems; among these, in particular, are all systems that result from the two just mentioned through the addition of a finite number of axioms,⁵ provided no false propositions of the kind specified in footnote 4 become provable owing to the added axioms.

Before going into details, we shall first sketch the main idea of the proof, of course without any claim to complete precision. The formulas of a formal system (we restrict ourselves here to the system PM) in outward appearance are finite sequences of primitive signs (variables, logical constants, and parentheses or punctuation dots), and it is easy to state with complete precision which sequences of primitive signs are meaningful formulas and which are not.⁶ Similarly, proofs, from a formal point of view, are nothing but finite sequences of formulas (with certain specifiable properties.) Of course, for metamathematical considerations it does not matter what objects are chosen as primitive signs, and we shall assign natural numbers to this use.⁷ Consequently, a formula will be a finite sequence of natural numbers,⁸ and a proof array a finite sequence of finite sequences of natural numbers. The metamathematical notions (propositions) thus become notions (propositions) about natural numbers or sequences of them;⁹ therefore they can (at least in part) be expressed by the symbols of the system PM itself. In particular, it can be shown that the notions "formula", "proof array", and "provable formula" can be defined in the system PM; that is, we can, for example, find a formula F(v) of PM with one free variable v (of the type of a number sequence)¹⁰ such that F(v), interpreted according to the meaning of the terms of PM, says: v is a provable formula. We now construct an undecidable proposition of the system PM, that is, a proposition A for which neither A nor not-A is provable, in the following manner.

598

A formula of PM with exactly one free variable, that variable being of the type of the natural numbers (class of classes), will be called a class sign. We assume that the class signs have been arranged in a sequence in some way,¹¹ we denote the nth one by R(n), and we observe that the notion "class sign", as well as the ordering relation R, can be defined in the system PM. Let α be any class sign; by [α; n] we denote the formula that results from the class sign α when the free variable is replaced by the sign denoting the natural number n. The ternary relation too, is seen to be definable in PM. We now define a class K of natural numbers in the following way:

(where Bew x means: x is a provable formula).^11a Since the notions that occur in the definiens can all be defined in PM, so can the notion K formed from them; that is, there is a class sign S such that the formula [S; n], interpreted according to the meaning of the terms of PM, states that the natural number n belongs to K.¹² Since S is a class sign, it is identical with some R(q); that is, we have

for a certain natural number q. We now show that the proposition [R(q); q] is un-decidable in PM.¹³ For let us suppose that the proposition [R(q); q] were provable; then it would also be true. But in that case, according to the definitions given above, q would belong to K, that is, by (1), would hold, which contradicts the assumption. If, on the other hand, the negation of [R(q); q] were provable, then ^13a that is, Bew [R(q); q], would hold. But then [R(q); q], as well as its negation, would be provable, which again is impossible.

The analogy of this argument with the Richard antinomy leaps to the eye. It is closely related to the "Liar" too;¹⁴ for the undecidable proposition [R(q); q] states that q belongs to K, that is, by (1), that [R(q); q] is not provable. We therefore have before us a proposition that says about itself that it is not provable [in PM].¹⁵ The method of proof just explained can clearly be applied to any formal system that, first, when interpreted as representing a system of notions and propositions, has at 599 its disposal sufficient means of expression to define the notions occurring in the argument above (in particular, the notion "provable formula") and in which, second, every provable formula is true in the interpretation considered. The purpose of carrying out the above proof with full precision in what follows is, among other things, to replace the second of the assumptions just mentioned by a purely formal and much weaker one.

From the remark that [R(q); q] says about itself that it is not provable it follows at once that [R(q); q] is true, for [R(q); q] is indeed unprovable (being undecidable). Thus, the proposition that is undecidable in the system PM still was decided by metamathematical considerations. The precise analysis of this curious situation leads to surprising results concerning consistency proofs for formal systems, results that will be discussed in more detail in Section 4 (Theorem XI).

2

We now proceed to carry out with full precision the proof sketched above. First we give a precise description of the formal system P for which we intend to prove the existence of undecidable propositions. P is essentially the system obtained when the logic of PM is superposed upon the Peano axioms¹⁶ (with the numbers as individuals and the successor relation as primitive notion).

The primitive signs of the system P are the following:

I. Constants: "~" (not), (or), "Π" (for all), "0" (zero), "f" (the successor of), "(", ")" (parentheses);

II. Variables of type 1 (for individuals, that is, natural numbers including 0):

Variables of type 2 (for classes of individuals):

Variables of type 3 (for classes of classes of individuals):

And so on, for every natural number as a type.¹⁷

Remark: Variables for functions of two or more argument places (relations) need not be included among the primitive signs since we can define relations to be classes of ordered pairs, and ordered pairs to be classes of classes; for example, the ordered pair a, b can be defined to be ((a), (a, b)), where (x, y) denotes the class whose sole elements are x and y, and (x) the class whose sole element is x.¹⁸

By a sign of type 1 we understand a combination of signs that has [any one of] the forms

a, fa, ffa, fffa, . . ., and so on,

where a is either 0 or a variable of type 1. In the first case, we call such a sign a numeral. For we understand by a sign of type n the same thing as by a variable of type n. A combination of signs that has the form a(b), where b is a sign of type n 600 and a a sign of type will be called an elementary formula. We define the class of formulas to be the smallest class¹⁹ containing all elementary formulas and containing (where x may be any variable)^18a whenever it contains a and b. We call the disjunction of a and b, ~ (a) the negation and xΠ(a) a generalization of a. A formula in which no free variable occurs (free variable being defined in the well-known manner) is called a sentential formula [Satzformel]. A formula with exactly n free individual variables (and no other free variables) will be called an n-place relation sign; for it will also be called a class sign.

By Subst (where a stands for a formula, v for a variable, and b for a sign of the same type as v) we understand the formula that results from a if in a we replace v, wherever it is free, by b.²⁰ We say that a formula a is a type elevation of another formula b if a results from b when the type of each variable occurring in b is increased by the same number.

The following formulas (I-V) are called axioms (we write them using these abbrevi-ations, defined in the well-known manner: ²¹ and observing the usual conventions about omitting parentheses):²²

I.

II. All formulas that result from the following schemata by substitution of any formulas whatsoever for p, q, r:

III. Any formula that results from either one of the two schemata

when the following substitutions are made for a, v, b, and c (and the operation indicated by "Subst" is performed in 1):

For a any formula, for v any variable, for b any formula in which v does not occur free, and for c any sign of the same type as v, provided c does not contain any variable that is bound in a at a place where v is free.²³

601

IV. Every formula that results from the schema

when for v we substitute any variable of type n, for u one of type and for a any formula that does not contain u free. This axiom plays the role of the axiom of reducibility (the comprehension axiom of set theory).

V. Every formula that results from

by type elevation (as well as this formula itself). This axiom states that a class is completely determined by its elements.

A formula c is called an immediate consequence of a and b if it is the formula and it is called an immediate consequence of a if it is the formula vΠ(a), where v denotes any variable. The class of provable formulas is defined to be the smallest class of formulas that contains the axioms and is closed under the relation "immediate consequence".²⁴

We now assign natural numbers to the primitive signs of the system P by the following one-to-one correspondence:

to the variables of type n we assign the numbers of the form pⁿ (where p is a prime number > 13). Thus we have a one-to-one correspondence by which a finite sequence of natural numbers is associated with every finite sequence of primitive signs (hence also with every formula). We now map the finite sequences of natural numbers on natural numbers (again by a one-to-one correspondence), associating the number where P_k denotes the kth prime number (in order of increasing magnitude), with the sequence A natural number [out of a certain subset] is thus assigned one-to-one not only to every primitive sign but also to every finite sequence of such signs. We denote by Φ(a) the number assigned to the primitive sign (or to the sequence of primitive signs) a. Now let some relation (or class) between [or of] primitive signs or sequences of primitive signs be given. With it we associate the relation (or class) between [or of] natural numbers that obtains between if and only if there are some such that and hold. The relations between (or classes of) natural numbers that in this manner are associated with the metamathematical notions defined so far, for example, "variable", "formula", "sentential formula", "axiom", "provable formula", and so on, will be denoted by the same words in SMALL CAPITALS. The proposition that there are undecidable problems in the system P, for example, reads thus: There are SENTENTIAL FORMULAS a such that neither a nor the NEGATION of a is a PROVABLE FORMULA.

We now insert a parenthetic consideration that for the present has nothing to do 602 with the formal system P. First we give the following definition: A number-theoretic function²⁵ is said to be recursively defined in terms of the number-theoretic functions and if

hold for all ²⁶

A number-theoretic function φ is said to be recursive if there is a finite sequence of number-theoretic functions that ends with φ and has the property that every function of the sequence is recursively defined in terms of two of the preceding functions, or results from any of the preceding functions by substitution,²⁷ or, finally, is a constant or the successor function The length of the shortest sequence of φ_i corresponding to a recursive function φ is called its degree. A relation between natural numbers is said to be recursive²⁸ if there is a recursive function such that, for all

.²⁹

The following theorems hold:

I. Every function (relation) obtained from recursive functions (relations) by substitution of recursive functions for the variables is recursive; so is every function obtained from recursive functions by recursive definition according to schema (2);

II. If R and S are recursive relations, so areand (hence also R & S);

III. If the functionsandare recursive, so is the relation ;³⁰

IV. If the functionand the relationare recursive, so are the relations S and T defined by

and

as well as the function ψ defined by

where εxF(x) means the least number x for which F(x) holds and 0 in case there is no such number.

603

Theorem I follows at once from the definition of "recursive". Theorems II and III are consequences of the fact that the number-theoretic functions

corresponding to the logical notions and =, namely,

when x and y are both

when when

are recursive, as we can readily see. The proof of Theorem IV is briefly as follows. By assumption there is a recursive such that

We now define a function by the recursion schema (2) in the following way:

³¹

where Therefore is equal either to or to ³² The first case clearly occurs if and only if all factors of a are 1, that is, if

holds. From this it follows that the function (considered as a function of n) remains 0 up to [but not including] the least value of n for which holds and, from there on, is equal to that value. (Hence, in case holds, is constant and equal to 0.) We have, therefore,

The relation T can, by negation, be reduced to a case analogous to that of S. Theorem IV is thus proved.

The functions and x^y, as well as the relations and are recursive, as we can readily see. Starting from these notions, we now define a number of functions (relations) 1–45, each of which is defined in terms of preceding ones by the procedures given in Theorems I–IV. In most of these definitions several of the steps allowed by Theorems I–IV are condensed into one. Each of the functions (relations) 1–45, among which occur, for example, the notions "FORMULA", "AXIOM", and "IMMEDIATE CONSEQUENCE", is therefore recursive.

1. ³³

x is divisible by y.³⁴

604

2.

x is a prime number.

3.

n Pr x is the nth prime number (in order of increasing magnitude) contained in x.^34a

4.

5.

Pr(n) is the nth prime number (in order of increasing magnitude).

6.

n Gl x is the nth term of the number sequence assigned to the number x (for and n not greater than the length of this sequence).

7.

l(x) is the length of the number sequence assigned to x.

8.

corresponds to the operation of "concatenating" two finite number sequences.

9.

R(x) corresponds to the number sequence consisting of x alone (for

10.

E(x) corresponds to the operation of "enclosing within parentheses" (11 and 13 are assigned to the primitive signs "(" and ")", respectively).

11.

x is a VARIABLE OF TYPE n.

12.

x is a VARIABLE.

13.

Neg(x) is the NEGATION of x.

14.

x Dis y is the DISJUNCTION of x and y.

15.

x Gen y is the GENERALIZATION of y with respect to the VARIABLE x (provided x is a VARIABLE).

16.

n N x corresponds to the operation of "putting the sign ’f’ n times in front of x".

17.

Z(n) is the NUMERAL denoting the number n.

18. ^34b

x is a SIGN OF TYPE 1.

605

19.

x is a SIGN OF TYPE n.

20.

x is an ELEMENTARY FORMULA.

21.

22.

x is a SEQUENCE OF FORMULAS, each of which either is an ELEMENTARY FORMULA or results from the preceding FORMULAS through the operations of NEGATION, DIS-JUNCTION, or GENERALIZATION.

23. ³⁵

x is a FORMULA (that is, the last term of a FORMULA SEQUENCE n).

24.

the VARIABLE v is BOUND in x at the nth place.

25.

the VARIABLE v is FREE in x at the nth place.

26.

v occurs as a FREE VARIABLE in x.

27.

results from x when we substitute y for the nth term of x (provided that

28.

k St v, x is the place in x (counted from the right end of the FORMULA x) at which v is FREE in x (and 0 in case there is no such place).

29.

A(v, x) is the number of places at which v is FREE in x.

30.

31. ,³⁶

is the notion SUBST defined above.³⁷

32.

606

33.

n Th x is the nth TYPE ELEVATION of x (in case x and n Th x are FORMULAS).

Three specific numbers, which we denote by z₁, z₂, and z₃ , correspond to the Axioms I, 1–3, and we define

34.

35.

x is a FORMULA resulting from Axiom schema II, 1 by substitution. Analogously, and are defined for Axioms [rather, Axiom Schemata] II, 2–4.

36.

x is a FORMULA resulting from a propositional axiom by substitution.

37.

z does not contain any VARIABLE BOUND in y at a place at which v is FREE.

38.

x is a FORMULA resulting from Axiom schema III, 1 by substitution.

39.

x is a FORMULA resulting from Axiom schema III, 2 by substitution.

40.

x is a FORMULA resulting from Axiom schema IV, 1 by substitution.

A specific number z₄ corresponds to Axiom V, 1, and we define:

41.

42.

x is an AXIOM.

43.

x is an IMMEDIATE CONSEQUENCE of y and z.

44.

x is a PROOF ARRAY (a finite sequence of FORMULAS, each of which is either an AXIOM or an IMMEDIATE CONSEQUENCE of two of the preceding FORMULAS.

45.

x is a PROOF of the FORMULA y.

46.

x is a PROVABLE FORMULA. (Bew(x) is the only one of the notions 1–46 of which we cannot assert that it is recursive.)

The fact that can be formulated vaguely by saying: every recursive relation is definable in the system P (if the usual meaning is given to the formulas of this system), is expressed in precise language, without reference to any interpretation of the formulas of P, by the following theorem:

Theorem V. For every recursive relationthere exists an n-place 607 RELATION SIGN r (with the FREE VARIABLES³⁸such that for all n-tuples of numberswe have

We shall give only an outline of the proof of this theorem because the proof does not present any difficulty in principle and is rather long.³⁹ We prove the theorem for all relations of the form ⁴⁰ (where φ is a recursive function) and we use induction on the degree of φ. For functions of degree 1 (that is, constants and the function the theorem is trivial. Assume now that φ is of degree m. It results from functions of lower degrees, through the operations of substitution or recursive definition. Since by the induction hypothesis everything has already been proved for there are corresponding RELATION SIGNS, such that (3) and (4) hold. The processes of definition by which φ results from (substitution and recursive definition) can both be formally reproduced in the system P. If this is done, a new RELATION SIGN r is obtained from ⁴¹ and, using the induction hypothesis, we can prove without difficulty that (3) and (4) hold for it. A RELATION SIGN r assigned to a recursive relation⁴² by this procedure will be said to be recursive.

We now come to the goal of our discussions. Let κ be any class of FORMULAS. We denote by Flg(κ) (the set of consequences of κ) the smallest set of FORMULAS that contains all FORMULAS of κ and all AXIOMS and is closed under the relation "IMMEDIATE CONSEQUENCE". κ is said to be ω-consistent if there is no CLASS SIGN a such that

where v is the FREE VARIABLE of the CLASS SIGN a.

Every ω-consistent system, of course, is consistent. As will be shown later, however, the converse does not hold.

The general result about the existence of undecidable propositions reads as follows:

Theorem VI. For every ω-consistent recursive class ω of FORMULAS there are recursive CLASS SIGNS r such that neither v Gen r nor Neg(v Gen r) belongs to Flg(ω) (where v is the FREE VARIABLE of r).

Proof. Let κ be any recursive ω-consistent class of FORMULAS. We define

608

(see the analogous notion 44),

(see the analogous notions 45 and 46).

We obviously have

and

We now define the relation

Since (by (6) and (5)) and (by Definitions 17 and 31) are recursive, so is Q(x, y). Therefore, by Theorem V and (8) there is a RELATION SIGN q (with the FREE VARIABLES 17 and 19) such that

and

We put

(p is a CLASS SIGN with the FREE VARIABLE 19) and

(r is a recursive CLASS SIGN⁴³ with the FREE VARIABLE 17).

Then we have

(by (11) and (12));⁴⁴ furthermore

(by (12)). If we now substitute p for y in (9) and (10) and take (13) and (14) into account, we obtain

This yields:

1. 17 Gen r is not κ-PROVABLE.⁴⁵ For, if it were, there would (by (6.1)) be an n such 609 that Hence by (16) we would have while, on the other hand, from the κ-PROVAILITY of 17 Gen r that of follows. Hence, κ would be inconsistent (and a fortiori ω-inconsistent).

2. Neg(17 Gen r) is not κ-PROVABLE. Proof: As has just been proved, 17 Gen r is not κ-PROVABLE; that is (by (6.1)), holds. From this, follows by (15), and that, in conjunction with is incompatible with the ω-consistency of κ.

17 Gen r is therefore undecidable on the basis of κ, which proves Theorem VI.

We can readily see that the proof just given is constructive;^45a that is, the following has been proved in an intuitionistically unobjectionable manner: Let an arbitrary recursively defined class κ of FORMULAS be given. Then, if a formal decision (on the basis of κ) of the SENTENTIAL FORMULA 17 Gen r (which [for each κ] can actually be exhibited) is presented to us, we can actually give

1. A PROOF of Neg(17 Gen r);

2. For any given n, a PROOF of

That is, a formal decision of 17 Gen r would have the consequence that we could actually exhibit an ω-inconsistency.

We shall say that a relation between (or a class of) natural numbers is decidable [entscheidungsdefinit] if there exists an n-place RELATION SIGN r such that (3) and (4) (see Theorem V) hold. In particular, therefore, by Theorem V every recursive relation is decidable. Similarly, a RELATION SIGN will be said to be decidable if it corresponds in this way to a decidable relation. Now it suffices for the existence of undecidable propositions that the class κ be ω-consistent and decidable. For the decidability carries over from κ to (see (5) and (6)) and to Q(x, y) (see (8.1)), and only this was used in the proof given above. In this case the undecidable proposition has the form v Gen r, where r is a decidable CLASS SIGN. (Note that it even suffices that κ be decidable in the system enlarged by κ.)

If, instead of assuming that κ is ω-consistent, we assume only that it is consistent, then, although the existence of an undecidable proposition does not follow [by the argument given above], it does follow that there exists a property (r) for which it is possible neither to give a counterexample nor to prove that it holds of all numbers. For in the proof that 17 Gen r is not κ-PROVABLE only the consistency of κ was used (see p. 608). Moreover from it follows by (15) that, for every number is κ-PROVABLE and consequently that is not κ-PROVABLE for any number.

If we adjoin Neg(17 Gen r) to κ, we obtain a class of FORMULAS κ′ that is consistent but not ω-consistent. κ′ is consistent, since otherwise 17 Gen r would be κ-PROVABLE. However, κ′ is not ω-consistent, because, by and (15), and, a fortiori, hold, while on the other hand, of course, holds.⁴⁶

We have a special case of Theorem VI when the class κ consists of a finite number of FORMULAS (and, if we so desire, of those resulting from them by TYPE ELEVATION). 610 Every finite class κ is, of course, recursive.^46a Let a be the greatest number contained in κ. Then we have for κ

Hence κ is recursive. This allows us to conclude, for example, that, even with the help of the axiom of choice (for all types) or the generalized continuum hypothesis, not all propositions are decidable, provided these hypotheses are ω-consistent.

In the proof of Theorem VI no properties of the system P were used besides the following:

1. The class of axioms and the rules of inference (that is, the relation "immediate consequence") are recursively definable (as soon as we replace the primitive signs in some way by natural numbers);

2. Every recursive relation is definable (in the sense of Theorem V) in the system P.

Therefore, in every formal system that satisfies the assumptions 1 and 2 and is ω-consistent there are undecidable propositions of the form (x)F(x), where F is a recursively defined property of natural numbers, and likewise in every extension of such a system by a recursively definable ω-consistent class of axioms. As can easily be verified, included among the systems satisfying the assumptions 1 and 2 are the Zermelo-Fraenkel and the von Neumann axiom systems of set theory,⁴⁷ as well as the axiom system of number theory consisting of the Peano axioms, recursive definition (by schema (2)), and the rules of logic.⁴⁸ Assumption 1 is satisfied by any system that has the usual rules of inference and whose axioms (like those of P) result from a finite number of schemata by substitution.^48a

3

We shall now deduce some consequences from Theorem VI, and to this end we give the following definition:

A relation (class) is said to be arithmetic if it can be defined in terms of the notions + and (addition and multiplication for natural numbers)⁴⁹ and the logical constants (x), and =, where (x) and = apply to natural numbers only.⁵⁰ The notion "arithmetic proposition" is defined accordingly. The relations "greater than" and "congruent modulo n", for example, are arithmetic because we have

611

We now have

Theorem VII. Every recursive relation is arithmetic.

We shall prove the following version of this theorem: every relation of the form where φ is recursive, is arithmetic, and we shall use induction on the degree of φ.Let φ be of degree s Then we have either

1. ⁵¹

(where ρ and all x₁ are of degrees less than s) or

2.

(where ψ and μ are of degrees less than s).

In the first case we have

where R and S_i are the arithmetic relations, existing by the induction hypothesis, that are equivalent to and respectively. Hence in this case is arithmetic.

In the second case we use the following method. We can express the relation with the help of the notion "sequence of numbers" (f)⁵² in the following way:

If and are the arithmetic relations, existing by the induction hypothesis, that are equivalent to and respectively, then

We now replace the notion "sequence of numbers" by "pair of numbers", assigning to the number pair n, d the number sequence where [n]_p denotes the least nonnegative remainder of n modulo p.

We then have

Lemma 1. If f is any sequence of natural numbers and k any natural number, there exists a pair of natural numbers, n, d such that f^{(n, d)} and f agree in the first k terms.

Proof. Let l be the maximum of the numbers k, Let us determine an n such that

which is possible, since any two of the numbers 612 are relatively prime. For a prime number contained in two of these numbers would also be contained in the difference and therefore, since in l!; but this is impossible. The number pair n, l! then has the desired property.

Since the relation is defined by

and is therefore arithmetic, the relation defined as follows:

is also arithmetic. But by (17) and Lemma 1 it is equivalent to (the sequence f enters in (17) only through its first terms). Theorem VII is thus proved.

By Theorem VII, for every problem of the form (x)F(x) (with recursive F) there is an equivalent arithmetic problem. Moreover, since the entire proof of Theorem VII (for every particular F) can be formalized in the system P, this equivalence is provable in P. Hence we have

Theorem VIII. In any of the formal systems mentioned in Theorem VI⁵³there are undecidable arithmetic propositions.

By the remark on page 610, the same holds for the axiom system of set theory and its extensions by ω-consistent recursive classes of axioms.

Finally, we derive the following result:

Theorem IX. In any of the formal systems mentioned in Theorem VI⁵³there are undecidable problems of the restricted functional calculus⁵⁴ (that is, formulas of the restricted functional calculus for which neither validity nor the existence of a counterexample is provable).⁵⁵

This is a consequence of

Theorem X. Every problem of the form (x)F(x) (with recursive F) can be reduced to the question whether a certain formula of the restricted functional calculus is satisfiable (that is, for every recursive F we can find a formula of the restricted functional calculus that is satisfiable if and only if (x)F(x) is true.

By formulas of the restricted functional calculus (r. f. c.) we understand expressions formed from the primitive signs (individual variables), F(x), G(x, y), H(x, y, z), . . . (predicate and relation variables), where (x) and = apply to individuals only.⁵⁶ To these signs we add a third kind of variables, φ(x), ψ(x, y), 613 κ(x, y, z), and so on, which stand for object-functions[Gegenstandsfunktionen] (that is, φ(x), ψ(x, y), and so on denote single-valued functions whose arguments and values are individuals).⁵⁷ A formula that contains variables of the third kind in addition to the signs of the r. f. c. first mentioned will be called a formula in the extended sense (i. e. s.).⁵⁸ The notions "satisfiable" and "valid" carry over immediately to formulas i. e. s., and we have the theorem that, for any formula A i. e. s., we can find a formula B of the r. f. c. proper such that A is satisfiable if and only if B is. We obtain B from A by replacing the variables of the third kind, φ(x), ψ(x, y), . . ., that occur in A with expressions of the form by eliminating the "descriptive" functions by the method used in PM (I, *14), and by logically multiplying⁵⁹ the formula thus obtained by an expression stating about each F, G, . . . put in place of some φ, ψ, . . . that it holds for a unique value of the first argument [for any choice of values for the other arguments].

We now show that, for every problem of the form (x)F(x) (with recursive F), there is an equivalent problem concerning the satisfiability of a formula i. e. s., so that, on account of the remark just made, Theorem X follows.

Since F is recursive, there is a recursive function Φ(x) such that and for Φ there is sequence of functions, such that and for every we have either

or

or

We then form the propositions

In all of the formulas (18), (19), (20) (for ) and in (21) and (22) we now replace the functions Φ_i by function variables φ_i and the number 0 by an 614 individual variable x₀ not used so far, and we form the conjunction C of all the formulas thus obtained.

The formula (Ex₀)C then has the required property, that is,

1. If holds, (Ex₀)C is satisfiable. For the functions obviously yield a true proposition when substituted for in (Ex₀)C);

2. If (Ex₀)C is satisfiable, holds.

Proof. Let be the functions (which exist by assumption) that yield a true proposition when substituted for in (Ex₀)C. Let be their domain of individuals. Since (Ex₀)C holds for the functions ψ_i, there is an individual a (in ) such that all of the formulas (18)–(22) go over into true propositions, (18′)–(22′), when the Φ_i are replaced by the ψ_i and 0 by a. We now form the smallest subclass of that contains a and is closed under the operation ψ₁(x). This subclass has the property that every function ψ_i, when applied to elements of again yields elements of For this holds of ψ₁ by the definition of and by (18′), (19′), and (20′) it carries over from ψ_i with smaller subscripts to ψ_i with larger ones. The functions that result from the when these are restricted to the domain of individuals will be denoted by All of the formulas (18)–(22) hold for these functions also (when we replace 0 by a and Φ_i by

Because (21) holds for and a, we can map the individuals of one-to-one onto the natural numbers in such a manner that a goes over into 0 and the function into the successor function Φ₁. But by this mapping the functions go over into the functions Φ_i, and, since (22) holds for and a, that is, holds, which was to be proved.⁶¹

Since (for each particular F) the argument leading to Theorem X can be carried out in the system P, it follows that any proposition of the form (x)F(x) (with recursive F) can in P be proved equivalent to the proposition that states about the corresponding formula of the r. f. c. that it is satisfiable. Hence the undecidability of one implies that of the other, which proves Theorem IX.⁶²

4

The results of Section 2 have a surprising consequence concerning a consistency proof for the system P (and its extensions), which can be stated as follows:

Theorem XI. Let κ be any recursive consistent⁶³class of FORMULAS; then the SENTENTIAL FORMULA stating that κ is consistent is not κ-PROVABLE; in particular, the consistency of P is not provable in P,⁶⁴ provided P is consistent (in the opposite case, of course, every proposition is provable [in P]).

The proof (briefly outlined) is as follows. Let κ be some recursive class of FORMULAS chosen once and for all for the following discussion (in the simplest case it is the 615 empty class). As appears from 1, page 608, only the consistency of κ was used in proving that 17 Gen r is not κ-PROVABLE;⁶⁵ that is, we have

that is, by (6.1),

By (13), we have

hence

that is, by (8.1),

We now observe the following: all notions defined (or statements proved) in Section 2,⁶⁶ and in Section 4 up to this point, are also expressible (or provable) in P. For throughout we have used only the methods of definition and proof that are customary in classical mathematics, as they are formalized in the system P. In particular, κ (like every recursive class) is definable in P. Let w be the SENTENTIAL FORMULA by which Wid(κ) is expressed in P. According to (8.1), (9), and (10), the relation Q(x, y) is expressed by the RELATION SIGN q, hence Q(x, p) by r (since, by (12), and the proposition (x)Q(x p) by 17 Gen r.

Therefore, by (24), w Imp (17 Gen r) is provable in P⁶⁷ (and a fortiori κ-PROVABLE). If now w were κ-PROVABLE, then 17 Gen r would also be κ-PROVABLE, and from this it would follow, by (23), that κ is not consistent.

Let us observe that this proof, too, is constructive; that is, it allows us to actually derive a contradiction from κ, once a PROOF of w from κ is given. The entire proof of Theorem XI carries over word for word to the axiom system of set theory, M, and to that of classical mathematics,⁶⁸A, and here, too, it yields the result: There is no consistency proof for M, or for A, that could be formalized in M, or A, respectively, provided M, or A, is consistent. I wish to note expressly that Theorem XI (and the corresponding results for M and A) do not contradict Hilbert’s formalistic viewpoint. For this viewpoint presupposes only the existence of a consistency proof in which nothing but finitary means of proof is used, and it is conceivable that there exist finitary proofs that cannot be expressed in the formalism of P (or of M or A).

Since, for any consistent class κ, w is not κ-PROVABLE, there always are propositions (namely w) that are undecidable (on the basis of κ) as soon as Neg(w) is not κ-PROVABLE; in other words, we can, in Theorem VI, replace the assumption of ω-consistency by the following: The proposition "κ is inconsistent" is not κ-PROVABLE. (Note that there are consistent κ for which this proposition is κ-PROVABLE.)

616

In the present paper we have on the whole restricted ourselves to the system P, and we have only indicated the applications to other systems. The results will be stated and proved in full generality in a sequel to be published soon.^68a In that paper, also, the proof of Theorem XI, only sketched here, will be given in detail.

Note added 28 August 1963. In consequence of later advances, in particular of the fact that due to A. M. Turing’s work⁶⁹ a precise and unquestionably adequate definition of the general notion of formal system⁷⁰ can now be given, a completely general version of Theorems VI and XI is now possible. That is, it can be proved rigorously that in every consistent formal system that contains a certain amount of finitary number theory there exist undecidable arithmetic propositions and that, moreover, the consistency of any such system cannot be proved in the system.

ON COMPLETENESS AND CONSISTENCY

KURT GöDEL n/a

(1931a)

Let Z be the formal system that we obtain by supplementing the Peano axioms with the schema of definition by recursion (on one variable) and the logical rules of the restricted functional calculus. Hence Z is to contain no variables other than variables for individuals (that is, natural numbers), and the principle of mathematical induction must therefore be formulated as a rule of inference. Then the following hold:

1. Given any formal system S in which there are finitely many axioms and in which the sole principles of inference are the rule of substitution and the rule of implication, if S contains¹Z, S is incomplete, that is, there are in S propositions (in 617 particular, propositions of Z) that are undecidable on the basis of the axioms of S, provided that S is ω-consistent. Here a system is said to be ω-consistent if, for no property F of natural numbers, as well as all the formulas are provable.

2. In particular, in every system S of the kind just mentioned the proposition that S is consistent (more precisely, the equivalent arithmetic proposition that we obtain by mapping the formulas one-to-one on natural numbers) is unprovable.

Theorems 1 and 2 hold also for systems in which there are infinitely many axioms and in which there are other principles of inference than those mentioned above, provided that when we enumerate the formulas (in order of increasing length and, for equal length, in lexicographical order) the class of numbers assigned to the axioms is definable and decidable [entscheidungsdefinit] in the system Z, and that the same holds of the following relation between natural numbers: "the formula with number x₁ follows from the formulas with numbers by a single application of one of the rules of inference". Here a relation (class) is said to be decidable in Z if for every n-tuple of natural numbers either or is provable in Z. (At present no decidable number-theoretic relation is known that is not definable and decidable already in Z.)

If we imagine that the system Z is successively enlarged by the introduction of variables for classes of numbers, classes of classes of numbers, and so forth, together with the corresponding comprehension axioms, we obtain a sequence (continuable into the transfinite) of formal systems that satisfy the assumptions mentioned above, and it turns out that the consistency (ω-consistency) of any of those systems is provable in all subsequent systems. Also, the undecidable propositions constructed for the proof of Theorem 1 become decidable by the adjunction of higher types and the corresponding axioms; however, in the higher systems we can construct other undecidable propositions by the same procedure, and so forth. To be sure, all the propositions thus constructed are expressible in Z (hence are number-theoretic propositions); they are, however, not decidable in Z, but only in higher systems, for example, in that of analysis. In case we adopt a type-free construction of mathematics, as is done in the axiom system of set theory, axioms of cardinality (that is, axioms postulating the existence of sets of ever higher cardinality) take the place of the type extensions, and it follows that certain arithmetic propositions that are undecidable in Z become decidable by axioms of cardinality, for example, by the axiom that there exist sets whose cardinality is greater than every α_n, where

¹ With the axiom of reducibility or without ramified theory of types.

² Furthermore, S contains formulas of the restricted functional calculus such that neither universal validity nor existence of a counterexample is provable for any of them.

³ This result, in particular, holds also for the axiom system of classical mathematics, as it has been constructed, for example, by von Neumann (1927).

¹ See a summary of the results of the present paper in Gödel 1930b.

²Whitehead and Russell 1925. Among the axioms of the system PM we include also the axiom of infinity (in this version: there are exactly denumerably many individuals), the axiom of reducibility, and the axiom of choice (for all types).

³ See Fraenkel 1927 and von Neumann 1925, 1928, and 1929. We note that in order to complete the formalization we must add the axioms and rules of inference of the calculus of logic to the set-theoretic axioms given in the literature cited. The considerations that follow apply also to the formal systems (so far as they are available at present) constructed in recent years by Hilbert and his collaborators. See Hilbert 1922, 1922a, 1927, Bernays 1923, von Neumann 1927, and Ackermann 1924.

⁴ That is, more precisely, there are undecidable propositions in which, besides the logical constants (not), (or), (x) (for all), and = (identical with), no other notions occur but + (addition) and (multiplication), both for natural numbers, and in which the prefixes (x), too, apply to natural numbers only.

⁵ In PM only axioms that do not result from one another by mere change of type are counted as distinct.

⁶ Here and in what follows we always understand by "formula of PM" a formula written without abbreviations (that is, without the use of definitions). It is well known that [in PM] definitions serve only to abbreviate notations and therefore are dispensable in principle.

⁷ That is, we map the primitive signs one-to-one onto some natural numbers. (See how this is done on page 601.)

⁸ That is, a number-theoretic function defined on an initial segment of the natural numbers. (Numbers, of course, cannot be arranged in a spatial order.)

⁹ In other words, the procedure described above yields an isomorphic image of the system PM in the domain of arithmetic, and all metamathematical arguments can just as well be carried out in this isomorphic image. This is what we do below when we sketch the proof; that is, by "formula", "proposition", "variable", and so on, we must always understand the corresponding objects of the isomorphic image.

¹⁰ It would be very easy (although somewhat cumbersome) to actually write down this formula.

¹¹ For example, by increasing sum of the finite sequence of integers that is the "class sign", and lexicographically for equal sums.

^11a The bar denotes negation.

¹² Again, there is not the slightest difficulty in actually writing down the formula S.

¹³ Note that "[R(q); q]" (or, which means the same, "[S; q]") is merely a metamathematical description of the undecidable proposition. But, as soon as the formula S has been obtained, we can, of course, also determine the number q and, therewith, actually write down the undecidable proposition itself. [This makes no difficulty in principle. However, in order not to run into formulas of entirely unmanageable lengths and to avoid practical difficulties in the computation of the number q, the construction of the undecidable proposition would have to be slightly modified, unless the technique of abbreviation by definition used throughout in PM is adopted.]

^13a [The German text reads which is a misprint.]

¹⁴ Any epistemological antinomy could be used for a similar proof of the existence of un-decidable propositions.

¹⁵ Contrary to appearances, such a proposition involves no faulty circularity, for initially it [only] asserts that a certain well-defined formula (namely, the one obtained from the qth formula in the lexicographic order by a certain substitution) is unprovable. Only subsequently (and so to speak by chance) does it turn out that this formula is precisely the one by which the proposition itself was expressed.

¹⁶ The addition of the Peano axioms, as well as all other modifications introduced in the system PM, merely serves to simplify the proof and is dispensable in principle.

¹⁷ It is assumed that we have denumerably many signs at our disposal for each type of variables.

¹⁸ Nonhomogeneous relations, too, can be defined in this manner; for example, a relation between individuals and classes can be defined to be a class of elements of the form ((x₂), ((x₁), x₂)). Every proposition about relations that is provable in PM is provable also when treated in this manner, as is readily seen.

¹⁹ Concerning this definition (and similar definitions occurring below) see Lukasiewicz and Tarski 1930.

^18a Hence xΠ(a) is a formula even if x does not occur in a or is not free in a. In this case, of course, xΠ(a) means the same thing as a.

²⁰ In case v does not occur in a as a free variable we put Subst Note that "Subst" is a metamathematical sign.

²¹ is to be regarded as defined by as in PM (I, *13) similarly for higher types).

²² In order to obtain the axioms from the schemata listed we must therefore

(1) Eliminate the abbreviations and

(2) Add the omitted parentheses

(in II, III, and IV after carrying out the substitutions allowed).

Note that all expressions thus obtained are "formulas" in the sense specified above. (See also the exact definitions of the metamathematical notions on pp. 603–606.)

²³ Therefore c is a variable or 0 or a sign of the form f . . . fu, where u is either 0 or a variable of type 1, Concerning the notion "free (bound) at a place in a", see I A 5 in von Neumann 1927.

²⁴ The rule of substitution is rendered superfluous by the fact that all possible substitutions have already been carried out in the axioms themselves. (This procedure was used also by von Neumann 1927.)

²⁵ That is, its domain of definition is the class of nonnegative integers (or of n-tuples of nonnegative integers) and its values are nonnegative integers.

²⁶ In what follows, lower-case italic letters (with or without subscripts) are always variables for nonnegative integers (unless the contrary is expressly noted).

²⁷ More precisely, by substitution of some of the preceding functions at the argument places of one of the preceding functions, for example, Not all variables on the left side need occur on the right side (the same applies to the recursion schema (2)).

²⁸ We include classes among relations (as one-place relations). Recursive relations R, of course, have the property that for every given n-tuple of numbers it can be decided whether holds or not.

²⁹ Whenever formulas are used to express a meaning (in particular, in all formulas expressing metamathematical propositions or notions), Hilbert’s symbolism is employed. See Hilbert and Ackermann 1928.

³⁰ We use German letters, as abbreviations for arbitrary n-tuples of variables, for example,

³¹ We assume familiarity with the fact that the functions (addition) and (multi-plication) are recursive.

³²a cannot take values other than 0 and 1, as can be seen from the definition of α.

³³ The sign ≡ is used in the sense of "equality by definition"; hence in definitions it stands for either = or ~ (otherwise, the symbolism is Hilbert’s).

³⁴ Wherever one of the signs (x), (Ex), or εx occurs in the definitions below, it is followed by a bound on x. This bound merely serves to ensure that the notion defined is recursive (see Theorem IV). But in most cases the extension of the notion defined would not change if this bound were omitted.

^34a For where z is the number of distinct prime factors of x. Note that for

^34b stands for & (similarly for more than two variables).

³⁵ That provides a bound can be seen thus: The length of the shortest sequence of formulas that corresponds to x can at most be equal to the number of subformulas of x. But there are at most l(x) subformulas of length 1, at most of length 2, and so on, hence altogether at most Therefore all prime factors of n can be assumed to be less than Pr([l(x)]²), their number and their exponents (which are subformulas of x)

³⁶ In case v is not a VARIABLE or x is not a FORMULA,

³⁷ Instead of we write (and similarly for more than two VARIABLES).

³⁸ The VARIABLES can be chosen arbitrarily. For example, there always is an r with the FREE VARIABLES 17, 19, 23, . . ., and so on, for which (3) and (4) hold.

³⁹ Theorem V, of course, is a consequence of the fact that in the case of a recursive relation R it can, for every n-tuple of numbers, be decided on the basis of the axioms of the system P whether the relation R obtains or not.

⁴⁰ From this it follows at once that the theorem holds for every recursive relation, since any such relation is equivalent to where φ is recursive.

⁴¹ When this proof is carried out in detail, r, of course, is not defined indirectly with the help of its meaning but in terms of its purely formal structure.

⁴² Which, therefore, in the usual interpretation expresses the fact that this relation holds.

⁴³ Since r is obtained from the recursive RELATION SIGN q through the replacement of a VARIABLE by a definite number, p. [Precisely stated the final part of this footnote (which refers to a side remark unnecessary for the proof) would read thus: "REPLACEMENT of a VARIABLE by the NUMERAL for p."]

⁴⁴ The operations Gen and Sb, of course, can always be interchanged in case they refer to different VARIABLES.

⁴⁵ By "x is κ-provable" we mean xε Flg(κ), which, by (7), means the same thing as

^45a Since all existential statements occurring in the proof are based upon Theorem V, which, as is easily seen, is unobjectionable from the intuitionistic point of view.

⁴⁶ Of course, the existence of classes κ that are consistent but not ω-consistent is thus proved only on the assumption that there exists some consistent κ (that is, that P is consistent).

^46a [On page 190, lines 21, 22, and 23, of the German text the three occurrences of α are misprints and should be replaced by occurrences of κ.]

⁴⁷ The proof of assumption 1 turns out to be even simpler here them for the system P, since there is just one kind of primitive variables (or two in von Neumann’ system).

⁴⁸ See Problem III in Hilbert 1928a.

^48a As will be shown in Part II of this paper, the true reason for the incompleteness inherent in all formal systems of mathematics is that the formation of ever higher types cart be continued into the transfinite (see Hilbert 1925, p. 184 [above, p. 387]), while in any formal system at most denumerably many of them are available. For it can be shown that the undecidable propositions constructed here become decidable whenever appropriate higher types are added (for example, the type ω to the system P). An analogous situation prevails for the axiom system of set theory.

⁴⁹ Here and in what follows, zero is always included among the natural numbers.

⁵⁰ The definiens of such a notion, therefore, must consist exclusively of the signs listed, variables for natural numbers, x, y, . . ., and the signs 0 and 1 (variables for functions and sets ore not permitted to occur). Instead of x any other number variable, of course, may occur in the prefixes.

⁵¹ Of course, not all need occur in the χ₁ (see the example in footnote 27).

⁵²f here is a variable with the [infinite] sequences of natural numbers as its domain of values. f_k denotes the term of a sequence f (f₀ denoting the first).

⁵³ These are the ω-consistent systems that result from P when recursively definable classes of axioms are added.

⁵⁴ See Hilbert and Ackermann 1928.

In the system P we must understand by formulas of the restricted functional calculus those that result from the formulas of the restricted functional calculus of PM when relations are replaced by classes of higher types as indicated on page 599.

⁵⁵ In 1930a I showed that every formula of the restricted functional calculus either can be proved to be valid or has a counterexample. However, by Theorem IX the existence of this counterexample is not always provable (in the formal systems we have been considering).

⁵⁶ Hilbert and Ackermann (1928) do not include the sign = in the restricted functional calculus. But for every formula in which the sign = occurs there exists a formula that does not contain this sign and is satisfiable if and only if the original formula is (see Gödel 1930a).

⁵⁷ Moreover, the domain of definition is always supposed to be the entire domain of individuals.

⁵⁸ Variables of the third kind may occur at all argument places occupied by individual variables, for example, and the like.

⁵⁹ That is, by forming the conjunction.

^59a [The last clause of footnote 27 was not taken into account in the formulas (18). But an explicit formulation of the cases with fewer variables on the right side is actually necessary here for the formal correctness of the proof, unless the identity function, is added to the initial functions.]

⁶⁰ The stand for finite sequences of the variables for example, x₁, x₃, x₂.

⁶¹ Theorem X implies, for example, that Fermat’s problem and Goldbach’s problem could be solved if the decision problem for the r. f. c. were solved.

⁶² Theorem IX, of course, also holds for the axiom system of set theory and for its extensions by recursively definable ω-consistent classes of axioms, since there are undecidable propositions of the form (x)F(x) (with recursive F) in these systems too.

⁶³ "κ is consistent" (abbreviated by "Wid(κ)") is defined thus:

⁶⁴ This follows if we substitute the empty class of FORMULAS for κ.

⁶⁵ Of course, r (like p) depends on κ.

⁶⁶ From the definition of "recursive" on page 602 to the proof of Theorem VI inclusive.

⁶⁷ That the truth of w Imp (17 Gen r) can be inferred from (23) is simply due to the fact that the undecidable proposition 17 Gen r asserts its own unprovability, as was noted at the very beginning.

⁶⁸ See von Neumann 1927.

^68a [This explains the "I" in the title of the paper. The author’s intention was to publish this sequel in the next volume of the Monatshefte. The prompt acceptance of his results was one of the reasons that made him change his plan.]

⁶⁹ See Turing 1937, p. 249.

⁷⁰ In my opinion the term "formal system" or "formalism" should never be used for anything but this notion. In a lecture at Princeton (mentioned in Princeton University 1946, p. 11 [see Davis 1965, pp. 84–88]) I suggested certain transfinite generalizations of formalisms, but these are something radically different from formal systems in the proper sense of the term, whose characteristic property is that reasoning in them, in principle, can be completely replaced by mechanical devices.

¹ That a formal system S contains another formal system T means that every proposition expressible (provable) in T is expressible (provable) also in S.

[Remark by the author, 18 May 1966:]

[This definition is not precise, and, if made precise in the straightforward manner, it does not yield a sufficient condition for the nondemonstrability in S of the consistency of S. A sufficient condition is obtained if one uses the following definition: "S contains T if and only if every meaningful formula (or axiom or rule (of inference, of definition, or of construction of axioms)) of T is a meaningful formula (or axiom, and so forth) of S, that is, if S is an extension of T".

Under the weaker hypothesis that Z is recursively one-to-one translatable into S, with demonstrability preserved in this direction, the consistency, even of very strong systems S, may be provable in S and even in primitive recursive number theory. However, what can be shown to be unprovable in S is the fact that the rules of the equational calculus applied to equations, between primitive recursive terms, demonstrable in S yield only correct numerical equations (provided that S possesses the property that is asserted to be unprovable). Note that it is necessary to prove this "outer" consistency of S (which for the usual systems is trivially equivalent with consistency) in order to "justify", in the sense of Hilbert’s program, the transfinite axioms of a system S. ("Rules of the equational calculus" in the foregoing means the two rules of substituting primitive recursive terms for variables and substituting one such term for another to which it has been proved equal.)

The last-mentioned theorem and Theorem 1 of the paper remain valid for much weaker systems than Z, in particular for primitive recursive number theory, that is, what remains of Z if quantifiers are omitted. With insignificant changes in the wording of the conclusions of the two theorems they even hold for any recursive translation into S of the equations between primitive recursive terms, under the sole hypothesis of ω-consistency (or outer consistency) of S in this translation.]