Gödel’s Proof of Incompleteness
Online English Translation

 

ON  FORMALLY  UNDECIDABLE  PROPOSITIONS  OF  PRINCIPIA  MATHEMATICA  AND RELATED  SYSTEMS 1 [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)[2] and, on the other, the axiom system for set theory of Zermelo-Fraenkel (later extended by J. v. Neumann).[3] These two systems are so extensive that all methods of proof used in mathematics today have been formalized in them, i.e: reduced to a few axioms and rules of inference. It might therefore be assumed that these axioms and rules of inference are also sufficient to decide all mathematical questions which can in any way at all be expressed formally in the systems concerned. It is shown below that this is not the case, and that in both the systems mentioned there are in fact relatively simple problems in the theory of ordinary whole numbers[4] which 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,[5] 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 formulas of a formal system–we restrict ourselves here to the system PM–are, looked at from outside the system, finite series of basic symbols (variables, logical constants and brackets or separation points), and it is easy to state precisely just which series of basic symbols are meaningful formulas and which are not.[6] Proofs, from the formal standpoint, are likewise nothing but finite series of formulas (with certain specifiable characteristics). For meta-mathematical purposes it is naturally immaterial what objects are taken as basic symbols, and we propose to use natural numbers[7] for them. Accordingly, then, a formula is a finite series of natural numbers,[8] and a particular proof-schema is a finite series of finite series of natural numbers. Meta-mathematical concepts and propositions thereby become concepts and propositions concerning natural numbers, or series of them,[9] 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[10] 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 according to its 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:

 

The term class-string will be used to refer to formulas of PM that have just one free variable, and which is of the type of the natural numbers (class of classes). We think of the class-strings as being somehow arranged in a series,[11] and denote the n^th one by R(n); and we note that the concept “class-string” as well as the ordering relation R are definable in the system PM. Let α be any class-string; by [α; n] we designate that formula that is derived by replacing the free variable in the class-string α by the string 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 definitions are all definable in PM, so too is the concept K that is derived from them, i.e: there is a class-string S,[12] such that the formula [S; n] – interpreted according to its content – states that the natural number n belongs to K. S, being a class-string, is identical with some specific R(q), i.e:

 

S = R(q)

 

holds for some specific natural number q. We now show that the proposition [R(q); q] [13] 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 ¬(q ∈ 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,[14] 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 that asserts its own unprovability.[15] The method of proof just exhibited can clearly be applied to every formal system having the following features: firstly, interpreted according to its 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 that is undecidable in the system PM yet turns out to be decided by meta-mathematical 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).

 

---

 

[Footnotes to Part 1]

 

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

[2] A. Whitehead and B. Russell, Principia Mathematica, 2nd edition, Cambridge 1925. In particular, we also reckon among the axioms of PM the axiom of infinity (in the form: there exist denumerably many individuals), and the axioms of reducibility and of choice (for all types).

[3] Cf. A. Fraenkel, ‘Zehn Vorlesungen über die Grundlegung der Mengenlehre’, Wissensch. u. Hyp., Vol. XXXI;
J. v. Neumann, ‘Die Axiomatisierung der Mengenlehre’, Math. Zeitschr. 27, 1928, Journ. f. reine u. angew. Math. 154 (1925), 160 (1929).
We may note that in order to complete the formalization, the axioms and rules of inference of the logical calculus must be added to the axioms of set-theory as given in the above-mentioned papers. The remarks that follow also apply to the formal systems presented in recent years by D. Hilbert and his colleagues (so far as these have yet been published).
Cf. D. Hilbert, Math. Ann. 88, Abh. aus d. math. Sem. der Univ. Hamburg I (1922), VI (1928);
P. Bernays, Math. Ann. 90;
J. v. Neumann, Math. Zeitsehr. 26 (1927);
W. Ackermann, Math. Ann. 93.

[4] i.e: more precisely, there are undecidable propositions in which, besides the logical constants ¬ (not), ∨ (or), (x) (for all) and = (identical with), there are no other concepts beyond + (addition) and . (multiplication), both referring to natural numbers, and where the prefixes (x) can also refer only to natural numbers.

[5] In this connection, such axioms in PM are only counted as distinct axioms where they do not arise from others purely by change of type.

[6] Here and in what follows, we shall always understand the term “formula of PM” to mean a formula written without abbreviations (i.e: without use of definitions). Definitions serve only to abridge the written text and are therefore in principle superfluous.

