Le mémoire de 1930 de Kurt Gödel où l'on peut lire de sa main "the undecidable proposition 17 Gen r asserts its own unprovability" (troisième ligne avant la fin du mémoire, note 67). La proposition 17 Gen r est non c-prouvable. Proposition, vétilleux, sournois et prétentieux imbécile. Pas théorème. Internet est encore mieux que le livre de poche.

[ Follow Ups ] [ Post Followup ] [ debord of directors ] [ FAQ ]

Posted by on April 05, 2001 at 09:02:08 AM EDT:

In Reply to: Bavard macaronique : tu essayes de noyer le poisson. posted by on April 04, 2001 at 04:40:33 PM EDT:

[173]

ON FORMALLY UNDECIDABLE PROPOSITIONS
OF PRINCIPIA MATHEMATICA AND RELATED
SYSTEMS 1¹

by Kurt Gödel, Vienna

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)² and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann).³ 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⁴ which

[174]

⁵

Before going into details, we shall first indicate the main lines of the proof, naturally without laying claim to exactness. The formulae of a formal system–we restrict ourselves here to the system PM–are, looked at from outside, finite series of basic signs (variables, logical constants and brackets or separation points), and it is easy to state precisely just which series of basic signs are meaningful formulae and which are not.⁶ Proofs, from the formal standpoint, are likewise nothing but finite series of formulae (with certain specifiable characteristics). For metamathematical purposes it is naturally immaterial what objects are taken as basic signs, and we propose to use natural numbers⁷ for them. Accordingly, then, a formula is a finite series of natural numbers,⁸ and a particular proof-schema is a finite series of finite series of natural numbers. Metamathematical concepts and propositions thereby become concepts and propositions concerning natural numbers, or series of them,⁹ and therefore at least partially expressible in the symbols of the system PM itself. In particular, it can be shown that the concepts, "formula", "proof-schema", "provable formula" are definable in the system PM, i.e. one can give¹⁰ a formula F(v) of PM–for example–with one free variable v (of the type of a series of numbers), such that F(v)–interpreted as to content–states: v is a provable formula. We now obtain an undecidable proposition of the system PM, i.e. a proposition A, for which neither A nor not-A are provable, in the following manner:

[175]

A formula of PM with just one free variable, and that of the type of the natural numbers (class of classes), we shall designate a class-sign. We think of the class-signs as being somehow arranged in a series,¹¹ and denote the n-th one by R(n); and we note that the concept "class-sign" as well as the ordering relation R are definable in the system PM. Let a be any class-sign; by [a; n] we designate that formula which is derived on replacing the free variable in the class-sign a by the sign for the natural number n. The three-term relation x = [y; z] also proves to be definable in PM. We now define a class K of natural numbers, as follows:

n Î K º ~(Bew [R(n); n])^11a (1)

(where Bew x means: x is a provable formula). Since the concepts which appear in the definiens are all definable in PM, so too is the concept K which is constituted from them, i.e. there is a class-sign S,¹² such that the formula [S; n]–interpreted as to its content–states that the natural number n belongs to K. S, being a class-sign, is identical with some determinate R(q), i.e.

S = R(q)

holds for some determinate natural number q. We now show that the proposition [R(q); q]¹³ is undecidable in PM. For supposing the proposition [R(q); q] were provable, it would also be correct; but that means, as has been said, that q would belong to K, i.e. according to (1), ~(Bew [R(q); q]) would hold good, in contradiction to our initial assumption. If, on the contrary, the negation of [R(q); q] were provable, then ~(n Î K), i.e. Bew [R(q); q] would hold good. [R(q); q] would thus be provable at the same time as its negation, which again is impossible.

The analogy between this result and Richard's antinomy leaps to the eye; there is also a close relationship with the "liar" antinomy,¹⁴ since the undecidable proposition [R(q); q] states precisely that q belongs to K, i.e. according to (1), that [R(q); q] is not provable. We are therefore confronted with a proposition which asserts its own unprovability.¹⁵ The method of proof just exhibited can clearly

[176]

From the remark that [R(q); q] asserts its own unprovability, it follows at once that [R(q); q] is correct, since [R(q); q] is certainly unprovable (because undecidable). So the proposition which is undecidable in the system PM yet turns out to be decided by metamathematical considerations. The close analysis of this remarkable circumstance leads to surprising results concerning proofs of consistency of formal systems, which are dealt with in more detail in Section 4 (Proposition XI).

¹ Cf. the summary of the results of this work, published in Anzeiger der Akad. d. Wiss. in Wien (math.-naturw. Kl.) 1930, No. 19.

² 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).

³ 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.

⁴ 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.

⁵ In this connection, only such axioms in PM are counted as distinct as do not arise from each other purely by change of type.

⁶ 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.

⁷ I.e. we map the basic signs in one-to-one fashion on the natural numbers (as is actually done on [179]).

⁸ I.e. a covering of a section of the number series by natural numbers. (Numbers cannot in fact be put into a spatial order.)

⁹ 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.

¹⁰ It would be very simple (though rather laborious) actually to write out this formula.

¹¹ Perhaps according to the increasing sums of their terms and, for equal sums, in alphabetical order.

^11a The bar-sign indicates negation. [Replaced with ~.]

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

¹³ Note that "[R(q); q]" (or–what comes to the same thing–"[S; q]") is merely a metamathematical description of the undecidable proposition. But as soon as one has ascertained the formula S, one can naturally also determine the number q, and thereby effectively write out the undecidable proposition itself.

¹⁴ Every epistemological antinomy can likewise be used for a similar undecidability proof.

¹⁵ 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.

We proceed now to the rigorous development of the proof sketched above, and begin by giving an exact description of the formal system P, for which we seek to demonstrate the existence of undecidable propositions. P is essentially the system obtained by superimposing on the Peano axioms the logic of PM¹⁶ (numbers as individuals, relation of successor as undefined basic concept).

The basic signs of the system P are the following:

