[173]

ON FORMALLY UNDECIDABLE PROPOSITIONS

OF PRINCIPIA MATHEMATICA AND RELATED

SYSTEMS 1¹

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)² 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]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,⁵ provided that thereby no false propositions of the kind described in footnote 4 become provable.

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 α be any class-sign; by [α; n] we designate that formula which is derived on replacing the free variable in the class-sign α 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]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.

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.

2

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), "S" (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, Sa, SSa, SSSa ... 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)²²:

These abbreviations have the following meanings, and definitions, which would have been familiar to anyone working with formalized arithmetic and first-order logic at the time of Principia Mathematica:

. represents multiplication. (Note that in some formal systems, . is used to represent logical conjunction (the and operator) which here is represented by the symbols & and ∧).

⊃ is the implication bolean operator: (a ⊃ b) is equivalent to (~a ∨ b)

≡ is the equivalence or biconditional operator. Gödel's definition of this is the standard one (which can be verified by looking at its definition in the metamathematics function 32 on page 184): (a ≡ b) :: ((a ⊃ b) ∧ (b ⊃ a)). When ∧ and ⊃ are expanded this becomes: (a ≡ b) :: ~(~(~a ∨ b) ∨ ~(~b ∨ a))

(∃x) is the Exists specifier; it specifies that there is a value for the free variable x that makes the following proposition true. Its definition is: (∃x) p :: ~ (x ∀ ~p)

= is the equal relation. As specified in Gödel's footnote, the definition of (a=b) is via a class variable: (a = b) :: a₂ ∀ (a₂(a) ⊃ a₂(b)) or (given the definition of ⊃ above) (a = b) :: a₂ ∀ (~(a₂(a)) ∨ a₂(b))

I.

Gödel uses only three of the Peano postulates; the others are supplanted by the axion-schemata defined later.

1. ~(Sx₁ = 0)

Zero is the successor of no number. Expanded into the basic signs, the axiom is: ~(a₂ ∀ (~(a₂(x₁)) ∨ a₂(0)))

This is the smallest axiom in the entire system (although there are smaller theorems, such as 0=0).

2. Sx₁ = Sy₁ ⊃ x₁ = y₁

If x+1 = y+1 then x=y. Expanding the ⊃ operator we get: ~(Sx₁ = Sy₁) ∨ (x₁ = y₁) And expanding the = operators we get: ~(a₂ ∀ (~(a₂(Sx₁)) ∨ a₂(Sy₁))) ∨ (a₂ ∀ (~(a₂(x₁)) ∨ a₂(y₁)))

3. x₂(0).x₁ ∀ (x₂(x₁) ⊃ x₂(fx₁)) ⊃ x₁ ∀ (x₂(x₁))

The principle of mathematical induction: If something is true for x=0, and if you can show that whenever it is true for y it is also true for y+1, then it is true for all whole numbers x.

[178]II. Every formula derived from the following schemata by substitution of any formulae for p, q and r.

1. p ∨ p ⊃ p

2. p ⊃ p ∨ q

3. p ∨ q ⊃ q ∨ p

4. (p ⊃ q) ⊃ (r ∨ p ⊃ r ∨ q)

III. Every formula derived from the two schemata

1. v ∀ (a) ∨ Subst a(v|c)

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

1. (∃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):

1. 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] "0" ... 1 "S" ... 3 "~" ... 5 "∨" ... 7 "∀" ... 9 "(" ... 11 ")" ... 13

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 Φ(a) the number corresponding to the basic sign or series of basic signs a.

Here is an example Gödel number for a string of symbols:

The smallest theorem in the formal system is "0=0", which expands to a₂ ∀ (~(a₂(0)) ∨ a₂(0)). This formula has 16 basic signs, and the Gödel number 2¹⁷²3⁹5¹¹7⁵11¹¹13¹⁷²17¹¹19¹23¹³29¹³31⁷37¹⁷²41¹¹43¹47¹³53¹³ ≅ 1.97231222789×10¹⁰¹⁵.

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=Φ(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²⁵ φ(x₁,x₂,...x_n) is said to be recursively defined by the number-theoretic functions υ(x₁,x₂,...x_n-1) and μ(x₁,x₂,...x_n+1), if for all x₂, ... x_n, k²⁶ the following hold:

φ(0,x₂,...x_n) = υ(x₂,...x_n)

φ(k+1,x₂,...x_n) = μ(k,φ(k,x₂,...x_n),x₂,...x_n). (2)

Gödel uses the term recursive to refer to what is now called primitive recursive.

A number-theoretic function φ is called recursive, if there exists a finite series of number-theoretic functions φ₁, φ₂, ... φ_n which ends in φ and has the property that every function φ_k of the series is either recursively defined

[180]by two of the earlier ones, or is derived from any of the earlier ones by substitution,²⁷ or, finally, is a constant or the successor function x+1. The length of the shortest series of φ_i, which belongs to a recursive function φ, is termed its degree. A relation R(x₁,x₂,...x_n) among natural numbers is called recursive,²⁸ if there exists a recursive function φ(x₁,x₂,...x_n) such that for all x₁, x₂, ... x_n

R(x₁,x₂,...x_n) ≡ [φ(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).

This is the first time the & operator is mentioned. This is the conjunction operator, commonly called and and represented by the symbol ∧. As evidenced by definition 32 below, Gödel's definition of & includes 5 pairs of brackets: (a & b) :: ~((~(a)) ∨ (~(b)))

III. If the functions φ(χ) and υ(η) are recursive, so also is the relation: φ(χ) = υ(η).³⁰

IV. If the function φ(χ) and the relation R(x,η) are recursive, so also then are the relations S, T

S(χ,η) ~ (∃x)[x <= φ(χ) & R(x,η)]:> T(χ,η) ~ (x)[x <= φ(χ) → R(x,η)]:>

and likewise the function υ

υ(χ,η) = ε x [x <= φ(χ) & R(x,η)]:>

where ε x 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 ~, ∨, =

α(x), β(x,y), γ(x,y)

namely

α(0) = 1; α(x) = 0 for x != 0 β(0,x) = β(x,0) = 0; β(x,y) = 1, if x, y both != O

[181] γ(x,y) = 0, if x = y; γ(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 ρ(x,η) such that

R(x,η) ≡ [ρ(x,η) = 0].

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

Χ(0,η) = 0 Χ(n+1,η) = (n+1).a + Χ(n,η).α(a)³¹

where

a = α[α(ρ(0,η))].α[ρ(n+1,η)].α[Χ(n,η)].

Χ(n+1,η) is therefore either = n+1 (if a = 1) or = Χ(n,η) (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,η) & R(n+1,η) & [Χ(n,η) = 0].

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

υ(χ,η) = C(φ(χ),η) S(χ,η) ≡ R[υ(χ,η)),η)]

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]

1. x/y ≡ (∃z)[z <= x & x = y.z]:>³³

x is divisible by y.³⁴

2. Prim(x) ≡ ~(∃z)[z <= x & z != 1 & z != x & x/z] & x > 1:>

x is a prime number.

3. 0 Pr x ≡ 0

(n+1) Pr x ≡ ε y [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.^34a

4. 0! ≡ 1

(n+1)! ≡ (n+1).n!

5. Pr(0) ≡ 0

Pr(n+1) ≡ ε y [y <= {Pr(n)}! + 1 & Prim(y) & y > Pr(n)]:>

Pr(n) is the n-th prime number (in order of magnitude).

6. n Gl x ≡ ε y [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).

7. l(x) ≡ ε y [y <= x & y Pr x > 0 & (y+1) Pr x = 0]:>

l(x) is the length of the series of numbers assigned to x.

8. x * y ≡ ε z [z <= [Pr{l(x)+l(y)}]^x+y & (n)[n <= l(x) → n Gl z = n Gl x] & (n)[0 <= l(y) → {n+l(x)} Gl z = n Gl y]]:>

x * y corresponds to the operation of "joining together" two finite series of numbers.

9. R(x) ≡ 2^x

R(x) corresponds to the number-series consisting only of the number x (for x > 0:>).

10. 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 ")"].

11. n Var x ≡ (∃z)[13 <= x & Prim(z) & x = zⁿ] & n != 0:>

x is a variable of n-th type.

12. Var(x) ≡ (∃n)[n <= x & n Var x]:>

x is a variable.

Note, the type of a variable is always less than its Gödel-number, because the Gödel number of a variable is p^t where p is a prime greater than 13 and t is the type.

13. Neg(x) ≡ R(5) * E(x)

Neg(x) is the negation of x.

Note brackets are added: the negation of x is constructed by adding 3 symbols, becoming "~(x)".

[183]

14. x Dis y ≡ E(x) * R(7) * E(y)

x Dis y is the disjunction of x and y.

Again, brackets are added: disjunction of x and y is "(x) ∨ (y)".

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

Generalizing a WFF with the variable x only makes sense if the WFF contains x as a free variable. The syntax adds four symbols: "x ∀ (y)"

16. 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 'S' before x."

17. Z(n) ≡ n N [R(1)]

Z(n) is the number-sign for the number n.