[7] i.e: we map the basic symbols by a one-to-one correspondence onto the natural numbers (as is actually done in the section [The Gödel numbering system]).

[8] i.e: a mapping of a section of the number series onto natural numbers. (Numbers cannot in fact be put into a spatial order.)

[9] In other words, the above-described procedure provides an isomorphic image of the system PM in the domain of arithmetic, and all meta-mathematical arguments can equally well be conducted in this isomorphic image. This occurs in the following outline proof, i.e: “formula”, “proposition”, “variable”, etc. are always to be understood as the corresponding objects of the isomorphic image.

[10] It would be very simple (though rather laborious) actually to write out this formula.

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

[11a] The ¬ indicates negation. [The original German used a bar over a formula to indicate negation]

[12] Again there is not the slightest difficulty in actually writing out the formula S.

[13] Note that “[R(q); q]” (or – what amounts to the same thing – “[S; q]”) is merely a meta-mathematical 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 actually write out the undecidable proposition itself.

[14] Every epistemological antinomy can likewise be used for a similar undecidability proof.

[15] In spite of appearances, there is nothing circular about such a proposition, since it begins by asserting the unprovability of a completely 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

[Description of the formal system P]

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 claim to demonstrate the existence of undecidable propositions. P is essentially the system obtained by superimposing on the Peano axioms the logic of PM[16] (numbers as individuals, the successor relation as an undefined basic concept).

 

The basic symbols of the system P are the following:

 

II. Constants: “¬” (not), “∨” (or), “∀” (for all), “0” (zero), “f ” (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.[17]

 

Note: Variables for two-termed and many-termed functions (relations) are superfluous as basic symbols, 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.[18]

 

By a string of first type we understand a combination of symbols of the form:

 

a, fa, ffa, fffa … etc.

 

where a is either 0 or a variable of first type. In the former case we call such a string a number-string. For n > 1 we understand by a string of n^th type the same as variable of n^th type.

 

Combinations of strings of the form a(b), where b is a string of n^th and a a string of (n + 1)^th type, we call elementary formulas. The class of formulas we define as the smallest class[19] containing all elementary formulas 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 which has 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-string and for n = 1 also a class-string.

 

By Subst a( ^v⁄_b ) (where a stands for a formula, v a variable and b a string 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.[20] 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.

 

 

[Axioms of the formal system P]

The following formulas (I-V) are called axioms (they are set out with the help of the customarily defined abbreviations: ∧, ⊃ , ≡, (∃x), ∀, = [21] and subject to the usual conventions about omission of parentheses):[22]

 

I.

1. ¬(fx₁ = 0)
2. fx₁ = fy₁ ⊃ x₁ = y₁
3. x₂(0) ∧ x₁∀ (x₂(x₁) ⊃ x₂(fx₁)) ⊃ x₁∀ (x₂(x₁))

 

II. Every formula derived from the following schemata by substitution of any formulas 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 string of the same type as v, provided that c contains no variable which is bound in a at a place where v is free.[23]

 

IV. Every formula derived from the schema

 

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

 

[Rules of inference of the formal system P]

A formula c is called an immediate consequence of a and b, if a is the formula (¬(b)) ∨ (c), and an immediate consequence of a, if c is the formula v∀ (a), where v denotes any given variable. The class of provable formulas is defined as the smallest class of formulas that contains the axioms and is closed with respect to the relation “immediate consequence of ”.[24]

 

[The Gödel numbering system]

The basic symbols of the system P are now associated by a one-to-one correspondence with natural numbers, as follows:

 

Furthermore, variables of type n are given numbers of the form pⁿ (where p is a prime number > 13). Hence, for every finite series of basic symbols (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 by a one-to-one correspondence) on to natural numbers, by letting the number 2ⁿ¹, 3ⁿ² p_k^nk 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 by a one-to-one correspondence, not only to every basic symbol, but also to every finite series of such symbols. We denote by Φ(a) the number corresponding to the basic symbol or series of basic symbols a. Suppose now one is given a class or relation R(a₁,  a₂, … a_n) of basic symbols or series of such. We assign to it that class (or relation) R(x₁, x₂, … x_n) of natural numbers that holds for x₁, x₂, … x_n if and only if 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 [with a colored background] those classes and relations of natural numbers that have been assigned in this fashion to such previously defined meta-mathematical 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 formulas a such that neither a nor the negation of a are provable formulas.

 

[Recursion]

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[25] Φ(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 [26] the following hold:

 

Φ(0, x₂, …x_n) = Ψ(x₂, …x_n)
Φ(k + 1, x₂, …x_n) = μ(k, Φ(k, x₂, …x_n), x₂, …x_n). (2)

 

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 by two of the earlier ones, or is derived from any of the earlier ones by substitution,[27] or, finally, is a constant or the successor function x + 1. The length of the shortest series of Φ_ithat belongs to a recursive function Φ, is termed its degree. A relation R(x₁, x₂, …x_n) among natural numbers is called recursive,[28] 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] [29]

 

[Propositions I-IV]

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 Φ(χ) and Ψ(η) are recursive, so also is the relation: Φ(χ) = Ψ(η). [30]

 

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 ≠ 0
γ(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:

 

 

where

 

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

 

χ(n + 1, η) is therefore either = n + 1 (if a = 1) or = χ(n, η) (if a = 0).[32] 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, η) already holds, then χ(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 Relations 1‑46]

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, where each is defined from the earlier ones by means of the operations referred to in Propositions I to IV. Generally speaking, several such definition steps permitted by the Propositions I to IV are collapsed into one. Each of the functions (relations) 1-45, containing, for example, the concepts “formula”, “axiom”, and “immediate consequence”, is therefore recursive.

 

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

 

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

 

 

[Proposition V]

The following proposition is an exact expression of a fact that can be roughly formulated in this manner: every recursive relation is definable in the system P (interpreted according to its content), regardless of what interpretation is given to the formulas of P:

 

Proposition V: To every recursive relation R(x₁ … x_n) there corresponds an n-place relation-string r (with the free variables[38] 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(x1) … Z(xn)} ]} (3)

     ¬R(x₁ … x_n) ⇒ Bew{Neg Sb[r  ^{u₁ … u_n} ⁄ _{Z(x1) … Z(xn)} ]} (4)

 

