Posted by on April 05, 2001 at 08:56:23 AM EDT:
In Reply to: Réponse à Jules G posted by Occam on March 25, 2001 at 12:01:41 PM EST:
[173]
ON FORMALLY UNDECIDABLE PROPOSITIONS
OF PRINCIPIA MATHEMATICA AND RELATED
SYSTEMS 11
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 numbers4 which[174]
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 pn (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 2n1, 3n2 … pknk correspond to the series n1, n2, … nk, where pk 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(a1,a2,…an) of basic signs or series of such. We assign to it that class (or relation) R'(x1,x2,…xn) of natural numbers, which holds for x1, x2, … xn when and only when there exist a1, a2, … an such that xi=F(ai) (i=1,2,…n) and R(a1,a2,…an) 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: ((x2),((x1),x2)). 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(x1…xn) 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. x1, x2 … xn.
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 Si 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 ($x0)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. fk denotes the k+1-th term of a series f (f0 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.