18. Typ₁'(x) ≡ (∃m,n){m,n <= x & [m = 1 ∨ 1 Var m] & x = n N [R(m)]}:>^34b

x is a sign of first type.

19. Typ_n(x) ≡ [n = 1 & Typ₁'(x)] ∨ [n > 1 & (∃v){v <= x & n Var v & x = R(v)}]:>

x is a sign of n-th type.

20. Elf(x) ≡ (∃y,z,n)[y,z,n <= x & Typ_n(y) & Typ_n+1(z) & x = z * E(y)]:>

x is an elementary formula.

21. Op(x,y,z) ≡ x = Neg(y) ∨ x = y Dis z ∨ (∃v)[v <= x & Var(v) & x = v Gen y]:>

x is derived from y (and if applicable z) by being the Gödel-number of ~(y), (y)∨(z), or v∀(y).

22. FR(x) ≡ (n){0 <= 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.

23. Form(x) ≡ (∃n){n <= (Pr[l(x)²])^x.[l(x)]2 & FR(n) & x = [l(n)] Gl n}³⁵:>

x is a formula (i.e. last term of a series of formulae n).

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

The variable v is bound at the n-th place in x.

[184]

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

26. v Fr x ≡ (∃n)[n <= l(x) & v Fr n,x]:>

v occurs in x as a free variable.

27. Su x(n|y) ≡ ε z {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 <= l(x):>).

28. 0 St v,x ≡ ε n {n <= l(x) & v Fr n,x & not (∃p)[n <= l(x) & v Fr p,x]}:>

(k+1) St v,x ≡ ε n {n ∃p)[n < p < k St v,x & v Fr p,x]}:>

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

29. A(v,x) ≡ ε n {n <= l(x) & n St v = 0}:>

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

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) is the concept Subst a(v|b), defined above.³⁷

32. x Imp y ≡ [Neg(x)] Dis y

This is how the definition Gödel is using for the ⊃ operator: Imp represents the ⊃ operator, and it is defined in terms of Neg and Dis (see above); thus we have x ⊃ y :: (~ (x)) ∨ (y).

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

Similarly, x ∧ y :: ~((~(x)) ∨ (~(y)))

x Aeq y ≡ (x Imp y) Con (y Imp x)

Aeq is the biconditional "if and only if" operator, commonly represented by the symbol ↔. "Aeq" comes from the German "Aequivalenz" meaning "equivalence". x ↔ y :: (x ⊃ y) ∧ (y ⊃ x) which expands to ~((~((~(x)) ∨ (y))) ∨ (~((~(y)) ∨ (x))))

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

v ∃ y :: ~(v ∀ (~(y)))

33. n Th x ≡ ε n {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 Th x is the n-th type-lift of x (in the case when x and n Th x are 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]:>

x is a formula derived by substitution in the axiom-schema II, 1. Similarly A₂-Ax, A₃-Ax, A₄-Ax are defined in accordance with the axioms II, 2 to 4.

36. A-Ax(x) ≡ A₁-Ax(x) ∨ A₂-Ax(x) ∨ A₃-Ax(x) ∨ A₄-Ax(x)

x is a formula derived by substitution in an axiom of the sentential calculus.

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

z contains no variable bound in y at a position where v is 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)]}:>

x is a formula derived from the axiom-schema III, 1 by substitution.

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

x is a formula derived from the axiom-schema III, 2 by substitution.

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]}]:>

x is a formula derived from the axiom-schema IV, 1 by substitution.

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)

x is an axiom.

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

[186] 44. Bw(x) ≡ (n){0 <= 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).

45. x B y ≡ Bw(x) & [l(x)] Gl x = y

x is a proof of the formula y.

46. 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.]

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₁ = φ(x₂ ... x_n)⁴⁰ (where φ is a recursive function) and apply mathematical induction on the degree of φ. For functions of the first degree (i.e. constants and the function x+1) the proposition is trivial. Let φ then be of degree m. It derives from functions of lower degree φ₁ ... φ_k by the operations of substitution or recursive definition. Since, by the inductive assumption, everything is already proved for φ₁ ... φ_k, there exist corresponding relation-signs r₁ ... r_k such that (3) and (4) hold. The processes of definition whereby φ is derived from φ₁ ... φ_k (substitution and re-

[187]cursive definition) can all be formally mapped in the system P. If this is done, we obtain from r₁ ... r_k a new relation-sign r⁴¹, for which we can readily prove the validity of (3) and (4) by use of the inductive assumption. A relation-sign r, assigned in this fashion to a recursive relation,⁴² will be called recursive.

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