We are content here with indicating the proof of this proposition in outline, since it offers no difficulties in principle and is somewhat involved.[39] We prove the proposition for all relations R(x₁ … x_n) of the form: x₁ = Φ(x₂ … x_n) [40] (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-strings r₁ … r_k such that (3) and (4) hold. The processes of definition whereby Φ is derived from Φ₁ … Φ_k (substitution and recursive definition) can all be formally mapped to the system P. If this is done, we obtain from r₁ … r_k a new relation-string r [41], for which we can readily prove the validity of (3) and (4) by use of the inductive assumption. A relation-string r, assigned in this fashion to a recursive relation,[42] will be called recursive.

 

We now come to the objective of our assertions:

 

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

 

[Proposition VI]

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

 

Proposition VI: For every ω-consistent recursive class c of formulas there are corresponding recursive class-strings 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 formulas. We define:

 

Bw_c(x) ≡ (n)[n ≤ l(x) ⇒ Ax(n Gl x) ∨ (n Gl x) ∈ c ∨ (∃p,q){0 < p,q < n & Fl(n Gl x, p Gl x, q Gl x)}] & l(x) > 0 (5)

(cf. the analogous relation 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 relations 45, 46)

 

The following clearly hold:

 

(x)[Bew_c(x) ≡ x ∈ Flg(c)] (7)

 

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

 

We now define the relation:

 

Q(x, y) ≡ ¬{x B_c[Sb(y  ¹⁹⁄_Z(y) )]} (8.1)

 

Since x B_c y (according to (6), (5)) and Sb(y  ¹⁹⁄_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-string q (with the free variables 17, 19) such that

 

¬{x B_c [Sb(y  ¹⁹⁄_Z(y) )]} ⇒ Bew_c[Sb(q  ¹⁷⁄_Z(x)    ¹⁹⁄_Z(y) )] (9)

 

                x B_c [Sb(y  ¹⁹⁄_Z(y) )] ⇒ Bew_c[Neg Sb(q  ¹⁷⁄_Z(x)   ¹⁹⁄_Z(y) )] (10)

We put

 

p = 17 Gen q (11)

(p is a class-string with the free variable 19)

 

and

 

r = Sb(q  ¹⁹⁄_Z(p) ) (12)

(r is a recursive class-string with the free variable 17). [43]

 

Then

Sb(p  ¹⁹⁄_Z(p) ) = Sb ([17 Gen q]  ¹⁹⁄_Z(p) ) = 17 Gen Sb(q  ¹⁹⁄_Z(p) ) = 17 Gen r [44] (13)

 

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

 

Sb(q  ¹⁷⁄_Z(x)   ¹⁹⁄_Z(p) ) = Sb(r  ¹⁷⁄_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  ¹⁷⁄_Z(x) )] (15)

 

             x B_c (17 Gen r) ⇒ Bew_c[Neg Sb(r  ¹⁷⁄_Z(x) )] (16)

 

Hence:

 

 

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 proven intuitionistically:

 

For a given recursively defined class c of formulas:

If a formal proof (in the class c) can be given for the propositional formula 17 Gen r (which is actually definable) we can in fact state:

 

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

 

2. For any given n, a proof for Sb(r  ¹⁷⁄_Z(n) ), i.e: a formal proof of 17 Gen r would in fact lead to the actual demonstration of an ω-inconsistency.

 

We shall call a relation (class) of natural numbers R(x₁ … x_n) decisional-definite, if there is an n-place relation-string r such that (3) and (4) hold (cf. Proposition V). In particular, therefore, by Proposition V, every recursive relation is decisional-definite. Similarly, a relation-string will be called decisional-definite, if it be assigned in this manner to a decisional-definite relation. It is, then sufficient, that for the existence of undecidable propositions, that the class c is assumed to be ω-consistent and decisional-definite. For the property of being decisional-definite carries over from c to x B_c y (cf. (5), (6)) and to Q(x, y) (cf. 8.1), and only these facts are applied in the above proof. The undecidable proposition has in this case the form v Gen r, where r is a decisional-definite class-string (it is in fact sufficient that c is decisional-definite in the system extended by c).

 

If, instead of ω-consistency, only consistency itself 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. Proposition VI: 1. “17 Gen r is not c-provable” ) and from ¬Bew_c(17 Gen r) it follows, according to (15), that for every number x, Sb(r  ¹⁷⁄_Z(x) ) is c-provable, and hence that Sb(r  ¹⁷⁄_Z(x) ) is not c-provable for any number.

 