I. Constants: "~" (not), "Ú" (or), """ (for all), "0" (nought), "¦" (the successor of), "(", ")" (brackets).

II. Variables of first type (for individuals, i.e. natural numbers including 0): "x₁", "y₁", "z₁", …

Variables of second type (for classes of individuals): "x₂", "y₂", "z₂", …

Variables of third type (for classes of classes of individuals): "x₃", "y₃", "z₃", …

and so on for every natural number as type.¹⁷

Note: Variables for two-termed and many-termed functions (relations) are superfluous as basic signs, since relations can be defined as classes of ordered pairs and ordered pairs again as classes of classes, e.g. the ordered pair a,b by ((a),(a,b)), where (x,y) means the class whose only elements are x and y, and (x) the class whose only element is x.¹⁸

[177]

By a sign of first type we understand a combination of signs of the form:

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 n > 1 we understand by a sign of n-th type the same as variable of n-th type. Combinations of signs of the form a(b), where b is a sign of n-th and a a sign of (n+1)-th type, we call elementary formulae. The class of formulae we define as the smallest class¹⁹ containing all elementary formulae and, also, along with any a and b the following: ~(a), (a)Ú(b), x"(a) (where x is any given variable).^18a We term (a)Ú(b) the disjunction of a and b, ~(a) the negation and (a)Ú(b) a generalization of a. A formula in which there is no free variable is called a propositional formula (free variable being defined in the usual way). A formula with just n free individual variables (and otherwise no free variables) we call an n-place relation-sign and for n = 1 also a class-sign.

By Subst a(v|b) (where a stands for a formula, v a variable and b a sign of the same type as v) we understand the formula derived from a, when we replace v in it, wherever it is free, by b.²⁰ We say that a formula a is a type-lift of another one b, if a derives from b, when we increase by the same amount the type of all variables appearing in b.

The following formulae (I-V) are called axioms (they are set out with the help of the customarily defined abbreviations: ., É, º, ($x), =,²¹ and subject to the usual conventions about omission of brackets)²²:

~(¦x₁ = 0)

¦x₁ = ¦y₁ É x₁ = y₁

x₂(0).x₁ " (x₂(x₁) É x₂(fx₁)) É x₁ " (x₂(x₁))

[178]

II.

p Ú p É p

p É p Ú q

p Ú q É q Ú p

(p É q) É (r Ú p É r Ú q)

III. Every formula derived from the two schemata

v " (a) Ú Subst a(v|c)

v " (b É a) Ú b É v " (a)

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.²³

IV. Every formula derived from the schema

($u)(v " (u(v) º a))

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):

x₁ " (x₂(x₁) º y₂(x₁)) Ú x₂ = y₂.

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 a is the formula (~(b)) Ú (c), and an immediate consequenee of a, if c is the formula v " (a), where v denotes any given variable. The class of provable formulae is defined as the smallest class of formulae which contains the axioms and is closed with respect to the relation "immediate consequence of".²⁴

The basic signs of the system P are now ordered in one-to-one correspondence with natural numbers, as follows:

[179]

(

)

Furthermore, variables of type n are given numbers of the form pⁿ (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^n₁, 3^n₂ … p_k^n_k correspond to the series n₁, n₂, … 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₁,a₂,…a_n) of basic signs or series of such. We assign to it that class (or relation) R'(x₁,x₂,…x_n) of natural numbers, which holds for x₁, x₂, … x_n when and only when there exist a₁, a₂, … a_n such that x_i=F(a_i) (i=1,2,…n) and R(a₁,a₂,…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.

We now introduce a parenthetic consideration having no immediate connection with the formal system P, and first put forward the following definition: A number-theoretic function²⁵ f(x₁,x₂,…x_n) is said to be recursively defined by the number-theoretic functions y(x₁,x₂,…x_n-1) and m(x₁,x₂,…x_n+1), if for all x₂, … x_n, k²⁶ the following hold:

f(0,x₂,…x_n) = y(x₂,…x_n)
f(k+1,x₂,…x_n) = m(k,f(k,x₂,…x_n),x₂,…x_n). (2)

A number-theoretic function f is called recursive, if there exists a finite series of number-theoretic functions f₁, f₂, … f_n which ends in f and has the property that every function f_k of the series is either recursively defined

[180]

²⁷

x+1

f_i

degree

R(x₁,x₂,…x_n)

²⁸

f(x₁,x₂,…x_n)

x₁

x₂

x_n

R(x₁,x₂,…x_n) º [f(x₁,x₂,…x_n) = 0]²⁹.

The following propositions hold:

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, R Ú S (and therefore also R & S).

III. If the functions f(c) and y(h) are recursive, so also is the relation: f(c) = y(h).³⁰

IV. If the function f(c) and the relation R(x,h) are recursive, so also then are the relations S, T

S(c,h) ~ ($x)[x £ f(c) & R(x,h)]

T(c,h) ~ (x)[x £ f(c) ® R(x,h)]

and likewise the function y

y(c,h) = ex [x £ f(c) & R(x,h)]

where ex F(x) means: the smallest number x for which F(x) holds and 0 if there is no such number.

Proposition I follows immediately from the definition of "recursive". Propositions II and III are based on the readily ascertainable fact that the number-theoretic functions corresponding to the logical concepts ~, Ú, =

a(x), b(x,y), g(x,y)

namely

a(0) = 1; a(x) = 0 for x ¹ 0

b(0,x) = b(x,0) = 0; b(x,y) = 1, if x, y both ¹ O

[181]

g(x,y) = 0, if x = y; g(x,y) = 1, if x ¹ y

are recursive. The proof of Proposition IV is briefly as follows: According to the assumption there exists a recursive r(x,h) such that

R(x,h) º [r(x,h) = 0].

We now define, according to the recursion schema (2), a function C(x,h) in the following manner:

C(0,h) = 0

C(n+1,h) = (n+1).a + C(n,h).a(a)³¹

where

a = a[a(r(0,h))].a[r(n+1,h)].a[C(n,h)].

C(n+1,h) is therefore either = n+1 (if a = 1) or = C(n,h) (if a = 0).³² The first case clearly arises if and only if all the constituent factors of a are 1, i.e. if

~R(O,h) & R(n+1,h) & [C(n,h) = 0].

From this it follows that the function C(n,h) (considered as a function of n) remains 0 up to the smallest value of n for which R(n,h) holds, and from then on is equal to this value (if R(0,h) is already the case, the corresponding C(x,h) is constant and = 0). Therefore:

y(c,h) = C(f(c),h)

S(c,h) º R[y(c,h)),h)]

The relation T can be reduced by negation to a case analogous to S, so that Proposition IV is proved.

The functions x+y, x.y, x^y, and also the relations x ‹ y, x = y are readily found to be recursive; starting from these concepts, we now define a series of functions (and relations) 1-45, of which each is defined from the earlier ones by means of the operations named in Propositions I to IV. This procedure, generally speaking, puts together many of the definition steps permitted by Propositions I to IV. Each of the functions (relations) 1-45, containing, for example, the concepts "formula", "axiom", and "immediate consequence", is therefore recursive.

[182]

x/y º ($z)[z £ x & x = y.z]³³

³⁴

Prim(x) º ~($z)[z £ x & z ¹ 1 & z ¹ x & x/z] & x > 1

0 Pr x º 0

(n+1) Pr x º ey [y £ x & Prim(y) & x/y & y > n Pr x]

n Pr x

^34a

0! º 1

(n+1)! º (n+1).n!

Pr(0) º 0

Pr(n+1) º ey [y £ {Pr(n)}! + 1 & Prim(y) & y > Pr(n)]

Pr(n)

n Gl x º ey [y £ x & x/(n Pr x)^y & not x/(n Pr x)^y+1]

n Gl x

n > 0

l(x) º ey [y £ x & y Pr x > 0 & (y+1) Pr x = 0]

l(x)

x * y º ez [z £ [Pr{l(x)+l(y)}]^x+y & (n)[n £ l(x) ® n Gl z = n Gl x] & (n)[0 < n £ l(y) ® {n+l(x)} Gl z = n Gl y]]

x * y

R(x) º 2^x

R(x)

x > 0

10.

E(x) º R(11) * x * R(13)

E(x)

(

)

11.

n Var x º ($z)[13 < z £ x & Prim(z) & x = zⁿ] & n ¹ 0

variable of

-th type

12.

Var(x) º ($n)[n £ x & n Var x]

variable

13.

Neg(x) º R(5) * E(x)

Neg(x)

negation

[183]

14.

x Dis y º E(x) * R(7) * E(y)

x Dis y

disjunction

15.

x Gen y º R(x) * R(9) * E(y)

x Gen y

is the generalization of y by means of the variable x (assuming x is a variable).

16.

0 N x º x

(n+1) N x º R(3) * n N x

n N x

17.

Z(n) º n N [R(1)]

Z(n)

number-sign

18.

Typ₁'(x) º ($m,n){m,n £ x & [m = 1 Ú 1 Var m] & x = n N [R(m)]}^34b

sign of first type

19.

Typ_n(x) º [n = 1 & Typ₁'(x)] Ú [n > 1 & ($v){v £ x & n Var v & x = R(v)}]

sign of

-th type

20.

Elf(x) º ($y,z,n)[y,z,n £ x & Typ_n(y) & Typ_n+1(z) & x = z * E(y)]

elementary formula

21.

Op(x,y,z) º x = Neg(y) Ú x = y Dis z Ú ($v)[v £ x & Var(v) & x = v Gen y]

22.

FR(x) º (n){0 < n £ l(x) ® Elf(n Gl x) Ú ($p,q)[0 < p,q < n & Op(n Gl x,p Gl x,q Gl x)]} & l(x) > 0

formulae

elementary formula

negation

disjunction

generalization

23.

Form(x) º ($n){n £ (Pr[l(x)²])^x.[l(x)]² & FR(n) & x = [l(n)] Gl n}³⁵

formula

series of formulae

)

24.

v Geb n,x º Var(v) & Form(x) & ($a,b,c)[a,b,c £ x & x = a * (v Gen b) * c & Form(b) & l(a)+1 £ n £ l(a)+l(v Gen b)]

variable

bound

[184]

25.

v Fr n,x º Var(v) & Form(x) & v = n Gl x & n £ l(x) & not(v Geb n,x)

variable

free

26.

v Fr x º ($n)[n £ l(x) & v Fr n,x]

free variable

27.

Su x(n|y) º ez {z £ [Pr(l(x)+l(y))]^x+y & [($u,v)u,v £ x & x = u * R(b Gl x) * v & z = u * y * v & n = l(u)+1]}

Su x(n|y)

0 < n £ l(x)).

28.

0 St v,x º en {n £ l(x) & v Fr n,x & not ($p)[n < p £ l(x) & v Fr p,x]}

(k+1) St v,x º en {n < k St v,x & v Fr n,x & ($p)[n < p < k St v,x & v Fr p,x]}

k St v,x

(k+1)

formula

29.

A(v,x) º en {n £ l(x) & n St v = 0}

A(v,x)

free

30.

Sb₀(x v|y) º x

Sb_k+1(x v|y) º Su[Sb_k(x v|y)][(k St v, x)|y)]

31.

Sb(x v|y) º Sb_A(v,x)(x v|y)

³⁶

Sb(x v|y)

Subst a(v|b),

³⁷

32.

x Imp y º [Neg(x)] Dis y

x Con y º Neg{[Neg(x)] Dis [Neg(y)]}

x Aeq y º (x Imp y) Con (y Imp x)

v Ex y º Neg{v Gen [Neg(y)]}

33.

n Th x º en {y £ x^(xⁿ) & (k) £ l(x) ® (k Gl x £ 13 & k Gl y = k Gl x) Ú (k Gl x > 13 & k Gl y = k Gl x.[1 Pr(k Gl x)]ⁿ)]}

n Th x

type-lift

n Th x

formulae

To the axioms I, 1 to 3, there correspond three determinate numbers, which we denote by z₁, z₂, z₃, and we define:

34.

Z–Ax(x) º (x = z₁ Ú x = z₂ Ú x = z₃)

[185]

35.

A₁-Ax(x) º ($y)[y £ x & Form(y) & x = (y Dis y) Imp y]

formula

axiom-schema II, 1

A₂-Ax

A₃-Ax

A₄-Ax

36.

A-Ax(x) º A₁-Ax(x) Ú A₂-Ax(x) Ú A₃-Ax(x) Ú A₄-Ax(x)

formula

37.

Q(z,y,v) º ($n,m,w)[n £ l(y) & m £ l(z) & w £ z & w = m Gl x & w Geb n,y & v Fr n,y]

variable bound

free

38.

L₁-Ax(x) º ($v,y,z,n){v,y,z,n £ x & n Var v & Typ_n(z) & Form(y) & Q(z,y,v) & x = (v Gen y) Imp [Sb(v|z)]}

formula

axiom-schema III, 1

39.

L₂-Ax(x) º ($v,q,p){v,q,p £ x & Var(v) & Form(p) & v Fr p & Form(q) & x = [v Gen (p Dis q)] Imp [p Dis (v Gen q)]}

formula

axiom-schema III, 2

40.

R-Ax(x) º ($u,v,y,n)[u, v, y, n £ x & n Var v & (n+1) Var u & u Fr y & Form(y) & x = u $x {v Gen [[R(u)*E(R(v))] Aeq y]}]

formula

axiom-schema IV, 1

To the axiom V, 1 there corresponds a determinate number z₄ and we define:

41.

M-Ax(x) º ($n)[n £ x & x = n Th z₄]

42.

Ax(x) º Z-Ax(x) Ú A-Ax(x) Ú L₁-Ax(x) Ú L₂-Ax(x) Ú R-Ax(x) Ú M-Ax(x)

axiom

43.

Fl(x y z) º y = z Imp x Ú ($v)[v £ x & Var(v) & x = v Gen y]

immediate consequence

[186]

44.

Bw(x) º (n){0 < n £ l(x) ® Ax(n Gl x) Ú ($p,q)[0 < p,q < n & Fl(n Gl x, p Gl x, q Cl x)]} & l(x) > 0

proof-schema

formulae

axiom

immediate consequence

45.

x B y º Bw(x) & [l(x)] Gl x = y

proof

formula

46.

Bew(x) = (Ey)y B x

provable formula

Bew(x)

The following proposition is an exact expression of a fact which can be vaguely formulated in this way: every recursive relation is definable in the system P (interpreted as to content), regardless of what interpretation is given to the formulae of P:

Proposition V: To every recursive relation R(x₁ … x_n) there corresponds an n-place relation-sign r (with the free variables³⁸ u₁, u₂, … u_n) such that for every n-tuple of numbers (x₁ … x_n) the following hold:

R(x₁ … x_n) ® Bew{Sb[r (u₁ … u_n)|(Z(x₁) … Z(x_n)]} (3)

~R(x₁ … x_n) ® Bew{Neg Sb[r (u₁ … u_n)|(Z(x₁) … Z(x_n)]} (4)

We content ourselves here with indicating the proof of this proposition in outline, since it offers no difficulties of principle and is somewhat involved.³⁹ We prove the proposition for all relations R(x₁ … x_n) of the form: x₁ = f(x₂ … x_n)⁴⁰ (where f is a recursive function) and apply mathematical induction on the degree of f. For functions of the first degree (i.e. constants and the function x+1) the proposition is trivial. Let f then be of degree m. It derives from functions of lower degree f₁ … f_k by the operations of substitution or recursive definition. Since, by the inductive assumption, everything is already proved for f₁ … f_k, there exist corresponding relation-signs r₁ … r_k such that (3) and (4) hold. The processes of definition whereby f is derived from f₁ … f_k (substitution and re-

[187]

r₁ … r_k

relation-sign

⁴¹

relation-sign

⁴²

We now come to the object of our exercises:
Let c be any class of formulae. We denote by Flg(c) (set of consequences of c) the smallest set of formulae which contains all the formulae of c and all axioms, and which is closed with respect to the relation "immediate consequence of". c is termed w-consistent, if there is no class-sign a such that:

(n)[Sb(a v|Z(n)) Î Flg(c)] & [Neg(v Gen a)] Î Flg(c)

where v is the free variable of the class-sign a.

Every w-consistent system is naturally also consistent. The converse, however, is not the case, as will be shown later.

The general result as to the existence of undecidable propositions reads:

Proposition VI: To every w-consistent recursive class c of formulae there correspond recursive class-signs r, such that neither v Gen r nor Neg (v Gen r) belongs to Flg(c) (where v is the free variable of r).

Proof: Let c be any given recursive w-consistent class of formulae. We define:

Bw_c(x) º (n)[n £ l(x) ® Ax(n Gl x) Ú (n Gl x) Î c Ú (Ep,q){0 < p,q < n & Fl(n Gl x, p Gl x, q Gl x)}] & l(x) > 0 (5)

(cf. the analogous concept 44)

x B_c y º Bw_c(x) & [l(x)] Gl x = y (6)

Bew_c(x) º ($y)y B_c x (6.1)

(cf. the analogous concepts 45, 46)

The following clearly hold:

(x)[Bew_c(x) º x Î Flg(c)] (7)

(x)[Bew(x) ® Bew_c(x)] (8)

[188]

We now define the relation:

Q(x,y) º ~{x B_c[Sb(y 19|z(y))]}. (8.1)

Since x B_c y [according to (6), (5)] and Sb(y 19|Z(y)) (according to definitions 17, 31) are recursive, so also is Q(x,y). According to Proposition V and (8) there is therefore a relation-sign q (with the free variables 17, 19) such that

~{x B_c [Sb(y 19|Z(y))]} ® Bew_c[Sb(q 17|Z(x) 19|Z(y))]. (9)

x B_c [Sb(y 19|Z(y))] ® Bew_c[Neg Sb(q 17|Z(x) 19|Z(y))]. (10)

We put

p = 17 Gen q (11)
(p is a class-sign with the free variable 19)

and

r = Sb(q 19|Z(p)) (12)
(r is a recursive class-sign with the free variable 17).⁴³

Then

Sb(p 19|Z(p)) (13)

= Sb ([17 Gen q] 19|z(p))

= 17 Gen Sb(q 19|z(p))

= 17 Gen r⁴⁴

[because of (11) and (12)] and furthermore:

Sb(q 17|Z(x) 19|Z(p)) = Sb(r 17|Z(x)) (14)

[according to (12)]. If now in (9) and (10) we substitute p for y, we find, in virtue of (13) and (14):

x B_c (17 Gen r) ® Bew_c[Sb(r 17|Z(x))] (15)

x B_c (17 Gen r) ® Bew_c[Neg Sb(r 17|Z(x))] (16)

[189]

Hence:

1. 17 Gen r is not c-provable.⁴⁵ For if that were so, there would (according to 6.1) be an n such that n B_c (17 Gen r). By (16) it would therefore be the case that:

Bew_c[Neg Sb(r 17|Z(n))]

while–on the other hand–from the c-provability of 17 Gen r there follows also that of Sb(r 17|Z(n)). c would therefore be inconsistent (and, a fortiori, w-inconsistent).

2. Neg(17 Gen r) is not c-provable. Proof: As shown above, 17 Gen r is not c-provable, i.e. (according to 6.1) the following holds: (n) n B_c(17 Gen r). Whence it follows, by (15), that (n) Bew_c[Sb(r 17|Z(n))], which together with Bew_c[Neg(17 Gen r)] would conflict with the w-consistency of c.

Neg(17 Gen r) is therefore undecidable in c, so that Proposition VI is proved.

One can easily convince oneself that the above proof is constructive,^45a i.e. that the following is demonstrated in an intuitionistically unobjectionable way: Given any recursively defined class c of formulae: If then a formal decision (in c) be given for the (effectively demonstrable) propositional formula 17 Gen r, we can effectively state:

1. A proof for Neg(17 Gen r).

2. For any given n, a proof for Sb(r 17|Z(n)), i.e. a formal decision of 17 Gen r would lead to the effective demonstrability of an w-inconsistency.

We shall call a relation (class) of natural numbers R(x₁ … x_n) calculable [entscheidungsdefinit], if there is an n-place relation-sign r such that (3) and (4) hold (cf. Proposition V). In particular, therefore, by Proposition V, every recursive relation is calculable. Similarly, a relation-sign will be called calculable, if it be assigned in this manner to a calculable relation. It is, then, sufficient for the existence of undecidable propositions, to assume of the class c that it is w-consistent and calculable. For the property of being calculable carries over from c to x B_c y (cf. (5), (6))

[190]

Q(x,y)

8.1

v Gen r,

class-sign

If, instead of w-consistency, mere consistency as such is assumed for c, then there follows, indeed, not the existence of an undecidable proposition, but rather the existence of a property (r) for which it is possible neither to provide a counter-example nor to prove that it holds for all numbers. For, in proving that 17 Gen r is not c-provable, only the consistency of c is employed (cf. [189]) and from ~Bew_c(17 Gen r) it follows, according to (15), that for every number x, Sb(r 17|z(x)) is c-provable, and hence that Sb(r 17|Z(x)) is not c-provable for any number.

By adding Neg(17 Gen r) to c, we obtain a consistent but not w-consistent class of formulae c'. c' is consistent, since otherwise 17 Gen r would be c-provable. c' is not however w-consistent, since in virtue of ~Bew_c(17 Gen r) and (15) we have: (x) Bew_cSb(r 17|Z(x)), and so a fortiori: (x) Bew_c'Sb(r 17|Z(x)), and on the other hand, naturally: Bew_c'[Neg(17 Gen r)].⁴⁶

A special case of Proposition VI is that in which the class c consists of a finite number of formulae (with or without those derived therefrom by type-lift). Every finite class a is naturally recursive. Let a be the largest number contained in a. Then in this case the following holds for c:

x Î c º ($m,n)[m £ x & n £ a & n Î a & x = m Th n]

c is therefore recursive. This allows one, for example, to conclude that even with the help of the axiom of choice (for all types), or the generalized continuum hypothesis, not all propositions are decidable, it being assumed that these hypotheses are w-consistent.

In the proof of Proposition VI the only properties of the system P employed were the following:

1. The class of axioms and the rules of inference (i.e. the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers).

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

Hence in every formal system that satisfies assumptions 1 and 2 and is w-consistent, undecidable propositions exist of the form (x) F(x), where F is a recursively defined property of natural numbers, and so too in every extension of such

[191]

⁴⁷

⁴⁸

^48a

¹⁶ 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.

¹⁷ It is presupposed that for every variable type denumerably many signs are available.

¹⁸ 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₂),((x₁),x₂)). As a simple consideration shows, all the provable propositions about relations in PM are also provable in this fashion.

^18a Thus x " (a) is also a formula if x does not occur, or does not occur free, in a. In that case x " (a) naturally means the same as a.

¹⁹ 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.

²⁰ Where v does not occur in a as a free variable, we must put Subst a(v|b) = a. Note that "Subst" is a sign belonging to metamathematics.

²¹ As in PM I, *13, x₁ = y₁ is to be thought of as defined by x₂ " (x₂(x₁) É x₂(y₁)) (and similarly for higher types.)

²² 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

Note that the resultant expressions must be "formulae" in the above sense. (Cf. also the exact definitions of the metamathematical concepts on [182]ff.)

²³ 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.

²⁴ 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).

²⁵ 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.

²⁶ 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.]

²⁷ More precisely, by substitution of certain of the foregoing functions in the empty places of the preceding, e.g. f_k(x₁,x₂) = f_p[f_q(x₁,x₁),f_r(x₂)] (p, q, r ‹ k). Not all the variables on the left-hand side must also occur on the right (and similarly in the recursion schema (2)).

²⁸ 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₁…x_n) holds or not.

²⁹ 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.

³⁰ We use [greek] letters c, h, as abbreviations for given n-tuple sets of variables, e.g. x₁, x₂ … x_n.

³¹ We take it to be recognized that the functions x+y (addition) and x.y (multiplication) are recursive.

³² a cannot take values other than 0 and 1, as is evident from the definition of a.

³³ 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).

³⁴ 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 0 < n £ z, where z is the number of distinct prime numbers dividing into x. Note that for n = z+1, n Pr x = 0.

^34b m,n £ x stands for: m £ x & n £ x (and similarly for more than two variables).

³⁵ The limitation n £ (Pr[l(x)]²^x.[l(x)]² means roughly this: The length of the shortest series of formulae belonging to x can at most be equal to the number of constituent formulae of x. There are however at most l(x) constituent formulae of length 1, at most l(x)-1 of length 2, etc. and in all, therefore, at most ¹¤₂[l(x){l(x)+1}] £ [l(x)]². The prime numbers in n can therefore all be assumed smaller that Pr{[l(x)]²}, their number £[l(x)]² and their exponents (which are constituent formulae of x) £x.

³⁶ Where v is not a variable or x not a formula, then Sb(x v|y) = x.

³⁷ Instead of Sb[Sb[x v|y] z|y] we write: Sb(x v|y w|z) (and similarly for more than two variables).

³⁸ The variables u₁ … u_n could be arbitrarily allotted. There is always, e.g., an r with the free variables 17, 19, 23 … etc., for which (3) and (4) hold.

³⁹ 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.

⁴⁰ From this there follows immediately its validity for every recursive relation, since any such relation is equivalent to 0 = f(x₁ … x_n), where f is recursive.

⁴¹ 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.

⁴² Which thus, as regards content, expresses the existence of this relation.

⁴³ r is derived in fact, from the recursive relation-sign q on replacement of a variable by a determinate number (p).

⁴⁴ The operations Gen and Sb are naturally always commutative, wherever they refer to different variables.

⁴⁵ "x is c-provable" signifies: x Î Flg(c), which, by (7), states the same as Bew_c(x).

^45a Since all existential assertions occurring in the proof are based on Proposition V, which, as can easily be seen, is intuitionistically unobjectionable.

⁴⁶ 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).

⁴⁷ 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).

⁴⁸ 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.

From Proposition VI we now obtain further consequences and for this purpose give the following definition:

A relation (class) is called arithmetical, if it can be defined solely by means of the concepts +, . [addition and multiplication, applied to natural numbers]⁴⁹ and the logical constants Ú, ~, (x), =, where (x) and = are to relate only to natural numbers.⁵⁰ The concept of "arithmetical proposition" is defined in a corresponding way. In particular the relations "greater [than]" and "congruent to a modulus" are arithmetical, since

x > y º ~($z)[y = x+z]
x @ y(mod n) º ($z)[x = y+z.n Ú y = x+z.n]

We now have:

Proposition VII: Every recursive relation is arithmetical.

We prove this proposition in the form: Every relation of the form x₀ = f(x₁ … x_n), where f is recursive, is arithmetical, and apply mathematical induction on the degree of f. Let f be of degree s (s > 1). Then either

[192]

1. f(x₁ … x_n) = r[c₁(x₁ … x_n), c₂(x₁ … x_n) … c_m(x₁ … x_n)]⁵¹

(where p and all the x's have degrees smaller than s) or

2. f(0,x₂ … x_n) = y(x₂ … x_n)

f(k+1,x₂ … x_n) = m[k,f(k,x₂ … x_n),x₂ … x_n]

(where y, m are of lower degree than s).

In the first case we have:

x₀ = f(x₁ … x_n) º ($y₁ … y_m)[R(x₀,y₁ … y_m) & S₁(y₁,x₁ … x_n) & … & S_m(y_m,x₁ … x_n)],

where R and S_i are respectively the arithmetical relations which by the inductive assumption exist, equivalent to x₀ = r(y₁ … y_m) and y = c_i(x₁ … x_n). In this case, therefore, x₀ = f(x₁ … x_n) is arithmetical.

In the second case we apply the following procedure: The relation x₀ = f(x₁ … x_n) can be expressed with the help of the concept "series of numbers" (f)⁵² as follows:

x₀ = f(x₁ … x_n) º ($f){f₀ = y(x₂ … x_n) & (k)[k < x₁ ® f_k+1 = m(k,f_k,x₂ … x_n)] & x₀ = f_x₁}

If S(y,x₂ … x_n) and T(z,x₁ … x_n+1) are respectively the arithmetical relations–which by the inductive assumption exist–equivalent to

y = y(x₂ … x_n) and z = m(x₁ … x_n+1),

the following then holds:

x₀ = f(x₁ … x_n) º ($f){S(f₀,x₂ … x_n) & (k)[k < x₁ ® T(f^k+1,k,f_k,x₂ … x_n)] & x₀ = f_x₁} (17)

We now replace the concept "series of numbers" by "pair of numbers", by assigning to the number pair n, d the number series f^(n,d)(f_k^(n,d) = [n]_1+(k+1)d), where [n]_p denotes the smallest non-negative residue of n modulo p.

We then have the following:

Lemma 1: If f is any series of natural numbers and k any natural number, then 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 largest of the numbers k,f₀,f₁ … f_k-1. Let n be so determined that

n = f_i(mod(1+(i+1)l!)] for i = 0,1 … k-1

[193]

which is possible, since every two of the numbers 1+(i+1)l! (i = 0,1 … k-1) are relatively prime. For a prime number contained in two of these numbers would also be contained in the difference (i₁-i₂)l! and therefore, because |i₁-i₂| < 1, in l!, which is impossible. The number pair n, l! thus accomplishes what is required.

Since the relation x = [n]_p is defined by x = n(mod p) & x < p and is therefore arithmetical, so also is the relation P(x₀,x₁ … x_n) defined as follows:

P(x₀ … x_n) º ($n,d){S([n]_d+1,x₂ … x_n) & (k) [k < x₁ ® T([n]_1+d(k+2),k,[n]_1+d(k+1),x₂ … x_n)] & x₀ = [n]_1+d(x₁+1)}

which, according to (17) and Lemma 1, is equivalent to x₀ = f(x₁ … x_n) (we are concerned with the series f in (17) only in its course up to the x₁+1-th term). Thereby Proposition VII is proved.

According to Proposition VII there corresponds to every problem of the form (x) F(x) (F recursive) an equivalent arithmetical problem, and since the whole proof of Proposition VII can be formalized (for every specific F) within the system P, this equivalence is provable in P. Hence:

Proposition VIII: In every one of the formal systems⁵³ referred to in Proposition VI there are undecidable arithmetical propositions.

The same holds (in virtue of the remarks at the end of Section 3) for the axiom system of set theory and its extensions by w-consistent recursive classes of axioms.

We shall finally demonstrate the following result also:

Proposition IX: In all the formal systems referred to in Proposition VI⁵³ there are undecidable problems of the restricted predicate calculus⁵⁴ (i.e. formulae of the restricted predicate calculus for which neither universal validity nor the existence of a counter-example is provable).⁵⁵

[194]

This is based on

Proposition X: Every problem of the form (x) F(x) (F recursive) can be reduced to the question of the satisfiability of a formula of the restricted predicate calculus (i.e. for every recursive F one can give a formula of the restricted predicate calculus, the satisfiability of which is equivalent to the validity of (x) F(x)).

We regard the restricted predicate calculus (r.p.c.) as consisting of those formulae which are constructed out of the basic signs: ~, Ú, (x), =; x, y … (individual variables) and F(x), G(x,y), H(x,y,z) … (property and relation variables)⁵⁶ where (x) and = may relate only to individuals. To these signs we add yet a third kind of variables f(x), y(x,y), c(x,y,z) etc. which represent object functions; i.e. f(x), y(x,y), etc. denote one-valued functions whose arguments and values are individuals.⁵⁷ A formula which, besides the first mentioned signs of the r.p.c., also contains variables of the third kind, will be called a formula in the wider sense (i.w.s.).⁵⁸ The concepts of "satisfiable" and "universally valid" transfer immediately to formulae i.w.s. and we have the proposition that for every formula i.w.s. A we can give an ordinary formula of the r.p.c. B such that the satisfiability of A is equivalent to that of B. We obtain B from A, by replacing the variables of the third kind f(x), y(x,y) … appearing in A by expressions of the form (^,z)F(z,x), (^,z)G(z,x y), …, by eliminating the "descriptive" functions on the lines of PM I *14, and by logically multiplying⁵⁹ the resultant formula by an expression, which states that all the F, G … substituted for the f, y … are strictly one-valued with respect to the first empty place.

We now show, that for every problem of the form (x) F(x) (F recursive) there is an equivalent concerning the satisfiability of a formula i.w.s., from which Proposition X follows in accordance with what has just been said.

Since F is recursive, there is a recursive function F(x) such that F(x) º [F(x) = 0], and for F there is a series of functions F₁,F₂ … F_n, such that F_n = F, F₁(x) = x+1 and for every F_k(1 < k £ n) either

1. (x₂ … x_m) [F_k(0,x₂ … x_m) = (F_p(x₂ … x_m)]

(x,x₂ … x_m) {F_k[F₁(x),x₂ … x_m] = (F_q[x,F_k(x,x₂ … x_m),x₂ … x_m]} (18)

p,q < k

[195]

2. (x₁ … x_m) [F_k(x₁ … x_m) = F_r(F_i₁(c₁) … f_{i_s}(c_s))]⁶⁰ (19)

r < k, i_v < k (for v = 1, 2 … s)

3. (x₁ … x_m) [F_k(x₁ … x_m) = F₁(F₁ … F₁(0))] (20)

In addition, we form the propositions:

(x) ~[F₁(x) = 0] & (x y) [F₁(x) = F₁(y) ® x = y] (21)

(x) [F_n(x) = 0] (22)

In all the formulae (18), (19), (20) (for k = 2,3, … n) and in (21), (22), we now replace the functions F_i by the function variable f_i, the number 0 by an otherwise absent individual variable x₀ and form the conjunction C of all the formulae so obtained.

The formula ($x₀)C then has the required property, i.e

1. If (x) [F(x) = 0] is the case, then ($x₀)C is satisfiable, since when the functions F₁, F₂ … F_n are substituted for f₁, f₂ … f_n in ($x₀)C they obviously yield a correct proposition.

2. If ($x₀)C is satisfiable, then (x) [F(x) = 0] is the case.

Proof: Let Y₁, Y₂ … Y_n be the functions presumed to exist, which yield a correct proposition when substituted for f₁, f₂ … f_n in ($x₀)C. Let its domain of individuals be I. In view of the correctness of ($x₀)C for all functions Y_i, there is an individual a (in I) such that all the formulae (18) to (22) transform into correct propositions (18') to (22') on replacement of the F_i by Y_i and of 0 by a. We now form the smallest sub-class of I, which contains a and is closed with respect to the operation Y₁(x). This subclass (I') has the property that every one of the functions Y_i, when applied to elements of I', again yields elements of I'. For this holds of Y₁ in virtue of the definition of I'; and by reason of (18'), (19'), (20') this property carries over from Y_i of lower index to those of higher. The functions derived from Y_i by restriction to the domain of individuals I', we shall call Y_i'. For these functions also the formulae (18) to (22) all hold (on replacement of 0 by a and F_i by Y_i').

Owing to the correctness of (21) for Y₁' and a, we can map the individuals of I' in one-to-one correspondence on the natural numbers, and this in such a manner that a transforms into 0 and the function Y₁' into the successor function F₁. But, by this mapping, all the functions Y_i' transform into the functions F_i, and owing to the correct-

[196]

Y_n'

(x) [F_n(x) = 0]

(x) [F(x) = 0],

⁶¹

Since the considerations leading to Proposition X (for every specific F) can also be restated within the system P, the equivalence between a proposition of the form (x) F(x) (F recursive) and the satisfiability of the corresponding formula of the r.p.c. is therefore provable in P, and hence the undecidability of the one follows from that of the other, whereby Proposition IX is proved.⁶²

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

⁵⁰ 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.)

⁵¹ It is not of course necessary that all x₁ … x_n should actually occur in c_i [cf. the example in footnote 27].

⁵² 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₀ being the first).

⁵³ These are the w-consistent systems derived from P by addition of a recursively definable class of axioms.

⁵⁴ 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].

⁵⁵ 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).

⁵⁶ 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).

⁵⁷ And of course the domain of the definition must always be the whole domain of individuals.

⁵⁸ Variables of the third kind may therefore occur at all empty places instead of individual variables, e.g. y = f(x), F(x,f(y)), G[y(x,f(y)),x] etc.

⁵⁹ I.e. forming the conjunction.

⁶⁰ c_i(i = 1 … s) represents any complex of the variables x₁, x₂ … x_m, e.g. x₁ x₃ x₂.

⁶¹ 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.

⁶² 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 (x) F(x) (F recursive).

From the conclusions of Section 2 there follows a remarkable result with regard to a consistency proof of the system P (and its extensions), which is expressed in the following proposition:

Proposition XI: If c be a given recursive, consistent class⁶³ of formulae, then the propositional formula which states that c is consistent is not c-provable; in particular, the consistency of P is unprovable in P,⁶⁴ it being assumed that P is consistent (if not, of course, every statement is provable).

The proof (sketched in outline) is as follows: Let c be any given recursive class of formulae, selected once and for all for purposes of the following argument (in the simplest case it may be the null class). For proof of the fact that 17 Gen r is not c-provable,⁶⁵ only the consistency of c was made use of, as appears from 1, page 59; i.e.

Wid(c) ® ~Bew_c(17 Gen r) (23)

i.e. by (6.1):

Wid(c) ® (x) ~[x B_c (17 Gen r)]

By (13), 17 Gen r = Sb(p 19|Z(p)) and hence:

Wid(c) ® (x) ~[x B_c Sb(p 19|Z(p))]

[197]

i.e. by (8.1):

Wid(c) ® (x) Q(x,p) (24)

We now establish the following: All the concepts defined (or assertions proved) in Sections 2⁶⁶ and 4 are also expressible (or provable) in P. For we have employed throughout only the normal methods of definition and proof accepted in classical mathematics, as formalized in the system P. In particular c (like any recursive class) is definable in P. Let w be the propositional formula expressing Wid(c) in P. The relation Q(x,y) is expressed, in accordance with (8.1), (9) and (10), by the relation-sign q, and Q(x,p), therefore, by r [since by (12) r = Sb(q 19|Z(p))] and the proposition (x) Q(x,p) by 17 Gen r.

In virtue of (24) w Imp (17 Gen r) is therefore provable in P⁶⁷ (and a fortiori c-provable). Now if w were c-provable, 17 Gen r would also be c-provable and hence it would follow, by (23), that c is not consistent.

It may be noted that this proof is also constructive, i.e. it permits, if a proof from c is produced for w, the effective derivation from c of a contradiction. The whole proof of Proposition XI can also be carried 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 that there is no consistency proof for M or for A which could be formalized in M or A respectively, it being assumed that M and A are consistent. It must be expressly noted that Proposition XI (and the corresponding results for M and A) represent no contradiction of the formalistic standpoint of Hilbert. For this standpoint presupposes only the existence of a consistency proof effected by finite means, and there might conceivably be finite proofs which cannot be stated in P (or in M or in A).

Since, for every consistent class c, w is not c-provable, there will always be propositions which are undecidable (from c), namely w, so long as Neg(w) is not c-provable; in

[198]

Proposition VI

c-provable

Throughout this work we have virtually confined ourselves to the system P, and have merely indicated the applications to other systems. The results will be stated and proved in fuller generality in a forthcoming sequel. There too, the mere outline proof we have given of Proposition XI will be presented in detail.

⁶³ C is consistent (abbreviated as Wid(c)) is defined as follows: Wid(c) = ($x) [Form(x) & ~Bew_c(x)].

⁶⁴ This follows if c is replaced by the null class of formulae.

⁶⁵ r naturally depends on c (just as p does).

⁶⁶ From the definition of "recursive" on [179] up to the proof of Proposition VI inclusive.

⁶⁷ That the correctness of w Imp (17 Gen r) can be concluded from (23), is simply based on the fact that–as was remarked at the outset–the undecidable proposition 17 Gen r asserts its own unprovability.

⁶⁸ Cf. J. v. Neumann, 'Zur Hilbertschen Beweistheorie', Math. Zeitschr. 26, 1927.

(Received: 17. xi. 1930.)

Follow Ups:

Post a Followup

Name:
E-Mail:

Subject:

Comments:
: [173]<UL> <H4 ALIGN=CENTER> ON FORMALLY UNDECIDABLE PROPOSITIONS OF PRINCIPIA MATHEMATICA AND RELATED SYSTEMS 1<A HREF="#1">1</A> </H4> 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)<A HREF="#2">2</A> and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann).<A HREF="#3">3</A> 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<A HREF="#4">4</A> which</UL>[174]<UL>cannot be decided from the axioms. This situation is not due in some way to the special nature of the systems set up, but holds for a very extensive class of formal systems, including, in particular, all those arising from the addition of a finite number of axioms to the two systems mentioned,<A HREF="#5">5</A> provided that thereby no false propositions of the kind described in footnote 4 become provable. <DD>Before going into details, we shall first indicate the main lines of the proof, naturally without laying claim to exactness. The formulae of a formal system–we restrict ourselves here to the system PM–are, looked at from outside, finite series of basic signs (variables, logical constants and brackets or separation points), and it is easy to state precisely just which series of basic signs are meaningful formulae and which are not.<A HREF="#6">6</A> Proofs, from the formal standpoint, are likewise nothing but finite series of formulae (with certain specifiable characteristics). For metamathematical purposes it is naturally immaterial what objects are taken as basic signs, and we propose to use natural numbers<A HREF="#7">7</A> for them. Accordingly, then, a formula is a finite series of natural numbers,<A HREF="#8">8</A> and a particular proof-schema is a finite series of finite series of natural numbers. Metamathematical concepts and propositions thereby become concepts and propositions concerning natural numbers, or series of them,<A HREF="#9">9</A> and therefore at least partially expressible in the symbols of the system PM itself. In particular, it can be shown that the concepts, "formula", "proof-schema", "provable formula" are definable in the system PM, i.e. one can give<A HREF="#10">10</A> a formula F(v) of PM–for example–with one free variable v (of the type of a series of numbers), such that F(v)–interpreted as to content–states: v is a provable formula. We now obtain an undecidable proposition of the system PM, i.e. a proposition A, for which neither A nor not-A are provable, in the following manner: </UL>[175]<UL><DD>A formula of PM with just one free variable, and that of the type of the natural numbers (class of classes), we shall designate a class-sign. We think of the class-signs as being somehow arranged in a series,<A HREF="#11">11</A> and denote the n-th one by R(n); and we note that the concept "class-sign" as well as the ordering relation R are definable in the system PM. Let a be any class-sign; by [a; n] we designate that formula which is derived on replacing the free variable in the class-sign a by the sign for the natural number n. The three-term relation x = [y; z] also proves to be definable in PM. We now define a class K of natural numbers, as follows: <A NAME="EQ1"></A> n Î K º ~(Bew [R(n); n])<A HREF="#11a">11a</A> (1) (where Bew x means: x is a provable formula). Since the concepts which appear in the definiens are all definable in PM, so too is the concept K which is constituted from them, i.e. there is a class-sign S,<A HREF="#12">12</A> such that the formula [S; n]–interpreted as to its content–states that the natural number n belongs to K. S, being a class-sign, is identical with some determinate R(q), i.e. S = R(q) holds for some determinate natural number q. We now show that the proposition [R(q); q]<A HREF="#13">13</A> is undecidable in PM. For supposing the proposition [R(q); q] were provable, it would also be correct; but that means, as has been said, that q would belong to K, i.e. according to (1), ~(Bew [R(q); q]) would hold good, in contradiction to our initial assumption. If, on the contrary, the negation of [R(q); q] were provable, then ~(n Î K), i.e. Bew [R(q); q] would hold good. [R(q); q] would thus be provable at the same time as its negation, which again is impossible. <DD>The analogy between this result and Richard's antinomy leaps to the eye; there is also a close relationship with the "liar" antinomy,<A HREF="#14">14</A> since the undecidable proposition [R(q); q] states precisely that q belongs to K, i.e. according to (1), that [R(q); q] is not provable. We are therefore confronted with a proposition which asserts its own unprovability.<A HREF="#15">15</A> The method of proof just exhibited can clearly</UL>[176]<UL>be applied to every formal system having the following features: firstly, interpreted as to content, it disposes of sufficient means of expression to define the concepts occurring in the above argument (in particular the concept "provable formula"); secondly, every provable formula in it is also correct as regards content. The exact statement of the above proof, which now follows, will have among others the task of substituting for the second of these assumptions a purely formal and much weaker one. <DD>From the remark that [R(q); q] asserts its own unprovability, it follows at once that [R(q); q] is correct, since [R(q); q] is certainly unprovable (because undecidable). So the proposition which is undecidable in the system PM yet turns out to be decided by metamathematical considerations. The close analysis of this remarkable circumstance leads to surprising results concerning proofs of consistency of formal systems, which are dealt with in more detail in Section 4 (<A HREF="#PROP-XI">Proposition XI</A>). <HR WIDTH="25%" ALIGN=LEFT> <UL> <A NAME="1">1</A> Cf. the summary of the results of this work, published in Anzeiger der Akad. d. Wiss. in Wien (math.-naturw. Kl.) 1930, No. 19. <A NAME="2">2</A> 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). <A NAME="3">3</A> 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. <A NAME="4">4</A> 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. <A NAME="5">5</A> In this connection, only such axioms in PM are counted as distinct as do not arise from each other purely by change of type. <A NAME="6">6</A> 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. <A NAME="7">7</A> I.e. we map the basic signs in one-to-one fashion on the natural numbers (as is actually done on [179]). <A NAME="8">8</A> I.e. a covering of a section of the number series by natural numbers. (Numbers cannot in fact be put into a spatial order.) <A NAME="9">9</A> 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. <A NAME="10">10</A> It would be very simple (though rather laborious) actually to write out this formula. <A NAME="11">11</A> Perhaps according to the increasing sums of their terms and, for equal sums, in alphabetical order. <A NAME="11a">11a</A> The bar-sign indicates negation. [Replaced with ~.] <A NAME="12">12</A> Again there is not the slightest difficulty in actually writing out the formula S. <A NAME="13">13</A> Note that "[R(q); q]" (or–what comes to the same thing–"[S; q]") is merely a metamathematical description of the undecidable proposition. But as soon as one has ascertained the formula S, one can naturally also determine the number q, and thereby effectively write out the undecidable proposition itself. <A NAME="14">14</A> Every epistemological antinomy can likewise be used for a similar undecidability proof. <A NAME="15">15</A> 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. </UL> <HR WIDTH="25%" ALIGN=LEFT> 2 <DD>We proceed now to the rigorous development of the proof sketched above, and begin by giving an exact description of the formal system P, for which we seek to demonstrate the existence of undecidable propositions. P is essentially the system obtained by superimposing on the Peano axioms the logic of PM<A HREF="#16">16</A> (numbers as individuals, relation of successor as undefined basic concept). <DD>The basic signs of the system P are the following: <DD>I. Constants: "~" (not), "Ú" (or), """ (for all), "0" (nought), "¦" (the successor of), "(", ")" (brackets). <DD>II. Variables of first type (for individuals, i.e. natural numbers including 0): "x1", "y1", "z1", … <DD>Variables of second type (for classes of individuals): "x2", "y2", "z2", … <DD>Variables of third type (for classes of classes of individuals): "x3", "y3", "z3", … and so on for every natural number as type.<A HREF="#17">17</A> <DD>Note: Variables for two-termed and many-termed functions (relations) are superfluous as basic signs, since relations can be defined as classes of ordered pairs and ordered pairs again as classes of classes, e.g. the ordered pair a,b by ((a),(a,b)), where (x,y) means the class whose only elements are x and y, and (x) the class whose only element is x.<A HREF="#18">18</A> </UL>[177]<UL><DD>By a sign of first type we understand a combination of signs of the form: 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 n > 1 we understand by a sign of n-th type the same as variable of n-th type. Combinations of signs of the form a(b), where b is a sign of n-th and a a sign of (n+1)-th type, we call elementary formulae. The class of formulae we define as the smallest class<A HREF="#19">19</A> containing all elementary formulae and, also, along with any a and b the following: ~(a), (a)Ú(b), x"(a) (where x is any given variable).<A HREF="#18a">18a</A> We term (a)Ú(b) the disjunction of a and b, ~(a) the negation and (a)Ú(b) a generalization of a. A formula in which there is no free variable is called a propositional formula (free variable being defined in the usual way). A formula with just n free individual variables (and otherwise no free variables) we call an n-place relation-sign and for n = 1 also a class-sign. <DD>By Subst a(v|b) (where a stands for a formula, v a variable and b a sign of the same type as v) we understand the formula derived from a, when we replace v in it, wherever it is free, by b.<A HREF="#20">20</A> We say that a formula a is a type-lift of another one b, if a derives from b, when we increase by the same amount the type of all variables appearing in b. <DD>The following formulae (I-V) are called axioms (they are set out with the help of the customarily defined abbreviations: ., É, º, ($x), =,<A HREF="#21">21</A> and subject to the usual conventions about omission of brackets)<A HREF="#22">22</A>: <A NAME="AXIOM-I"></A> I. <UL> <A NAME="AXIOM-I1"></A> 1. ~(¦x1 = 0) <A NAME="AXIOM-I2"></A> 2. ¦x1 = ¦y1 É x1 = y1 <A NAME="AXIOM-I3"></A> 3. x2(0).x1 " (x2(x1) É x2(fx1)) É x1 " (x2(x1)) </UL> <A NAME="AXIOM-II"></A> </UL>[178]<UL>II. Every formula derived from the following schemata by substitution of any formulae for p, q and r. <UL> <A NAME="AXIOM-II1"></A> 1. p Ú p É p <A NAME="AXIOM-II2"></A> 2. p É p Ú q <A NAME="AXIOM-II3"></A> 3. p Ú q É q Ú p <A NAME="AXIOM-II4"></A> 4. (p É q) É (r Ú p É r Ú q) </UL> <A NAME="AXIOM-III"></A> III. Every formula derived from the two schemata <UL> <A NAME="AXIOM-III1"></A> 1. v " (a) Ú Subst a(v|c) <A NAME="AXIOM-III2"></A> 2. v " (b É a) Ú b É v " (a) </UL> 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.<A HREF="#23">23</A> <A NAME="AXIOM-IV"></A> IV. Every formula derived from the schema <A NAME="AXIOM-IV1"></A> <UL> 1. ($u)(v " (u(v) º a)) </UL> 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). <A NAME="AXIOM-V"></A> V. Every formula derived from the following by type-lift (and this formula itself): <A NAME="AXIOM-V1"></A> <UL> 1. x1 " (x2(x1) º y2(x1)) Ú x2 = y2. </UL> <DD>This axiom states that a class is completely determined by its elements. <DD>A formula c is called an immediate consequence of a and b, if a is the formula (~(b)) Ú (c), and an immediate consequenee of a, if c is the formula v " (a), where v denotes any given variable. The class of provable formulae is defined as the smallest class of formulae which contains the axioms and is closed with respect to the relation "immediate consequence of".<A HREF="#24">24</A> <DD>The basic signs of the system P are now ordered in one-to-one correspondence with natural numbers, as follows: </UL>[179]<UL><UL> "0" … 1 "¦" … 3 "~" … 5 "Ú" … 7 """ … 9 "(" … 11 ")" … 13 </UL> 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. <DD>We now introduce a parenthetic consideration having no immediate connection with the formal system P, and first put forward the following definition: A number-theoretic function<A HREF="#25">25</A> f(x1,x2,…xn) is said to be recursively defined by the number-theoretic functions y(x1,x2,…xn-1) and m(x1,x2,…xn+1), if for all x2, … xn, k<A HREF="#26">26</A> the following hold: <A NAME="EQ2"></A> f(0,x2,…xn) = y(x2,…xn) f(k+1,x2,…xn) = m(k,f(k,x2,…xn),x2,…xn). (2) <DD>A number-theoretic function f is called recursive, if there exists a finite series of number-theoretic functions f1, f2, … fn which ends in f and has the property that every function fk of the series is either recursively defined</UL>[180]<UL>by two of the earlier ones, or is derived from any of the earlier ones by substitution,<A HREF="#27">27</A> or, finally, is a constant or the successor function x+1. The length of the shortest series of fi, which belongs to a recursive function f, is termed its degree. A relation R(x1,x2,…xn) among natural numbers is called recursive,<A HREF="#28">28</A> if there exists a recursive function f(x1,x2,…xn) such that for all x1, x2, … xn R(x1,x2,…xn) º [f(x1,x2,…xn) = 0]<A HREF="#29">29</A>. <DD>The following propositions hold: <A NAME="PROP-I"></A> 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). <A NAME="PROP-II"></A> II. If R and S are recursive relations, then so also are ~R, R Ú S (and therefore also R & S). <A NAME="PROP-III"></A> III. If the functions f(c) and y(h) are recursive, so also is the relation: f(c) = y(h).<A HREF="#30">30</A> <A NAME="PROP-IV"></A> IV. If the function f(c) and the relation R(x,h) are recursive, so also then are the relations S, T <UL> S(c,h) ~ ($x)[x £ f(c) & R(x,h)] T(c,h) ~ (x)[x £ f(c) ® R(x,h)] </UL> and likewise the function y <UL> y(c,h) = ex [x £ f(c) & R(x,h)] </UL> where ex F(x) means: the smallest number x for which F(x) holds and 0 if there is no such number. <DD>Proposition I follows immediately from the definition of "recursive". Propositions II and III are based on the readily ascertainable fact that the number-theoretic functions corresponding to the logical concepts ~, Ú, = a(x), b(x,y), g(x,y) namely <UL> a(0) = 1; a(x) = 0 for x ¹ 0 b(0,x) = b(x,0) = 0; b(x,y) = 1, if x, y both ¹ O </UL></UL>[181]<UL><UL> g(x,y) = 0, if x = y; g(x,y) = 1, if x ¹ y </UL> are recursive. The proof of Proposition IV is briefly as follows: According to the assumption there exists a recursive r(x,h) such that R(x,h) º [r(x,h) = 0]. <DD>We now define, according to the recursion schema (2), a function C(x,h) in the following manner: C(0,h) = 0 C(n+1,h) = (n+1).a + C(n,h).a(a)<A HREF="#31">31</A> where a = a[a(r(0,h))].a[r(n+1,h)].a[C(n,h)]. <DD>C(n+1,h) is therefore either = n+1 (if a = 1) or = C(n,h) (if a = 0).<A HREF="#32">32</A> The first case clearly arises if and only if all the constituent factors of a are 1, i.e. if ~R(O,h) & R(n+1,h) & [C(n,h) = 0]. <DD>From this it follows that the function C(n,h) (considered as a function of n) remains 0 up to the smallest value of n for which R(n,h) holds, and from then on is equal to this value (if R(0,h) is already the case, the corresponding C(x,h) is constant and = 0). Therefore: <UL> y(c,h) = C(f(c),h) S(c,h) º R[y(c,h)),h)] </UL> The relation T can be reduced by negation to a case analogous to S, so that Proposition IV is proved. <DD>The functions x+y, x.y, xy, and also the relations x ‹ y, x = y are readily found to be recursive; starting from these concepts, we now define a series of functions (and relations) 1-45, of which each is defined from the earlier ones by means of the operations named in Propositions I to IV. This procedure, generally speaking, puts together many of the definition steps permitted by Propositions I to IV. Each of the functions (relations) 1-45, containing, for example, the concepts "formula", "axiom", and "immediate consequence", is therefore recursive. </UL>[182]<UL> <A NAME="DEF1"></A> 1. <UL>x/y º ($z)[z £ x & x = y.z]<A HREF="#33">33</A> x is divisible by y.<A HREF="#34">34</A></UL> <A NAME="DEF2"></A> 2.<UL> Prim(x) º ~($z)[z £ x & z ¹ 1 & z ¹ x & x/z] & x > 1 x is a prime number.</UL> <A NAME="DEF3"></A> 3.<UL> 0 Pr x º 0 (n+1) Pr x º ey [y £ x & Prim(y) & x/y & y > n Pr x] n Pr x is the n-th (in order of magnitude) prime number contained in x.<A HREF="#34a">34a</A></UL> <A NAME="DEF4"></A> 4.<UL> 0! º 1 (n+1)! º (n+1).n!</UL> <A NAME="DEF5"></A> 5.<UL> Pr(0) º 0 Pr(n+1) º ey [y £ {Pr(n)}! + 1 & Prim(y) & y > Pr(n)] Pr(n) is the n-th prime number (in order of magnitude).</UL> <A NAME="DEF6"></A> 6.<UL> n Gl x º ey [y £ x & x/(n Pr x)y & not x/(n Pr x)y+1] n Gl x is the n-th term of the series of numbers assigned to the number x (for n > 0 and n not greater than the length of this series).</UL> <A NAME="DEF7"></A> 7.<UL> l(x) º ey [y £ x & y Pr x > 0 & (y+1) Pr x = 0] l(x) is the length of the series of numbers assigned to x.</UL> <A NAME="DEF8"></A> 8.<UL> x * y º ez [z £ [Pr{l(x)+l(y)}]x+y & (n)[n £ l(x) ® n Gl z = n Gl x] & (n)[0 < n £ l(y) ® {n+l(x)} Gl z = n Gl y]] x * y corresponds to the operation of "joining together" two finite series of numbers.</UL> <A NAME="DEF9"></A> 9.<UL> R(x) º 2x R(x) corresponds to the number-series consisting only of the number x (for x > 0).</UL> <A NAME="DEF10"></A> 10.<UL> E(x) º R(11) * x * R(13) E(x) corresponds to the operation of "bracketing" [11 and 13 are assigned to the basic signs "(" and ")"].</UL> <A NAME="DEF11"></A> 11.<UL> n Var x º ($z)[13 < z £ x & Prim(z) & x = zn] & n ¹ 0 x is a variable of n-th type.</UL> <A NAME="DEF12"></A> 12.<UL> Var(x) º ($n)[n £ x & n Var x] x is a variable.</UL> <A NAME="DEF13"></A> 13.<UL> Neg(x) º R(5) * E(x) Neg(x) is the negation of x.</UL> </UL>[183]<UL> <A NAME="DEF14"></A> 14.<UL> x Dis y º E(x) * R(7) * E(y) x Dis y is the disjunction of x and y.</UL> <A NAME="DEF15"></A> 15.<UL> x Gen y º R(x) * R(9) * E(y) x Gen y is the generalization of y by means of the variable x (assuming x is a variable).</UL> <A NAME="DEF16"></A> 16.<UL> 0 N x º x (n+1) N x º R(3) * n N x n N x corresponds to the operation: "n-fold prefixing of the sign '¦' before x."</UL> <A NAME="DEF17"></A> 17.<UL> Z(n) º n N [R(1)] Z(n) is the number-sign for the number n.</UL> <A NAME="DEF18"></A> 18.<UL> Typ1'(x) º ($m,n){m,n £ x & [m = 1 Ú 1 Var m] & x = n N [R(m)]}<A HREF="#34b">34b</A> x is a sign of first type.</UL> <A NAME="DEF19"></A> 19.<UL> Typn(x) º [n = 1 & Typ1'(x)] Ú [n > 1 & ($v){v £ x & n Var v & x = R(v)}] x is a sign of n-th type.</UL> <A NAME="DEF20"></A> 20.<UL> Elf(x) º ($y,z,n)[y,z,n £ x & Typn(y) & Typn+1(z) & x = z * E(y)] x is an elementary formula.</UL> <A NAME="DEF21"></A> 21.<UL> Op(x,y,z) º x = Neg(y) Ú x = y Dis z Ú ($v)[v £ x & Var(v) & x = v Gen y]</UL> <A NAME="DEF22"></A> 22.<UL> FR(x) º (n){0 < n £ l(x) ® Elf(n Gl x) Ú ($p,q)[0 < p,q < n & Op(n Gl x,p Gl x,q Gl x)]} & l(x) > 0 x is a series of formulae of which each is either an elementary formula or arises from those preceding by the operations of negation, disjunction and generalization.</UL> <A NAME="DEF23"></A> 23.<UL> Form(x) º ($n){n £ (Pr[l(x)2])x.[l(x)]2 & FR(n) & x = [l(n)] Gl n}<A HREF="#35">35</A> x is a formula (i.e. last term of a series of formulae n).</UL> <A NAME="DEF24"></A> 24.<UL> v Geb n,x º Var(v) & Form(x) & ($a,b,c)[a,b,c £ x & x = a * (v Gen b) * c & Form(b) & l(a)+1 £ n £ l(a)+l(v Gen b)] The variable v is bound at the n-th place in x.</UL> </UL>[184]<UL> <A NAME="DEF25"></A> 25.<UL> v Fr n,x º Var(v) & Form(x) & v = n Gl x & n £ l(x) & not(v Geb n,x) The variable v is free at the n-th place in x.</UL> <A NAME="DEF26"></A> 26.<UL> v Fr x º ($n)[n £ l(x) & v Fr n,x] v occurs in x as a free variable.</UL> <A NAME="DEF27"></A> 27.<UL> Su x(n|y) º ez {z £ [Pr(l(x)+l(y))]x+y & [($u,v)u,v £ x & x = u * R(b Gl x) * v & z = u * y * v & n = l(u)+1]} Su x(n|y) derives from x on substituting y in place of the n-th term of x (it being assumed that 0 < n £ l(x)).</UL> <A NAME="DEF28"></A> 28.<UL> 0 St v,x º en {n £ l(x) & v Fr n,x & not ($p)[n £ l(x) & v Fr p,x]} (k+1) St v,x º en {n < k St v,x & v Fr n,x & ($p)[n k St v,x is the (k+1)-th place in x (numbering from the end of formula x) at which v is free in x (and 0, if there is no such place.)</UL> <A NAME="DEF29"></A> 29.<UL> A(v,x) º en {n £ l(x) & n St v = 0} A(v,x) is the number of places at which v is free in x.</UL> <A NAME="DEF30"></A> 30.<UL> Sb0(x v|y) º x Sbk+1(x v|y) º Su[Sbk(x v|y)][(k St v, x)|y)]</UL> <A NAME="DEF31"></A> 31.<UL> Sb(x v|y) º SbA(v,x)(x v|y)<A HREF="#36">36</A> Sb(x v|y) is the concept Subst a(v|b), defined above.<A HREF="#37">37</A></UL> <A NAME="DEF32"></A> 32.<UL> x Imp y º [Neg(x)] Dis y x Con y º Neg{[Neg(x)] Dis [Neg(y)]} x Aeq y º (x Imp y) Con (y Imp x) v Ex y º Neg{v Gen [Neg(y)]}</UL> <A NAME="DEF33"></A> 33.<UL> n Th x º en {y £ x(xn) & (k) £ l(x) ® (k Gl x £ 13 & k Gl y = k Gl x) Ú (k Gl x > 13 & k Gl y = k Gl x.[1 Pr(k Gl x)]n)]} n Th x is the n-th type-lift of x (in the case when x and n Th x are formulae).</UL> <DD>To the <A HREF="#AXIOM-I">axioms I</A>, 1 to 3, there correspond three determinate numbers, which we denote by z1, z2, z3, and we define: <A NAME="DEF34"></A> 34.<UL> Z–Ax(x) º (x = z1 Ú x = z2 Ú x = z3)</UL> </UL>[185]<UL> <A NAME="DEF35"></A> 35.<UL> A1-Ax(x) º ($y)[y £ x & Form(y) & x = (y Dis y) Imp y] x is a formula derived by substitution in the <A HREF="#AXIOM-II1">axiom-schema II, 1</A>. Similarly A2-Ax, A3-Ax, A4-Ax are defined in accordance with the axioms II, 2 to 4.</UL> <A NAME="DEF36"></A> 36.<UL> A-Ax(x) º A1-Ax(x) Ú A2-Ax(x) Ú A3-Ax(x) Ú A4-Ax(x) x is a formula derived by substitution in an axiom of the sentential calculus.</UL> <A NAME="DEF37"></A> 37.<UL> Q(z,y,v) º ($n,m,w)[n £ l(y) & m £ l(z) & w £ z & w = m Gl x & w Geb n,y & v Fr n,y] z contains no variable bound in y at a position where v is free.</UL> <A NAME="DEF38"></A> 38.<UL> L1-Ax(x) º ($v,y,z,n){v,y,z,n £ x & n Var v & Typn(z) & Form(y) & Q(z,y,v) & x = (v Gen y) Imp [Sb(v|z)]} x is a formula derived from the <A HREF="#AXIOM-III1">axiom-schema III, 1</A> by substitution.</UL> <A NAME="DEF39"></A> 39.<UL> L2-Ax(x) º ($v,q,p){v,q,p £ x & Var(v) & Form(p) & v Fr p & Form(q) & x = [v Gen (p Dis q)] Imp [p Dis (v Gen q)]} x is a formula derived from the <A HREF="#AXIOM-III2">axiom-schema III, 2</A> by substitution.</UL> <A NAME="DEF40"></A> 40.<UL> R-Ax(x) º ($u,v,y,n)[u, v, y, n £ x & n Var v & (n+1) Var u & u Fr y & Form(y) & x = u $x {v Gen [[R(u)*E(R(v))] Aeq y]}] x is a formula derived from the <A HREF="#AXIOM-IV1">axiom-schema IV, 1</A> by substitution.</UL> <DD>To the <A HREF="#AXIOM-V1">axiom V, 1</A> there corresponds a determinate number z4 and we define: <A NAME="DEF41"></A> 41.<UL> M-Ax(x) º ($n)[n £ x & x = n Th z4]</UL> <A NAME="DEF42"></A> 42.<UL> Ax(x) º Z-Ax(x) Ú A-Ax(x) Ú L1-Ax(x) Ú L2-Ax(x) Ú R-Ax(x) Ú M-Ax(x) x is an axiom.</UL> <A NAME="DEF43"></A> 43.<UL> Fl(x y z) º y = z Imp x Ú ($v)[v £ x & Var(v) & x = v Gen y] x is an immediate consequence of y and z.</UL> <A NAME="DEF44"></A> </UL>[186]<UL> 44.<UL> Bw(x) º (n){0 < n £ l(x) ® Ax(n Gl x) Ú ($p,q)[0 < p,q < n & Fl(n Gl x, p Gl x, q Cl x)]} & l(x) > 0 x is a proof-schema (a finite series of formulae, of which each is either an axiom or an immediate consequence of two previous ones).</UL> <A NAME="DEF45"></A> 45.<UL> x B y º Bw(x) & [l(x)] Gl x = y x is a proof of the formula y.</UL> <A NAME="DEF46"></A> 46.<UL> Bew(x) = (Ey)y B x x is a provable formula. [Bew(x) is the only one of the concepts 1-46 of which it cannot be asserted that it is recursive.]</UL> <DD>The following proposition is an exact expression of a fact which can be vaguely formulated in this way: every recursive relation is definable in the system P (interpreted as to content), regardless of what interpretation is given to the formulae of P: <A NAME="PROP-V"></A> <DD>Proposition V: To every recursive relation R(x1 … xn) there corresponds an n-place relation-sign r (with the free variables<A HREF="#38">38</A> u1, u2, … un) such that for every n-tuple of numbers (x1 … xn) the following hold: <UL> <A NAME="EQ3"></A> R(x1 … xn) ® Bew{Sb[r (u1 … un)|(Z(x1) … Z(xn)]} (3) <A NAME="EQ4"></A> ~R(x1 … xn) ® Bew{Neg Sb[r (u1 … un)|(Z(x1) … Z(xn)]} (4) </UL> <DD>We content ourselves here with indicating the proof of this proposition in outline, since it offers no difficulties of principle and is somewhat involved.<A HREF="#39">39</A> We prove the proposition for all relations R(x1 … xn) of the form: x1 = f(x2 … xn)<A HREF="#40">40</A> (where f is a recursive function) and apply mathematical induction on the degree of f. For functions of the first degree (i.e. constants and the function x+1) the proposition is trivial. Let f then be of degree m. It derives from functions of lower degree f1 … fk by the operations of substitution or recursive definition. Since, by the inductive assumption, everything is already proved for f1 … fk, there exist corresponding relation-signs r1 … rk such that (<A HREF="#EQ3">3</A>) and (<A HREF="#EQ4">4</A>) hold. The processes of definition whereby f is derived from f1 … fk (substitution and re-</UL>[187]<UL>cursive definition) can all be formally mapped in the system P. If this is done, we obtain from r1 … rk a new relation-sign r<A HREF="#41">41</A>, for which we can readily prove the validity of (<A HREF="#EQ3">3</A>) and (<A HREF="#EQ4">4</A>) by use of the inductive assumption. A relation-sign r, assigned in this fashion to a recursive relation,<A HREF="#42">42</A> will be called recursive. <DD>We now come to the object of our exercises: Let c be any class of formulae. We denote by Flg(c) (set of consequences of c) the smallest set of formulae which contains all the formulae of c and all axioms, and which is closed with respect to the relation "immediate consequence of". c is termed w-consistent, if there is no class-sign a such that: <UL> (n)[Sb(a v|Z(n)) Î Flg(c)] & [Neg(v Gen a)] Î Flg(c) </UL> where v is the free variable of the class-sign a. <DD>Every w-consistent system is naturally also consistent. The converse, however, is not the case, as will be shown later. <DD>The general result as to the existence of undecidable propositions reads: <A NAME="PROP-VI"></A> <DD>Proposition VI: To every w-consistent recursive class c of formulae there correspond recursive class-signs r, such that neither v Gen r nor Neg (v Gen r) belongs to Flg(c) (where v is the free variable of r). <DD>Proof: Let c be any given recursive w-consistent class of formulae. We define: <UL> <A NAME="EQ5"></A> Bwc(x) º (n)[n £ l(x) ® Ax(n Gl x) Ú (n Gl x) Î c Ú (Ep,q){0 < p,q < n & Fl(n Gl x, p Gl x, q Gl x)}] & l(x) > 0 (5) (cf. the analogous concept <A HREF="#DEF44">44</A>) <A NAME="EQ6"></A> x Bc y º Bwc(x) & [l(x)] Gl x = y (6) <A NAME="EQ6.1"></A> Bewc(x) º ($y)y Bc x (6.1) (cf. the analogous concepts <A HREF="#DEF45">45</A>, <A HREF="#DEF46">46</A>) </UL> The following clearly hold: <UL> <A NAME="EQ7"></A> (x)[Bewc(x) º x Î Flg(c)] (7) <A NAME="EQ8"></A> (x)[Bew(x) ® Bewc(x)] (8) </UL> </UL>[188]<UL> We now define the relation: <UL> <A NAME="EQ8.1"></A> Q(x,y) º ~{x Bc[Sb(y 19|z(y))]}. (8.1) </UL> <DD>Since x Bc y [according to (<A HREF="#EQ6">6</A>), (<A HREF="#EQ5">5</A>)] and Sb(y 19|Z(y)) (according to definitions <A HREF="#DEF17">17</A>, <A HREF="#DEF31">31</A>) are recursive, so also is Q(x,y). According to <A HREF="#PROP-V">Proposition V</A> and (<A HREF="#EQ8">8</A>) there is therefore a relation-sign q (with the free variables 17, 19) such that <UL> <A NAME="EQ9"></A> ~{x Bc [Sb(y 19|Z(y))]} ® Bewc[Sb(q 17|Z(x) 19|Z(y))]. (9) <A NAME="EQ10"></A> x Bc [Sb(y 19|Z(y))] ® Bewc[Neg Sb(q 17|Z(x) 19|Z(y))]. (10) </UL> We put <A NAME="EQ11"></A> p = 17 Gen q (11) (p is a class-sign with the free variable 19) and <A NAME="EQ12"></A> r = Sb(q 19|Z(p)) (12) (r is a recursive class-sign with the free variable 17).<A HREF="#43">43</A> Then <A NAME="EQ13"></A> <UL> Sb(p 19|Z(p)) (13) <DD>= Sb ([17 Gen q] 19|z(p)) <DD>= 17 Gen Sb(q 19|z(p)) <DD>= 17 Gen r<A HREF="#44">44</A> </UL> [because of (<A HREF="#EQ11">11</A>) and (<A HREF="#EQ12">12</A>)] and furthermore: <A NAME="EQ14"></A> Sb(q 17|Z(x) 19|Z(p)) = Sb(r 17|Z(x)) (14) [according to (<A HREF="#EQ12">12</A>)]. If now in (<A HREF="#EQ9">9</A>) and (<A HREF="#EQ10">10</A>) we substitute p for y, we find, in virtue of (<A HREF="#EQ13">13</A>) and (<A HREF="#EQ14">14</A>): <UL> <A NAME="EQ15"></A> x Bc (17 Gen r) ® Bewc[Sb(r 17|Z(x))] (15) <A NAME="EQ16"></A> x Bc (17 Gen r) ® Bewc[Neg Sb(r 17|Z(x))] (16) </UL> </UL>[189]<UL> Hence: <DD>1. 17 Gen r is not c-provable.<A HREF="#45">45</A> For if that were so, there would (according to <A HREF="#EQ6.1">6.1</A>) be an n such that n Bc (17 Gen r). By (<A HREF="#EQ16">16</A>) it would therefore be the case that: Bewc[Neg Sb(r 17|Z(n))] while–on the other hand–from the c-provability of 17 Gen r there follows also that of Sb(r 17|Z(n)). c would therefore be inconsistent (and, a fortiori, w-inconsistent). <DD>2. Neg(17 Gen r) is not c-provable. Proof: As shown above, 17 Gen r is not c-provable, i.e. (according to <A HREF="#EQ6.1">6.1</A>) the following holds: (n) n Bc(17 Gen r). Whence it follows, by (<A HREF="#EQ15">15</A>), that (n) Bewc[Sb(r 17|Z(n))], which together with Bewc[Neg(17 Gen r)] would conflict with the w-consistency of c. Neg(17 Gen r) is therefore undecidable in c, so that <A HREF="#PROP-VI">Proposition VI</A> is proved. <DD>One can easily convince oneself that the above proof is constructive,<A HREF="#45a">45a</A> i.e. that the following is demonstrated in an intuitionistically unobjectionable way: Given any recursively defined class c of formulae: If then a formal decision (in c) be given for the (effectively demonstrable) propositional formula 17 Gen r, we can effectively state: <DD>1. A proof for Neg(17 Gen r). <DD>2. For any given n, a proof for Sb(r 17|Z(n)), i.e. a formal decision of 17 Gen r would lead to the effective demonstrability of an w-inconsistency. <DD>We shall call a relation (class) of natural numbers R(x1 … xn) calculable [entscheidungsdefinit], if there is an n-place relation-sign r such that (<A HREF="#EQ3">3</A>) and (<A HREF="#EQ4">4</A>) hold (cf. <A HREF="#PROP-V">Proposition V</A>). In particular, therefore, by Proposition V, every recursive relation is calculable. Similarly, a relation-sign will be called calculable, if it be assigned in this manner to a calculable relation. It is, then, sufficient for the existence of undecidable propositions, to assume of the class c that it is w-consistent and calculable. For the property of being calculable carries over from c to x Bc y (cf. (<A HREF="#EQ5">5</A>), (<A HREF="#EQ6">6</A>))</UL>[190]<UL>and to Q(x,y) (cf. <A HREF="#EQ8.1">8.1</A>), and only these are applied in the above proof. The undecidable proposition has in this case the form v Gen r, where r is a calculable class-sign (it is in fact enough that c should be calculable in the system extended by adding c). <DD>If, instead of w-consistency, mere consistency as such is assumed for c, then there follows, indeed, not the existence of an undecidable proposition, but rather the existence of a property (r) for which it is possible neither to provide a counter-example nor to prove that it holds for all numbers. For, in proving that 17 Gen r is not c-provable, only the consistency of c is employed (cf. [189]) and from ~Bewc(17 Gen r) it follows, according to (<A HREF="#EQ15">15</A>), that for every number x, Sb(r 17|z(x)) is c-provable, and hence that Sb(r 17|Z(x)) is not c-provable for any number. <DD>By adding Neg(17 Gen r) to c, we obtain a consistent but not w-consistent class of formulae c'. c' is consistent, since otherwise 17 Gen r would be c-provable. c' is not however w-consistent, since in virtue of ~Bewc(17 Gen r) and (<A HREF="#EQ15">15</A>) we have: (x) BewcSb(r 17|Z(x)), and so a fortiori: (x) Bewc'Sb(r 17|Z(x)), and on the other hand, naturally: Bewc'[Neg(17 Gen r)].<A HREF="#46">46</A> <DD>A special case of <A HREF="#PROP-VI">Proposition VI</A> is that in which the class c consists of a finite number of formulae (with or without those derived therefrom by type-lift). Every finite class a is naturally recursive. Let a be the largest number contained in a. Then in this case the following holds for c: x Î c º ($m,n)[m £ x & n £ a & n Î a & x = m Th n] <DD>c is therefore recursive. This allows one, for example, to conclude that even with the help of the axiom of choice (for all types), or the generalized continuum hypothesis, not all propositions are decidable, it being assumed that these hypotheses are w-consistent. <DD>In the proof of <A HREF="#PROP-VI">Proposition VI</A> the only properties of the system P employed were the following: <DD>1. The class of axioms and the rules of inference (i.e. the relation "immediate consequence of") are recursively definable (as soon as the basic signs are replaced in any fashion by natural numbers). <DD>2. Every recursive relation is definable in the system P (in the sense of <A HREF="#PROP-V">Proposition V</A>). <DD>Hence in every formal system that satisfies assumptions 1 and 2 and is w-consistent, undecidable propositions exist of the form (x) F(x), where F is a recursively defined property of natural numbers, and so too in every extension of such</UL>[191]<UL>a system made by adding a recursively definable w-consistent class of axioms. As can be easily confirmed, the systems which satisfy assumptions 1 and 2 include the Zermelo-Fraenkel and the v. Neumann axiom systems of set theory,<A HREF="#47">47</A> and also the axiom system of number theory which consists of the Peano axioms, the operation of recursive definition [according to schema (2)] and the logical rules.<A HREF="#48">48</A> Assumption 1 is in general satisfied by every system whose rules of inference are the usual ones and whose axioms (like those of P) are derived by substitution from a finite number of schemata.<A HREF="#48a">48a</A> <HR WIDTH="25%" ALIGN=LEFT> <UL> <A NAME="16">16</A> 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. <A NAME="17">17</A> It is presupposed that for every variable type denumerably many signs are available. <A NAME="18">18</A> 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. <A NAME="18a">18a</A> Thus x " (a) is also a formula if x does not occur, or does not occur free, in a. In that case x " (a) naturally means the same as a. <A NAME="19">19</A> 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. <A NAME="20">20</A> Where v does not occur in a as a free variable, we must put Subst a(v|b) = a. Note that "Subst" is a sign belonging to metamathematics. <A NAME="21">21</A> As in PM I, *13, x1 = y1 is to be thought of as defined by x2 " (x2(x1) É x2(y1)) (and similarly for higher types.) <A NAME="22">22</A> 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 <UL> 1. eliminate the abbreviations 2. add the suppressqd brackets. </UL> Note that the resultant expressions must be "formulae" in the above sense. (Cf. also the exact definitions of the metamathematical concepts on [182]ff.) <A NAME="23">23</A> 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. <A NAME="24">24</A> 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). <A NAME="25">25</A> 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. <A NAME="26">26</A> 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.] <A NAME="27">27</A> More precisely, by substitution of certain of the foregoing functions in the empty places of the preceding, e.g. fk(x1,x2) = fp[fq(x1,x1),fr(x2)] (p, q, r ‹ k). Not all the variables on the left-hand side must also occur on the right (and similarly in the recursion schema (2)). <A NAME="28">28</A> 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. <A NAME="29">29</A> 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. <A NAME="30">30</A> We use [greek] letters c, h, as abbreviations for given n-tuple sets of variables, e.g. x1, x2 … xn. <A NAME="31">31</A> We take it to be recognized that the functions x+y (addition) and x.y (multiplication) are recursive. <A NAME="32">32</A> a cannot take values other than 0 and 1, as is evident from the definition of a. <A NAME="33">33</A> 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). <A NAME="34">34</A> 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. <A HREF="#PROP-IV">Proposition IV</A>.) On the other hand, the range of the defined concept would almost always remain unaffected by its omission. <A NAME="34a">34a</A> For 0 < n £ z, where z is the number of distinct prime numbers dividing into x. Note that for n = z+1, n Pr x = 0. <A NAME="34b">34b</A> m,n £ x stands for: m £ x & n £ x (and similarly for more than two variables). <A NAME="35">35</A> The limitation n £ (Pr[l(x)]2x.[l(x)]2 means roughly this: The length of the shortest series of formulae belonging to x can at most be equal to the number of constituent formulae of x. There are however at most l(x) constituent formulae of length 1, at most l(x)-1 of length 2, etc. and in all, therefore, at most 1¤2[l(x){l(x)+1}] £ [l(x)]2. The prime numbers in n can therefore all be assumed smaller that Pr{[l(x)]2}, their number £[l(x)]2 and their exponents (which are constituent formulae of x) £x. <A NAME="36">36</A> Where v is not a variable or x not a formula, then Sb(x v|y) = x. <A NAME="37">37</A> Instead of Sb[Sb[x v|y] z|y] we write: Sb(x v|y w|z) (and similarly for more than two variables). <A NAME="38">38</A> The variables u1 … un could be arbitrarily allotted. There is always, e.g., an r with the free variables 17, 19, 23 … etc., for which (<A HREF="#EQ3">3</A>) and (<A HREF="#EQ4">4</A>) hold. <A NAME="39">39</A> <A HREF="#PROP-V">Proposition V</A> 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. <A NAME="40">40</A> From this there follows immediately its validity for every recursive relation, since any such relation is equivalent to 0 = f(x1 … xn), where f is recursive. <A NAME="41">41</A> 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. <A NAME="42">42</A> Which thus, as regards content, expresses the existence of this relation. <A NAME="43">43</A> r is derived in fact, from the recursive relation-sign q on replacement of a variable by a determinate number (p). <A NAME="44">44</A> The operations Gen and Sb are naturally always commutative, wherever they refer to different variables. <A NAME="45">45</A> "x is c-provable" signifies: x Î Flg(c), which, by (<A HREF="#EQ7">7</A>), states the same as Bewc(x). <A NAME="45a">45a</A> Since all existential assertions occurring in the proof are based on <A HREF="#PROP-V">Proposition V</A>, which, as can easily be seen, is intuitionistically unobjectionable. <A NAME="46">46</A> 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). <A NAME="47">47</A> 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). <A NAME="48">48</A> Cf. Problem III in D. Hilbert's lecture: 'Probleme der Grundlegung der Mathematik', Math. Ann. 102. <A NAME="48a">48a</A> 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. </UL> <HR WIDTH="25%" ALIGN=LEFT> 3 <DD>From <A HREF="#PROP-VI">Proposition VI</A> we now obtain further consequences and for this purpose give the following definition: <DD>A relation (class) is called arithmetical, if it can be defined solely by means of the concepts +, . [addition and multiplication, applied to natural numbers]<A HREF="#49">49</A> and the logical constants Ú, ~, (x), =, where (x) and = are to relate only to natural numbers.<A HREF="#50">50</A> The concept of "arithmetical proposition" is defined in a corresponding way. In particular the relations "greater [than]" and "congruent to a modulus" are arithmetical, since x > y º ~($z)[y = x+z] x @ y(mod n) º ($z)[x = y+z.n Ú y = x+z.n] <DD>We now have: <A NAME="PROP-VII"></A> <DD>Proposition VII: Every recursive relation is arithmetical. <DD>We prove this proposition in the form: Every relation of the form x0 = f(x1 … xn), where f is recursive, is arithmetical, and apply mathematical induction on the degree of f. Let f be of degree s (s > 1). Then either </UL>[192]<UL> <DD>1. f(x1 … xn) = r[c1(x1 … xn), c2(x1 … xn) … cm(x1 … xn)]<A HREF="#51">51</A> <DD>(where p and all the x's have degrees smaller than s) or <DD>2. f(0,x2 … xn) = y(x2 … xn) <DD>f(k+1,x2 … xn) = m[k,f(k,x2 … xn),x2 … xn] <DD>(where y, m are of lower degree than s). <DD>In the first case we have: <UL> x0 = f(x1 … xn) º ($y1 … ym)[R(x0,y1 … ym) & S1(y1,x1 … xn) & … & Sm(ym,x1 … xn)], </UL> where R and Si are respectively the arithmetical relations which by the inductive assumption exist, equivalent to x0 = r(y1 … ym) and y = ci(x1 … xn). In this case, therefore, x0 = f(x1 … xn) is arithmetical. <DD>In the second case we apply the following procedure: The relation x0 = f(x1 … xn) can be expressed with the help of the concept "series of numbers" (f)<A HREF="#52">52</A> as follows: <UL> x0 = f(x1 … xn) º ($f){f0 = y(x2 … xn) & (k)[k < x1 ® fk+1 = m(k,fk,x2 … xn)] & x0 = fx1} </UL> If S(y,x2 … xn) and T(z,x1 … xn+1) are respectively the arithmetical relations–which by the inductive assumption exist–equivalent to <UL> y = y(x2 … xn) and z = m(x1 … xn+1), </UL> the following then holds: <UL> <A NAME="EQ17"></A> x0 = f(x1 … xn) º ($f){S(f0,x2 … xn) & (k)[k < x1 ® T(fk+1,k,fk,x2 … xn)] & x0 = fx1} (17) </UL> We now replace the concept "series of numbers" by "pair of numbers", by assigning to the number pair n, d the number series f(n,d)(fk(n,d) = [n]1+(k+1)d), where [n]p denotes the smallest non-negative residue of n modulo p. <DD>We then have the following: <A NAME="LEMMA1"></A> <DD>Lemma 1: If f is any series of natural numbers and k any natural number, then there exists a pair of natural numbers n, d, such that f(n,d) and f agree in the first k terms. <DD>Proof: Let l be the largest of the numbers k,f0,f1 … fk-1. Let n be so determined that <DD>n = fi(mod(1+(i+1)l!)] for i = 0,1 … k-1 </UL>[193]<UL> which is possible, since every two of the numbers 1+(i+1)l! (i = 0,1 … k-1) are relatively prime. For a prime number contained in two of these numbers would also be contained in the difference (i1-i2)l! and therefore, because |i1-i2| < 1, in l!, which is impossible. The number pair n, l! thus accomplishes what is required. <DD>Since the relation x = [n]p is defined by x = n(mod p) & x < p and is therefore arithmetical, so also is the relation P(x0,x1 … xn) defined as follows: <UL> P(x0 … xn) º ($n,d){S([n]d+1,x2 … xn) & (k) [k < x1 ® T([n]1+d(k+2),k,[n]1+d(k+1),x2 … xn)] & x0 = [n]1+d(x1+1)} </UL> which, according to (<A HREF="#EQ17">17</A>) and <A HREF="#Lemma1">Lemma 1</A>, is equivalent to x0 = f(x1 … xn) (we are concerned with the series f in (<A HREF="#EQ17">17</A>) only in its course up to the x1+1-th term). Thereby <A HREF="#PROP-VII">Proposition VII</A> is proved. <DD>According to <A HREF="#PROP-VII">Proposition VII</A> there corresponds to every problem of the form (x) F(x) (F recursive) an equivalent arithmetical problem, and since the whole proof of <A HREF="#PROP-VII">Proposition VII</A> can be formalized (for every specific F) within the system P, this equivalence is provable in P. Hence: <A NAME="PROP-VIII"></A> <DD>Proposition VIII: In every one of the formal systems<A HREF="#53">53</A> referred to in <A HREF="#PROP-VI">Proposition VI</A> there are undecidable arithmetical propositions. <DD>The same holds (in virtue of the remarks at the end of Section 3) for the axiom system of set theory and its extensions by w-consistent recursive classes of axioms. <DD>We shall finally demonstrate the following result also: <A NAME="PROP-IX"></A> <DD>Proposition IX: In all the formal systems referred to in <A HREF="#PROP-VI">Proposition VI</A><A HREF="#53">53</A> there are undecidable problems of the restricted predicate calculus<A HREF="#54">54</A> (i.e. formulae of the restricted predicate calculus for which neither universal validity nor the existence of a counter-example is provable).<A HREF="#55">55</A> </UL>[194]<UL> <DD>This is based on <A NAME="PROP-X"></A> <DD>Proposition X: Every problem of the form (x) F(x) (F recursive) can be reduced to the question of the satisfiability of a formula of the restricted predicate calculus (i.e. for every recursive F one can give a formula of the restricted predicate calculus, the satisfiability of which is equivalent to the validity of (x) F(x)). <DD>We regard the restricted predicate calculus (r.p.c.) as consisting of those formulae which are constructed out of the basic signs: ~, Ú, (x), =; x, y … (individual variables) and F(x), G(x,y), H(x,y,z) … (property and relation variables)<A HREF="#56">56</A> where (x) and = may relate only to individuals. To these signs we add yet a third kind of variables f(x), y(x,y), c(x,y,z) etc. which represent object functions; i.e. f(x), y(x,y), etc. denote one-valued functions whose arguments and values are individuals.<A HREF="#57">57</A> A formula which, besides the first mentioned signs of the r.p.c., also contains variables of the third kind, will be called a formula in the wider sense (i.w.s.).<A HREF="#58">58</A> The concepts of "satisfiable" and "universally valid" transfer immediately to formulae i.w.s. and we have the proposition that for every formula i.w.s. A we can give an ordinary formula of the r.p.c. B such that the satisfiability of A is equivalent to that of B. We obtain B from A, by replacing the variables of the third kind f(x), y(x,y) … appearing in A by expressions of the form (,z)F(z,x), (,z)G(z,x y), …, by eliminating the "descriptive" functions on the lines of PM I *14, and by logically multiplying<A HREF="#59">59</A> the resultant formula by an expression, which states that all the F, G … substituted for the f, y … are strictly one-valued with respect to the first empty place. <DD>We now show, that for every problem of the form (x) F(x) (F recursive) there is an equivalent concerning the satisfiability of a formula i.w.s., from which <A HREF="#PROP-X">Proposition X</A> follows in accordance with what has just been said. <DD>Since F is recursive, there is a recursive function F(x) such that F(x) º [F(x) = 0], and for F there is a series of functions F1,F2 … Fn, such that Fn = F, F1(x) = x+1 and for every Fk(1 < k £ n) either <A NAME="EQ18"></A> <UL> 1. (x2 … xm) [Fk(0,x2 … xm) = (Fp(x2 … xm)] (x,x2 … xm) {Fk[F1(x),x2 … xm] = (Fq[x,Fk(x,x2 … xm),x2 … xm]} (18) <DD>p,q < k </UL> </UL>[195]<UL> or <A NAME="EQ19"></A> <UL> 2. (x1 … xm) [Fk(x1 … xm) = Fr(Fi1(c1) … fis(cs))]<A HREF="#60">60</A> (19) r < k, iv < k (for v = 1, 2 … s) </UL> or <A NAME="EQ20"></A> <UL> 3. (x1 … xm) [Fk(x1 … xm) = F1(F1 … F1(0))] (20) </UL> <DD>In addition, we form the propositions: <A NAME="EQ21"></A> (x) ~[F1(x) = 0] & (x y) [F1(x) = F1(y) ® x = y] (21) <A NAME="EQ22"></A> (x) [Fn(x) = 0] (22) <DD>In all the formulae (<A HREF="#EQ18">18</A>), (<A HREF="#EQ19">19</A>), (<A HREF="#EQ20">20</A>) (for k = 2,3, … n) and in (<A HREF="#EQ21">21</A>), (<A HREF="#EQ22">22</A>), we now replace the functions Fi by the function variable fi, the number 0 by an otherwise absent individual variable x0 and form the conjunction C of all the formulae so obtained. <DD>The formula ($x0)C then has the required property, i.e <UL> 1. If (x) [F(x) = 0] is the case, then ($x0)C is satisfiable, since when the functions F1, F2 … Fn are substituted for f1, f2 … fn in ($x0)C they obviously yield a correct proposition. 2. If ($x0)C is satisfiable, then (x) [F(x) = 0] is the case. </UL> <DD>Proof: Let Y1, Y2 … Yn be the functions presumed to exist, which yield a correct proposition when substituted for f1, f2 … fn in ($x0)C. Let its domain of individuals be I. In view of the correctness of ($x0)C for all functions Yi, there is an individual a (in I) such that all the formulae (<A HREF="#EQ18">18</A>) to (<A HREF="#EQ22">22</A>) transform into correct propositions (18') to (22') on replacement of the Fi by Yi and of 0 by a. We now form the smallest sub-class of I, which contains a and is closed with respect to the operation Y1(x). This subclass (I') has the property that every one of the functions Yi, when applied to elements of I', again yields elements of I'. For this holds of Y1 in virtue of the definition of I'; and by reason of (18'), (19'), (20') this property carries over from Yi of lower index to those of higher. The functions derived from Yi by restriction to the domain of individuals I', we shall call Yi'. For these functions also the formulae (<A HREF="#EQ18">18</A>) to (<A HREF="#EQ22">22</A>) all hold (on replacement of 0 by a and Fi by Yi'). <DD>Owing to the correctness of (<A HREF="#EQ21">21</A>) for Y1' and a, we can map the individuals of I' in one-to-one correspondence on the natural numbers, and this in such a manner that a transforms into 0 and the function Y1' into the successor function F1. But, by this mapping, all the functions Yi' transform into the functions Fi, and owing to the correct-</UL>[196]<UL>ness of (<A HREF="#EQ22">22</A>) for Yn' and a, we get (x) [Fn(x) = 0] or (x) [F(x) = 0], which was to be proved.<A HREF="#61">61</A> <DD>Since the considerations leading to <A HREF="#PROP-X">Proposition X</A> (for every specific F) can also be restated within the system P, the equivalence between a proposition of the form (x) F(x) (F recursive) and the satisfiability of the corresponding formula of the r.p.c. is therefore provable in P, and hence the undecidability of the one follows from that of the other, whereby <A HREF="#PROP-IX">Proposition IX</A> is proved.<A HREF="#62">62</A> <HR WIDTH="25%" ALIGN=LEFT> <UL> <A NAME="49">49</A> Here, and in what follows, zero is always included among the natural numbers. <A NAME="50">50</A> 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.) <A NAME="51">51</A> It is not of course necessary that all x1 … xn should actually occur in ci [cf. the example in <A HREF="#27">footnote 27</A>]. <A NAME="52">52</A> 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). <A NAME="53">53</A> These are the w-consistent systems derived from P by addition of a recursively definable class of axioms. <A NAME="54">54</A> 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]. <A NAME="55">55</A> 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 <A HREF="#PROP-IX">Proposition IX</A> the existence of this counter-example is not always demonstrable (in the formal systems in question). <A NAME="56">56</A> 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 <A HREF="#55">footnote 55</A>). <A NAME="57">57</A> And of course the domain of the definition must always be the whole domain of individuals. <A NAME="58">58</A> Variables of the third kind may therefore occur at all empty places instead of individual variables, e.g. y = f(x), F(x,f(y)), G[y(x,f(y)),x] etc. <A NAME="59">59</A> I.e. forming the conjunction. <A NAME="60">60</A> ci(i = 1 … s) represents any complex of the variables x1, x2 … xm, e.g. x1 x3 x2. <A NAME="61">61</A> From <A HREF="#PROP-X">Proposition X</A> 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. <A NAME="62">62</A> <A HREF="#PROP-IX">Proposition IX</A> 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 (x) F(x) (F recursive). </UL> <HR WIDTH="25%" ALIGN=LEFT> 4 <DD>From the conclusions of Section 2 there follows a remarkable result with regard to a consistency proof of the system P (and its extensions), which is expressed in the following proposition: <A NAME="PROP-XI"></A> <DD>Proposition XI: If c be a given recursive, consistent class<A HREF="#63">63</A> of formulae, then the propositional formula which states that c is consistent is not c-provable; in particular, the consistency of P is unprovable in P,<A HREF="#64">64</A> it being assumed that P is consistent (if not, of course, every statement is provable). <DD>The proof (sketched in outline) is as follows: Let c be any given recursive class of formulae, selected once and for all for purposes of the following argument (in the simplest case it may be the null class). For proof of the fact that 17 Gen r is not c-provable,<A HREF="#65">65</A> only the consistency of c was made use of, as appears from 1, page 59; i.e. <A NAME="EQ23"></A> <UL> Wid(c) ® ~Bewc(17 Gen r) (23) </UL> i.e. by (<A HREF="#EQ6.1">6.1</A>): <UL> Wid(c) ® (x) ~[x Bc (17 Gen r)] </UL> <DD>By (<A HREF="#EQ13">13</A>), 17 Gen r = Sb(p 19|Z(p)) and hence: <UL> Wid(c) ® (x) ~[x Bc Sb(p 19|Z(p))] </UL> </UL>[197]<UL> i.e. by (<A HREF="#EQ8.1">8.1</A>): <A NAME="EQ24"></A> <UL> Wid(c) ® (x) Q(x,p) (24) </UL> <DD>We now establish the following: All the concepts defined (or assertions proved) in Sections 2<A HREF="#66">66</A> and 4 are also expressible (or provable) in P. For we have employed throughout only the normal methods of definition and proof accepted in classical mathematics, as formalized in the system P. In particular c (like any recursive class) is definable in P. Let w be the propositional formula expressing Wid(c) in P. The relation Q(x,y) is expressed, in accordance with (<A HREF="#EQ8.1">8.1</A>), (<A HREF="#EQ9">9</A>) and (<A HREF="#EQ10">10</A>), by the relation-sign q, and Q(x,p), therefore, by r [since by (<A HREF="#EQ12">12</A>) r = Sb(q 19|Z(p))] and the proposition (x) Q(x,p) by 17 Gen r. <DD>In virtue of (<A HREF="#EQ24">24</A>) w Imp (17 Gen r) is therefore provable in P<A HREF="#67">67</A> (and a fortiori c-provable). Now if w were c-provable, 17 Gen r would also be c-provable and hence it would follow, by (<A HREF="#EQ23">23</A>), that c is not consistent. <DD>It may be noted that this proof is also constructive, i.e. it permits, if a proof from c is produced for w, the effective derivation from c of a contradiction. The whole proof of <A HREF="#PROP-XI">Proposition XI</A> can also be carried over word for word to the axiom-system of set theory M, and to that of classical mathematics A,<A HREF="#68">68</A> and here too it yields the result that there is no consistency proof for M or for A which could be formalized in M or A respectively, it being assumed that M and A are consistent. It must be expressly noted that <A HREF="#PROP-XI">Proposition XI</A> (and the corresponding results for M and A) represent no contradiction of the formalistic standpoint of Hilbert. For this standpoint presupposes only the existence of a consistency proof effected by finite means, and there might conceivably be finite proofs which cannot be stated in P (or in M or in A). <DD>Since, for every consistent class c, w is not c-provable, there will always be propositions which are undecidable (from c), namely w, so long as Neg(w) is not c-provable; in</UL>[198]<UL>other words, one can replace the assumption of w-consistency in <A HREF="#PROP-VI">Proposition VI</A> by the following: The statement "c is inconsistent" is not c-provable. (Note that there are consistent c's for which this statement is c-provable.) <DD>Throughout this work we have virtually confined ourselves to the system P, and have merely indicated the applications to other systems. The results will be stated and proved in fuller generality in a forthcoming sequel. There too, the mere outline proof we have given of <A HREF="#PROP-XI">Proposition XI</A> will be presented in detail. <HR WIDTH="25%" ALIGN=LEFT> <UL> <A NAME="63">63</A> C is consistent (abbreviated as Wid(c)) is defined as follows: Wid(c) = ($x) [Form(x) & ~Bewc(x)]. <A NAME="64">64</A> This follows if c is replaced by the null class of formulae. <A NAME="65">65</A> r naturally depends on c (just as p does). <A NAME="66">66</A> From the definition of "recursive" on [179] up to the proof of <A HREF="#PROP-VI">Proposition VI</A> inclusive. <A NAME="67">67</A> That the correctness of w Imp (17 Gen r) can be concluded from (<A HREF="#EQ23">23</A>), is simply based on the fact that–as was remarked at the outset–the undecidable proposition 17 Gen r asserts its own unprovability. <A NAME="68">68</A> Cf. J. v. Neumann, 'Zur Hilbertschen Beweistheorie', Math. Zeitschr. 26, 1927. </UL> <HR WIDTH="25%" ALIGN=LEFT> (Received: 17. xi. 1930.) </UL> <HR WIDTH="100%"> <A HREF="http://www.ddc.net/ygg/etext/godel/index.htm"><IMG SRC="../../images/back2.jpg" ALT="Back" BORDER=0 HEIGHT=30 WIDTH=120></A> Design © 1998 Siegfried. All rights reserved.

Optional Link URL:
Link Title:
Optional Image URL:

[ Follow Ups ] [ Post Followup ] [ debord of directors ] [ FAQ ]

ON FORMALLY UNDECIDABLE PROPOSITIONS OF PRINCIPIA MATHEMATICA AND RELATED SYSTEMS 11

ON FORMALLY UNDECIDABLE PROPOSITIONS
OF PRINCIPIA MATHEMATICA AND RELATED
SYSTEMS 1¹