[173]
by Kurt Gödel, Vienna
1
The development of mathematics in the direction of greater exactness has–as is well known–led to large tracts of it becoming formalized, so that proofs can be carried out according to a few mechanical rules. The most comprehensive formal systems yet set up are, on the one hand, the system of Principia Mathematica (PM)^{2} and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann).^{3} These two systems are so extensive that all methods of proof used in mathematics today have been formalized in them, i.e. reduced to a few axioms and rules of inference. It may therefore be surmised that these axioms and rules of inference are also sufficient to decide all mathematical questions which can in any way at all be expressed formally in the systems concerned. It is shown below that this is not the case, and that in both the systems mentioned there are in fact relatively simple problems in the theory of ordinary whole numbers^{4} which
n Î K º ~(Bew [R(n); n])^{11a} (1)
(where
S = R(q)
holds for some determinate natural number q. We now show that the
proposition
^{1} Cf. the summary of the results of this work, published in Anzeiger der Akad. d. Wiss. in Wien (math.-naturw. Kl.) 1930, No. 19.
^{2} A. Whitehead and B. Russell, Principia Mathematica, 2nd edition, Cambridge 1925. In particular, we also reckon among the axioms of PM the axiom of infinity (in the form: there exist denumerably many individuals), and the axioms of reducibility and of choice (for all types).
^{3} Cf. A. Fraenkel, 'Zehn Vorlesungen über die Grundlegung der Mengenlehre', Wissensch. u. Hyp., Vol. XXXI; J. v. Neumann, 'Die Axiomatisierung der Mengenlehre', Math. Zeitschr. 27, 1928, Journ. f. reine u. angew. Math. 154 (1925), 160 (1929). We may note that in order to complete the formalization, the axioms and rules of inference of the logical calculus must be added to the axioms of set-theory given in the above-mentioned papers. The remarks that follow also apply to the formal systems presented in recent years by D. Hilbert and his colleagues (so far as these have yet been published). Cf. D. Hilbert, Math. Ann. 88, Abh. aus d. math. Sem. der Univ. Hamburg I (1922), VI (1928); P. Bernays, Math. Ann. 90; J. v. Neumann, Math. Zeitsehr. 26 (1927); W. Ackermann, Math. Ann. 93.
^{4} I.e., more precisely, there are undecidable propositions in which, besides the logical constants ~ (not), Ú (or), (x) (for all) and = (identical with), there are no other concepts beyond + (addition) and . (multiplication), both referred to natural numbers, and where the prefixes (x) can also refer only to natural numbers.
^{5} In this connection, only such axioms in PM are counted as distinct as do not arise from each other purely by change of type.
^{6} Here and in what follows, we shall always understand the term "formula of PM" to mean a formula written without abbreviations (i.e. without use of definitions). Definitions serve only to abridge the written text and are therefore in principle superfluous.
^{7} I.e. we map the basic signs in one-to-one fashion on the natural numbers (as is actually done on [179]).
^{8} I.e. a covering of a section of the number series by natural numbers. (Numbers cannot in fact be put into a spatial order.)
^{9} In other words, the above-described procedure provides an isomorphic image of the system PM in the domain of arithmetic, and all metamathematical arguments can equally well be conducted in this isomorphic image. This occurs in the following outline proof, i.e. "formula", "proposition", "variable", etc. are always to be understood as the corresponding objects of the isomorphic image.
^{10} It would be very simple (though rather laborious) actually to write out this formula.
^{11} Perhaps according to the increasing sums of their terms and, for equal sums, in alphabetical order.
^{11a} The bar-sign indicates negation. [Replaced with ~.]
^{12} Again there is not the slightest difficulty in actually writing out the formula S.
^{13} Note that
^{14} Every epistemological antinomy can likewise be used for a similar undecidability proof.
^{15} In spite of appearances, there is nothing circular about such a proposition, since it begins by asserting the unprovability of a wholly determinate formula (namely the q-th in the alphabetical arrangement with a definite substitution), and only subsequently (and in some way by accident) does it emerge that this formula is precisely that by which the proposition was itself expressed.
2
and so on for every natural number as type.^{17}
a, ¦a, ¦¦a, ¦¦¦a … etc.
where a is either 0 or a variable of first type. In the former case we call such a
sign a number-sign. For
I.
III. Every formula derived from the two schemata
by making the following substitutions for a, v, b, c (and carrying out in I the operation denoted by "Subst"): for a any given formula, for v any variable, for b any formula in which v does not appear free, for c a sign of the same type as v, provided that c contains no variable which is bound in a at a place where v is free.^{23}
IV. Every formula derived from the schema
on substituting for v or u any variables of types n or n + 1 respectively, and for a a formula which does not contain u free. This axiom represents the axiom of reducibility (the axiom of comprehension of set theory).
V. Every formula derived from the following by type-lift (and this formula itself):
Furthermore, variables of type n are given numbers of the form p^{n} (where p is a prime number > 13). Hence, to every finite series of basic signs (and so also to every formula) there corresponds, one-to-one, a finite series of natural numbers. These finite series of natural numbers we now map (again in one-to-one correspondence) on to natural numbers, by letting the number 2^{n1}, 3^{n2} … p_{k}^{nk} correspond to the series n_{1}, n_{2}, … n_{k}, where p_{k} denotes the k-th prime number in order of magnitude. A natural number is thereby assigned in one-to-one correspondence, not only to every basic sign, but also to every finite series of such signs. We denote by F(a) the number corresponding to the basic sign or series of basic signs a. Suppose now one is given a class or relation R(a_{1},a_{2},…a_{n}) of basic signs or series of such. We assign to it that class (or relation) R'(x_{1},x_{2},…x_{n}) of natural numbers, which holds for x_{1}, x_{2}, … x_{n} when and only when there exist a_{1}, a_{2}, … a_{n} such that x_{i}=F(a_{i}) (i=1,2,…n) and R(a_{1},a_{2},…a_{n}) holds. We represent by the same words in italics those classes and relations of natural numbers which have been assigned in this fashion to such previously defined metamathematical concepts as "variable", "formula", "propositional formula", "axiom", "provable formula", etc. The proposition that there are undecidable problems in the system P would therefore read, for example, as follows: There exist propositional formulae a such that neither a nor the negation of a are provable formulae.
I. Every function (or relation) derived from recursive functions (or relations) by the substitution of recursive functions in place of variables is recursive; so also is every function derived from recursive functions by recursive definition according to schema (2).
II. If R and S are recursive relations, then so
also are ~R,
III. If the functions f(c)
and y(h) are
recursive, so also is the relation:
IV. If the function f(c) and the relation R(x,h) are recursive, so also then are the relations S, T
and likewise the function y
where
namely
are recursive. The proof of Proposition IV is briefly as follows: According to the assumption there exists a recursive r(x,h) such that
where
The relation T can be reduced by negation to a case analogous to S, so that Proposition IV is proved.
1.
2.
3.
4.
5.
6.
7.
8.
9.
10.
11.
12.
13.
14.
15.
16.
17.
18.
19.
20.
21.
22.
23.
24.
25.
26.
27.
28.
29.
30.
31.
32.
33.
34.
35.
36.
37.
38.
39.
40.
41.
42.
43.
44.
45.
46.
where v is the free variable of the class-sign a.
(cf. the analogous concept 44)
The following clearly hold:
We now define the relation:
We put
(p is a class-sign with the free variable 19)
and
(r is a recursive class-sign with the free variable 17).^{43}
Then
[because of (11) and (12)] and furthermore:
[according to (12)]. If now in (9) and (10) we substitute p for y, we find, in virtue of (13) and (14):
Hence:
while–on the other hand–from the c-provability of
^{16} The addition of the Peano axioms, like all the other changes made in the system PM, serves only to simplify the proof and can in principle be dispensed with.
^{17} It is presupposed that for every variable type denumerably many signs are available.
^{18} Unhomogeneous relations could also be defined in this manner, e.g. a relation between individuals and classes as a class of elements of the form: ((x_{2}),((x_{1}),x_{2})). As a simple consideration shows, all the provable propositions about relations in PM are also provable in this fashion.
^{18a} Thus
^{19} With regard to this definition (and others like it occurring later), cf. J. Lukasiewicz and A. Tarski, 'Untersuchungen über den Aussagenkalkül', Comptes Rendus des séances de la Soeiété des Sciences et des Lettres de Varsovie XXIII, 1930, Cl. 111.
^{20} Where v does not occur in a as a free
variable, we must put
^{21} As in PM I, *13,
^{22} To obtain the axioms from the schemata presented
(and in the cases of II, III and IV, after carrying out the permitted substitutions),
one must therefore still
^{23} c is therefore either a variable or 0 or a sign of the form ¦ … ¦_{u} where u is either 0 or a variable of type 1. With regard to the concept "free (bound) at a place in a" cf. section I A5 of the work cited in footnote 24.
^{24} The rule of substitution becomes superfluous, since we have already dealt with all possible substitutions in the axioms themselves (as is also done in J. v. Neumann, 'Zur Hilbertschen Beweistheorie', Math. Zeitschr. 26, 1927).
^{25} I.e. its field of definition is the class of non-negative whole numbers (or n-tuples of such), respectively, and its values are non-negative whole numbers.
^{26} In what follows, small italic letters (with or without indices) are always variables for non-negative whole numbers (failing an express statement to the contrary). [Italics omitted.]
^{27} More precisely, by substitution of certain of the
foregoing functions in the empty places of the preceding, e.g.
^{28} We include classes among relations (one-place relations). Recursive relations R naturally have the property that for every specific n-tuple of numbers it can be decided whether R(x_{1}…x_{n}) holds or not.
^{29} For all considerations as to content (more especially also of a metamathematical kind) the Hilbertian symbolism is used, cf. Hilbert-Ackermann, Grundzüge der theoretischen Logik, Berlin 1928.
^{30} We use [greek] letters c, h, as abbreviations for given n-tuple sets of variables, e.g. x_{1}, x_{2} … x_{n}.
^{31} We take it to be recognized that the functions x+y (addition) and x.y (multiplication) are recursive.
^{32} a cannot take values other than 0 and 1, as is evident from the definition of a.
^{33} The sign º is used to mean "equivalence by definition", and therefore does duty in definitions either for = or for ~ [not the negation symbol] (otherwise the symbolism is Hilbertian).
^{34} Wherever in the following definitions one of the signs (x), ($x), ex occurs, it is followed by a limitation on the value of x. This limitation merely serves to ensure the recursive nature of the concept defined. (Cf. Proposition IV.) On the other hand, the range of the defined concept would almost always remain unaffected by its omission.
^{34a} For
^{34b}
^{35} The limitation
^{36} Where v is not a variable or x
not a formula, then
^{37} Instead of
^{38} The variables
^{39} Proposition V naturally is based on the fact that for any recursive relation R, it is decidable, for every n-tuple of numbers, from the axioms of the system P, whether the relation R holds or not.
^{40} From this there follows immediately its validity
for every recursive relation, since any such relation is equivalent to
^{41} In the precise development of this proof, r is naturally defined, not by the roundabout route of indicating its content, but by its purely formal constitution.
^{42} Which thus, as regards content, expresses the existence of this relation.
^{43} r is derived in fact, from the recursive relation-sign q on replacement of a variable by a determinate number (p).
^{44} The operations Gen and Sb are naturally always commutative, wherever they refer to different variables.
^{45} "x is c-provable" signifies:
^{45a} Since all existential assertions occurring in the proof are based on Proposition V, which, as can easily be seen, is intuitionistically unobjectionable.
^{46} Thus the existence of consistent and not w-consistent c's can naturally be proved only on the assumption that, in general, consistent c's do exist (i.e. that P is consistent).
^{47} The proof of assumption 1 is here even simpler than that for the system P, since there is only one kind of basic variable (or two for J. v. Neumann).
^{48} Cf. Problem III in D. Hilbert's lecture: 'Probleme der Grundlegung der Mathematik', Math. Ann. 102.
^{48a} The true source of the incompleteness attaching to all formal systems of mathematics, is to be found–as will be shown in Part II of this essay–in the fact that the formation of ever higher types can be continued into the transfinite (cf. D. Hilbert 'Über das Unendliche', Math. Ann. 95, p. 184), whereas in every formal system at most denumerably many types occur. It can be shown, that is, that the undecidable propositions here presented always become decidable by the adjunction of suitable higher types (e.g. of type w for the system P). A similar result also holds for the axiom system of set theory.
3
where R and S_{i} are respectively the arithmetical
relations which by the inductive assumption exist, equivalent to
If
the following then holds:
We now replace the concept "series of numbers" by "pair of
numbers", by assigning to the number pair n, d the number series
which is possible, since every two of the numbers 1+(i+1)l!
which, according to (17) and Lemma 1, is
equivalent to
1.
or
2.
or
3.
1. If
2. If ($x_{0})C is satisfiable, then
^{49} Here, and in what follows, zero is always included among the natural numbers.
^{50} The definiens of such a concept must therefore be constructed solely by means of the signs stated, variables for natural numbers x,y… and the signs 0 and 1 (function and set variables must not occur). (Any other number-variable may naturally occur in to prefixes in place of x.)
^{51} It is not of course necessary that all
^{52} f signifies here a variable, whose domain of values consists of series of natural numbers. f_{k} denotes the k+1-th term of a series f (f_{0} being the first).
^{53} These are the w-consistent systems derived from P by addition of a recursively definable class of axioms.
^{54} Cf. Hilbert-Ackermann, Grundzüge der theoretischen Logik. In the system P, formulae of the restricted predicate calculus are to be understood as those derived from the formulae of the restricted predicate calculus of PM on replacement of relations by classes of higher type, as indicated on [176].
^{55} In my article 'Die Vollständigkeit der Axiome des logischen Funktionenkalküls', Monatsh. f. Math. u. Phys. XXXVII, 2, I have shown of every formula of the restricted predicate calculus that it is either demonstrable as universally valid or else that a counter-example exists; but in virtue of Proposition IX the existence of this counter-example is not always demonstrable (in the formal systems in question).
^{56} D. Hilbert and W. Ackermann, in the work already cited, do not include the sign = in the restricted predicate calculus. But for every formula in which the sign = occurs, there exists a formula without this sign, which is satisfiable simultaneously with the original one (cf. the article cited in footnote 55).
^{57} And of course the domain of the definition must always be the whole domain of individuals.
^{58} Variables of the third kind may therefore occur at
all empty places instead of individual variables, e.g.
^{59} I.e. forming the conjunction.
^{60}
^{61} From Proposition X it follows, for example, that the Fermat and Goldbach problems would be soluble, if one had solved the decision problem for the r.p.c.
^{62} Proposition IX naturally
holds also for the axiom system of set theory and its extensions by recursively
definable w-consistent classes of axioms, since in these
systems also there certainly exist undecidable theorems of the form
4
i.e. by (6.1):
i.e. by (8.1):
^{63} C is consistent (abbreviated as Wid(c))
is defined as follows:
^{64} This follows if c is replaced by the null class of formulae.
^{65} r naturally depends on c (just as p does).
^{66} From the definition of "recursive" on [179] up to the proof of Proposition VI inclusive.
^{67} That the correctness of
^{68} Cf. J. v. Neumann, 'Zur Hilbertschen Beweistheorie', Math. Zeitschr. 26, 1927.
(Received: 17. xi. 1930.)
Design © 1998 Siegfried. All rights reserved.