By adding Neg(17 Gen r) to c, we obtain a consistent but not ω-consistent class of formulas c′. c′ is consistent, since otherwise 17 Gen r would be c-provable. However c′ is not ω-consistent, since by ¬Bew_c(17 Gen r) and (15) we have:

 

(x) Bew_cSb(r  ¹⁷⁄_Z(x) )

 

and hence we also have that:

 

(x) Bew_c′Sb(r  ¹⁷⁄_Z(x) )

 

holds. While on the other hand:

 

Bew_c′[Neg(17 Gen r)]. [46]

 

also holds.

 

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

 

x ∈ c ≡ (∃m,n)[m ≤ x & n ≤ a & n ∈ α & 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 ω-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 symbols 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 ω-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 a system made by adding a recursively definable ω-consistent class of axioms. As can be easily confirmed, the systems that satisfy assumptions 1 and 2 include the Zermelo-Fraenkel and the v. Neumann axiom systems of set theory,[47] 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.[48] 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.[48a]

 

---

 

[Footnotes to Part 2]

 

[16] The addition of the Peano axioms, like all the other changes made to the system PM, serves only to simplify the proof and can in principle be dispensed with.

[17] It is assumed that for every variable type denumerably many combinations of symbols are available.

[18] Non-homogeneous 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.

[19] Regarding this definition (and similar ones occurring later):
cf. J. Lukasiewicz and A. Tarski, ‘Untersuchungen über den Aussagenkalkül’, Comptes Rendus des séances de la Soeiété des Sciences et des Lettres de Varsovie XXIII, 1930, Cl. 111.

[20] Where v does not occur in a as a free variable, we put Subst a( ^v⁄_b ) = a. Note that “Subst” is a term belonging to meta-mathematics.

[21] 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).

[22] To obtain the axioms from the schemata presented (and in the cases of II, III and IV, after carrying out the permitted substitutions), one must therefore also:
1. eliminate the abbreviations.
2. add the suppressed brackets.
Note that the resultant expressions must be “formulas” in the above sense. (Cf. also the exact definitions of the meta-mathematical concepts in the section [The Relations 1‑46].)

[23] c is therefore either a variable or 0 or a string of the form f … f_u where u is either 0 or a variable of type 1. With regard to the concept “free/bound at a place in a”, cf. section I A5 of the work cited in footnote 24.

[24] The rule of substitution becomes superfluous, since we have already dealt with all possible substitutions in the axioms themselves (as is also done in J. v. Neumann, ‘Zur Hilbertschen Beweistheorie’, Math. Zeitschr. 26, 1927).

[25] i.e: its field of definition is the class of non-negative whole numbers (or n-tuples of such), respectively, and its values are non-negative whole numbers.

[26] In what follows, small [italic] letters (with or without indices) are always variables for non-negative whole numbers (failing an express statement to the contrary). [Italics omitted in this translation]

[27] More precisely, by substitution of certain of the foregoing functions at the argument places of one of the preceding functions, e.g. Φ_k(x₁, x₂) = Φ_p[Φ_q(x₁, x₁),Φ_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)).

[28] We include classes among relations (one-place relations). Recursive relations R naturally have the property that for every specific n-tuple of numbers it can be decided whether R(x₁…x_n) holds or not.

[29] For all considerations as to content (more especially also of a meta-mathematical kind) the Hilbert symbolism is used,
cf. Hilbert-Ackermann, Grundzüge der theoretischen Logik, Berlin 1928.

[30] We use [Greek] letters χ, η, as abbreviations for given n-tuple sets of variables, e.g. x₁, x₂ … x_n.

[31] We take it as evident that the functions x + y (addition) and x.y (multiplication) are recursive.

[32] a cannot take values other than 0 and 1, as is evident from the definition of α.

[33] The symbol ≡ is used to mean “equivalence by definition”, and therefore is usable in definitions either for = or for ~ (otherwise the symbolism is of the Hilbert type). [Translator’s note: the symbol ~ does not appear in this translation]

[34] Wherever in the following definitions one of the symbols x∀, ∃x, εx 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).

[35] The bound defined by n ≤ (Pr[l(x)]^2x.[l(x)]2 is calculated as follows: The length of the shortest series of formulas belonging to x can at most be equal to the number of constituent formulas of x. There are however at most l(x) constituent formulas 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 than Pr{[l(x)]²}, their number ≤[l(x)]² and their exponents (which are constituent formulas of x) ≤ x.

[36] Where v is not a variable or x not a formula, then Sb(x  ^v⁄_y ) = x..

[37] Instead of Sb[Sb[x  ^v⁄_y ]  ^w⁄_z ] we write: Sb(x  ^v⁄_y   ^w⁄_z ) (and similarly for more than two variables).

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

[39] Proposition V naturally is based on the fact that for any recursive relation R, it is decidable, for every n-tuple of numbers, from the axioms of the system P, whether the relation R holds or not.

[40] From this it follows immediately that this is valid for every recursive relation, since any such relation is equivalent to 0 = Φ(x₁ … x_n), where Φ is recursive.

[41] In the precise development of this proof, r is of course defined, not indirectly by an interpretation of its content, but by its purely formal structure.

[42] Where the interpretation of the content of r expresses the existence of that corresponding relation.

[43] r is derived in fact, from the recursive relation-string q on replacement of a variable by a specific number (p).

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

[45] “x is c-provable” signifies: x ∈ Flg(c), which by (7), states the same as Bew_c(x).

[45a] Since all assertions of existence that occur in the proof are based on Proposition V, which, as can easily be seen, is intuitionistically irreproachable.

[46] Thus the existence of consistent and non ω-consistent c′s can naturally be proved only on the assumption that a consistent class c′ exists (i.e: that P is consistent).

[47] The proof of assumption 1 is here even simpler than that for the system P, since there is only one kind of basic variable (or two for J. v. Neumann).

[48] Cf. Problem III in D. Hilbert’s lecture: ‘Probleme der Grundlegung der Mathematik’, Math. Ann. 102.

[48a] The real reason for the incompleteness inherent in all formal systems of mathematics – as will be shown in Part II of this paper – is 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 there is at most denumerably many types. It can be shown that the undecidable propositions presented here always become decidable by the adjunction of suitable higher types (e.g. of type ω to the system P). The same applies to the axiom system of set theory.

 

---

 

3

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][49] and the logical constants ∨, ¬, (x), =, where (x) and = are to relate only to natural numbers.[50] 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₀ = Φ(x₁ … x_n), where Φ is recursive, is arithmetical, and apply mathematical induction on the degree of Φ. Let Φ be of degree s (s > 1). Then either

 

1. Φ(x₁ … x_n) = ρ[χ₁(x₁ … x_n), χ₂(x₁ … x_n) … χ_m(x₁ … x_n)] [51]
(where p and all the x′s have degrees smaller than s) or

 

2. Φ(0,x₂ … x_n) = Ψ(x₂ … x_n)
Φ(k + 1,x₂ … x_n) = μ[k,Φ(k,x₂ … x_n),x₂ … x_n]
(where Ψ, μ are of lower degree than s).

 

In the first case we have:

 

x₀ = Φ(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 assumption of induction exist, are equivalent to x₀ = ρ(y₁ … y_m) and y = χ_i(x₁ … x_n). In this case, therefore, x₀ = Φ(x₁ … x_n) is arithmetical.

 

In the second case we apply the following procedure: The relation x₀ = Φ(x₁ … x_n) can be expressed with the help of the concept “series of numbers” (f) [52] as follows.

 

x₀ = Φ(x₁ … x_n) ≡ (∃f){f₀ = Ψ(x₂ … x_n) & (k)[k < x₁ ⇒ f_k + 1 = μ(k,f_k,x₂ … x_n)] & x₀ = f_x1}

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

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

the following then holds:

x₀ = Φ(x₁ … x_n) ≡ (∃f){S(f₀,x₂ … x_n) & (k)[k < x₁ ⇒ T(f^k + 1,k,f_k,x₂ … x_n)] & x₀ = f_x1} (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

 

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(x1 + 1)}}

which, according to (17) and Lemma 1, is equivalent to x₀ = Φ(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[53] 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 ω-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[54] (i.e: formulas of the restricted predicate calculus for which neither universal validity nor the existence of a counter-example is provable).[55]

 

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 formulas which are constructed out of the basic symbols: ¬, ∨, (x), =; x, y … (individual variables) and F(x), G(x,y), H(x,y,z) … (property and relation variables)[56] where (x) and = may relate only to individuals. To these strings we add yet a third kind of variables Φ(x), Ψ(x,y), χ(x,y,z) etc. which represent object functions; i.e: Φ(x), Ψ(x,y), etc. denote one-valued functions whose arguments and values are individuals.[57] A formula which, besides the first mentioned strings of the r.p.c. also contains variables of the third kind, will be called an i.w.s. formula (a formula in the wider sense) .[58] The concepts of “satisfiable” and “universally valid” transfer immediately to i.w.s. formulas and we have the proposition that for every i.w.s. formula A we can give an ordinary r.p.c. formula 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 Φ(x), Ψ(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[59] the resultant formula by an expression, which states that all the F, G … substituted for the Φ, Ψ … hold for a unique value of the first argument place.

 

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

 

Since F is recursive, there is a recursive function Φ(x) such that F(x) ≡ [Φ(x) = 0], and for Φ there is a series of functions Φ₁,Φ₂ … Φ_n, such that Φ_n = Φ, Φ₁(x) = x + 1 and for every Φ_k(1 < k ≤ n) either:

 

1. (x₂ … x_m) [Φ_k(0,x₂ … x_m) = (Φ_p(x₂ … x_m)]

     (x,x₂ … x_m) {Φ_k[Φ₁(x),x₂ … x_m] = (Φ_q[x,Φ_k(x,x₂ … x_m),x₂ … x_m]} (18)

    p,q < k

 

or

2. (x₁ … x_m) [Φ_k(x₁ … x_m) = Φ_r(Φ_i1(χ₁) … Φ_is(χ_s))] [60] (19)

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

or

3. (x₁ … x_m) [Φ_k(x₁ … x_m) = Φ₁(Φ₁ … Φ₁(0))] (20)

 

In addition, we form the propositions:

 

(x) ¬[Φ₁(x) = 0] & (x y) [Φ₁(x) = Φ₁(y) ⇒ x = y] (21)

(x) [Φ_n(x) = 0] (22)

 

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

 

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

 

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

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

 

Proof: Let Ψ₁, Ψ₂ … Ψ_n be the functions presumed to exist, which yield a correct proposition when substituted for Φ₁, Φ₂ … Φ_n in (∃x₀)C. Let its domain of individuals be I. In view of the correctness of (∃x₀)C for all functions Ψ_i, there is an individual a (in I) such that all the formulas (18) to (22) transform into correct propositions (18′) to (22′) on replacement of the Φ_i by Ψ_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 Ψ₁(x). This subclass (I′) has the property that every one of the functions Ψ_i, when applied to elements of I′, again yields elements of I′. For this holds of Ψ₁ in virtue of the definition of I′; and by reason of (18′), (19′), (20′) this property carries over from Ψ_i of lower index to those of higher. The functions derived from Ψ_i by restriction to the domain of individuals I′, we shall call Ψ_i′. For these functions also the formulas (18) to (22) all hold (on replacement of 0 by a and Φ_i by Ψ_i′).

 

Owing to the correctness of (21) for Ψ₁′ 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 Ψ₁′ into the successor function Φ₁. But, by this mapping, all the functions Ψ_i′ transform into the functions Φ_i, and owing to the correctness of (22) for Ψ_n′ and a, we get (x) [Φ_n(x) = 0] or (x) [Φ(x) = 0], which was to be proved.[61]

 

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

 

---

 

[Footnotes to Part 3]

 

[49] Here, and in what follows, zero is always included among the natural numbers.

[50] The definition of such a concept must therefore be constructed solely by means of the symbols stated, variables for natural numbers x,y… and the symbols 0 and 1 (function and set variables must not occur). (Any other number-variable may naturally occur in to prefixes in place of x.

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

[52] f signifies here a variable, whose domain of values consists of series of natural numbers. f_k denotes the k + 1 ^th term of a series f (f₀ being the first).

[53] These are the ω-consistent systems derived from P by addition of a recursively definable class of axioms.

[54] Cf. Hilbert-Ackermann, Grundzüge der theoretischen Logik.
In the system P, formulas of the restricted predicate calculus are to be understood as those derived from the formulas of the restricted predicate calculus of PM on replacement of relations by classes of higher type, as indicated in Part 2: description of the system P.

[55] In my article ‘Die Vollständigkeit der Axiome des logischen Funktionenkalküls’, Monatsh. f. Math. u. Phys. XXXVII, 2, I have shown of every formula of the restricted predicate calculus that it is either demonstrable as universally valid or else that a counter-example exists; but in virtue of Proposition IX the existence of this counter-example is not always demonstrable (in the formal systems in question).

[56] D. Hilbert and W. Ackermann, in the work already cited, do not include the symbol = in the restricted predicate calculus. But for every formula in which the symbol = occurs, there exists a formula without this symbol, which is satisfiable if and only if the original one is (cf. the article cited in footnote 55).

[57] In fact the domain of the definition must always be the whole domain of individuals.

[58] Variables of the third kind may occur at all argument places instead of individual variables, e.g.y = Φ(x), F(x,Φ(y)), G[Ψ(x,Φ(y)),x] etc.

[59] i.e: forming the conjunction.

[60] χ_i(i = 1 … s) represents any complex of the variables x₁, x₂ … x_m, e.g. x₁ x₃ x₂..

[61] From Proposition X it follows, for example, that the Fermat and Goldbach problems would be soluble, if one had solved the decision problem for the r.p.c.

[62] Proposition IX naturally holds also for the axiom system of set theory and its extensions by recursively definable ω-consistent classes of axioms, since in these systems also there certainly exist undecidable propositions of the form (x) F(x) (F recursive).

 

---

 

4

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[63] of formulas, then the propositional formula which states that c is consistent is not c-provable; in particular, the consistency of P is unprovable in P,[64] 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 formulas, 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,[65] only the consistency of c was made use of, as appears from Proposition VI: 1. “17 Gen r is not c-provable” ; 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  ¹⁹⁄_Z(p) )

and hence:

Wid(c) ⇒ (x) ¬[x B_c Sb(p  ¹⁹⁄_Z(p) )]

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[66] 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-string q, and Q(x,p), therefore, by r [since by (12) r = Sb(q  ¹⁹⁄_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[67] (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 actual 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,[68] 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 other words, one can replace the assumption of ω-consistency in Proposition VI 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.

 

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. In that sequel the outline proof we have given of Proposition XI will also be presented in detail.

 

---

 

[Footnotes to Part 4]

 

[63] c is consistent (abbreviated as Wid(c)) is defined as follows: Wid(c) = (∃x) [Form(x) & ¬Bew_c(x)] .

[64] This follows if c is replaced by the null class of formulas.

[65] r naturally depends on c (just as p does).

[66] From the definition of “recursive” on up to the proof of Proposition VI inclusive.

[67] 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.

[68] Cf. J. v. Neumann, ‘Zur Hilbertschen Beweistheorie’, Math. Zeitschr. 26, 1927.