Note: Full functionality of this website requires JavaScript to be enabled in your browser.
Gödel’s Proof of Incompleteness  Online English Translation
Page last updated 15 May 2021
This is an updated online English translation of Gödel’s Proof of Incompleteness (Footnote:
Kurt Gödel: “Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I”, Monatshefte für mathematik und physik 38, no. 1 (1931): 173198.)
with clickable crossreferences, and which takes account of Meltzer’s, (Footnote:
Bernard Meltzer: On Formally Undecidable Propositions of Principia Mathematica and Related Systems (Translation of the German original by Gödel). Basic Books, 1962. Reprinted, Dover, 1992. ISBN: 0486669807.)
van Heijenoort’s (Footnote:
Jean Van Heijenoort: From Frege to Gödel: A Source Book in Mathematical Logic, publisher: Harvard University Press, details at From Frege to Gödel: A Source Book in Mathematical Logic.)
and Mendelson’s (Footnote:
Elliott Mendelson: On formally undecidable propositions of Principia Mathematica and related systems I The Journal of Symbolic Logic 31.3 (1966): 484494.
Also published in the book:
Martin Davis: The undecidable, Basic papers on undecidable propositions, unsolvable problems and computable functions, edited by Martin Davis, Raven Press, Hewlett, New York, 1965.)
English translations of the original German, and also the reviews of Meltzer’s and Mendelson’s translations by Stefan BauerMengelberg (Footnote:
Stefan BauerMengelberg: Review of Meltzer’s translation, The Journal of Symbolic Logic, Vol. 30, No. 3 (Sept., 1965), pp. 359362,
Stefan BauerMengelberg: Review of Mendelson’s translation, The Journal of Symbolic Logic, Vol. 31, No. 3 (Sept., 1966), pp. 484494.)
which point out some errors in those translations. The original German text can be viewed at:
Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.
English translation by James R Meyer, copyright 20142022 www.jamesrmeyer.com
Notes:
In this translation, text in italics enclosed in square brackets is additional to the original text, e.g. [Recursion]; this is for convenience for the reader.
It is important to note that in the paper a number may correspond by Gödel numbering to a concept such as a formula of the formal system. Gödel often refers to such numbers by the corresponding concept in italic font. This is a common source of confusion, and so in this translation to help readers to avoid confusion, these references are represented here by italic words which also have a colored background, e.g. formula, variable (see The Gödel numbering system).
Gödel uses the terminology for the universal quantifier as x∀ (a), rather than ∀x (a). The ordering of the symbols in this way is used in definitions later in the text so it is preferable to retain this in the translation.
Meltzer’s and van Heijenoort’s translations both use the term “sign” to refer both to single symbols and to sequences of symbols which can be confusing. Here the term “string” is used to refer to sequences of symbols.
An online guide to help readers follow the proof is available on this site at A Step by Step Guide to Gödel’s Incompleteness Proof
Footnotes:
Contents
 Part 1

Part 2
 Description of the formal system P
 The axioms of the system P
 The rules of inference of the system P
 The Gödel numbering system
 Recursion
 Propositions IIV
 The Relations 146
 1 2 3 4 5 6 7 8 9 10
 11 12 13 14 15 16 17 18 19 20
 21 22 23 24 25 26 27 28 29 30
 31 32 33 34 35 36 37 38 39 40
 41 42 43 44 45 46
 Proposition V
 Proposition VI
 Part 3
 Part 4
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]}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.
and, on the other, the axiom system for set theory of ZermeloFraenkel (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,
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]}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 notA are provable, in the following manner:
Proofs, from the formal standpoint, are likewise nothing but finite series of formulas (with certain specifiable characteristics). For metamathematical 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 proofschema 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,^{[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”, “proofschema”, “provable formula” are definable in the system PM,
The term classstring 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 classstrings as being somehow arranged in a series,^{[11]}[α; n] we designate that formula that is derived by replacing the free variable in the classstring α by the string for the natural number n. The threeterm relation x = [y; z] also proves to be definable in PM. We now define a class K of natural numbers, as follows:
and denote the n^{th} one by R(n); and we note that the concept “classstring” as well as the ordering relation R are definable in the system PM. Let α be any classstring; by
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 classstring 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 classstring, 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]}[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.
since the undecidable proposition
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 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).
[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 settheory as given in the abovementioned 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 onetoone 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 abovedescribed procedure provides an isomorphic image of the system PM in the domain of arithmetic, and all metamathematical arguments can equally well be conducted in this isomorphic image. This occurs in the following outline proof, i.e. “formula”, “proposition”, “variable”, etc. are always to be understood as the corresponding objects of the isomorphic image.
[10]It would be very simple (though rather laborious) actually to write out this formula.
[11]Perhaps according to the increasing sums of their terms and, for equal sums, in alphabetical order.
[11a]The ¬ 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 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 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” (nought), “f ” (the successor of), “(”, “)” (brackets).
II. Variables of first type (for individuals, i.e. natural numbers including 0): “x_{1}”, “y_{1}”, “z_{1}”, …
Variables of second type (for classes of individuals): “x_{2}”, “y_{2}”, “z_{2}”, …
Variables of third type (for classes of classes of individuals): “x_{3}”, “y_{3}”, “z_{3}”, …
and so on for every natural number as type.^{[17]}
Note: Variables for twotermed and manytermed 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 numberstring. 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]}¬(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 nplace relationstring and for n = 1 also a classstring.
containing all elementary formulas and, also, along with any a and b the following:
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 typelift 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 (IV) 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_{1} = 0)
2. fx_{1} = fy_{1} ⊃ x_{1} = y_{1}
3. x_{2}(0) ∧ x_{1}∀ (x_{2}(x_{1}) ⊃ x_{2}(fx_{1})) ⊃ x_{1}∀ (x_{2}(x_{1}))
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 typelift (and this formula itself):
1. x_{1}∀ (x_{2}(x_{1}) ≡ y_{2}(x_{1})) ⊃ x_{2} = y_{2}.
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 onetoone correspondence with natural numbers, as follows:
“0”  …  1 
“f ”  …  3 
“¬”  …  5 
“∨”  …  7 
“∀”  …  9 
“(”  …  11 
“)”  …  13 
Furthermore, variables of type n are given numbers of the form p^{n} (where p is a prime number > 13). Hence, for every finite series of basic symbols (and so also to every formula) there corresponds, onetoone, a finite series of natural numbers. These finite series of natural numbers we now map (again by a onetoone correspondence) on to natural numbers, by letting the number 2^{n1}, 3^{n2} p_{k}^{nk} correspond to the series n_{1}, n_{2}, … n_{k}, where p_{k} denotes the k^{th} prime number in order of magnitude. A natural number is thereby assigned by a onetoone 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_{1}, a_{2}, … a_{n}) of basic symbols or series of such. We assign to it that class (or relation) R(x_{1}, x_{2}, … x_{n}) of natural numbers that holds for x_{1}, x_{2}, … x_{n} if and only if there exist a_{1}, a_{2}, … a_{n} such that x_{i} = Φ(a_{i}) (i = 1, 2, … n) and R(a_{1}, a_{2}, … 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 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 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 numbertheoretic function^{[25]}Φ(x_{1}, x_{2}, …x_{n}) is said to be recursively defined by the numbertheoretic functions Ψ(x_{1}, x_{2}, …x_{n1}) and μ(x_{1}, x_{2}, …x_{n + 1}), if for all x_{2}, … x_{n}, k ^{[26]} the following hold:
Φ(0, x_{2}, …x_{n}) = Ψ(x_{2}, …x_{n})
Φ(k + 1, x_{2}, …x_{n}) = μ(k, Φ(k, x_{2}, …x_{n}), x_{2}, …x_{n}). (2)
A numbertheoretic function Φ is called recursive, if there exists a finite series of numbertheoretic functions Φ_{1}, Φ_{2}, … Φ_{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 Φ_{i}that belongs to a recursive function Φ, is termed its degree. A relation R(x_{1}, x_{2}, …x_{n}) among natural numbers is called recursive,^{[28]} if there exists a recursive function Φ(x_{1}, x_{2}, …x_{n}) such that for all x_{1}, x_{2},… x_{n}
R(x_{1}, x_{2}, …x_{n}) ≡ [Φ(x_{1}, x_{2}, …x_{n}) = 0] ^{[29]}
[Propositions IIV]
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 numbertheoretic 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:
χ(0, η) = 0
χ(n + 1, η) = (n + 1) . a + χ(n, η) . α(a) ^{[31]}
where
a = α[α(ρ(0, η))] . α[ρ(n + 1, η)].α[χ(n, η)].
χ(n + 1, η) is therefore either = n + 1 (if a = 1) or = χ(n, η) (if a = 0).^{[32]}i.e. if:
The first case clearly arises if and only if all the constituent factors of a are 1,
¬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 146]
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) 145, 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) 145, containing, for example, the concepts “formula”, “axiom”, and “immediate consequence”, is therefore recursive.
1.
x/y ≡ (∃z)[z ≤ x & x = y · z] ^{[33]}
x is divisible by y. ^{[34]}
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} & ¬ 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 < 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.
9.
R(x) ≡ 2^{x}
R(x) corresponds to the numberseries 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 symbols “(” and “)”].
11.
n Var x ≡ (∃z)[13 < z ≤ x & Prim(z) & x = z^{n}] & n ≠ 0
x is a variable of n^{th} type.
12.
Var(x) ≡ (∃n)[n ≤ x & n Var x]
x is a variable.
13.
Neg(x) ≡ R(5) * E(x)
Neg(x) is the negation of x.
14.
x Dis y ≡ E(x) * R(7) * E(y)
x Dis y is the disjunction of x and 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).
16.
0 N x ≡ x
(n + 1) N x ≡ R(3) * n N x
n N x corresponds to the operation: “nfold prefixing of the symbol ‘f’ before x.”
17.
Z(n) ≡ n N [R(1)]
Z(n) is the numberstring for the number n.
18.
Typ_{1}′(x) ≡ (∃m,n){m,n ≤ x & [m = 1 ∨ 1 Var m] & x = n N [R(m)]} ^{[34b]}
x is a string of first type.
19.
Typ_{n}(x) ≡ [n = 1 & Typ_{1}′(x)] ∨ [n > 1 & (∃v){v ≤ x & n Var v & x = R(v)}]
x is a string 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]
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
x is a series of formulas where 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)^{2}])^{x · [l(x)]2} & FR(n) & x = [l(n)] Gl n} ^{[35]}
x is a formula (i.e. last term of a series of formulas 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.
25.
v Fr n,x ≡ Var(v) & Form(x) & v = n Gl x & n ≤ l(x) & ¬(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 < n ≤ l(x)).
28.
0 St v,x ≡ εn {n ≤ l(x) & v Fr n,x & ¬ (∃p)[n < p ≤ l(x) & v Fr p,x]}
(k + 1) St v,x ≡ εn {n < k St v,x & v Fr n,x & (∃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) where 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 where v is free in x.
30.
Sb_{0}(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} ) ^{[36]}
Sb(x ^{v}⁄_{y} ) is the concept Subst a( ^{v}⁄_{b} ), defined above. ^{[37]}
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 ∃x y ≡ Neg{v Gen [Neg(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})]}
n Th x is the n^{th} typelift of x (in the case when x and n Th x are formulas).
To the axioms I, 1 to 3, there correspond three specific numbers, which we denote by z_{1}, z_{2}, z_{3}, and we define:
34.
ZAx(x) ≡ (x = z_{1} ∨ x = z_{2} ∨ x = z_{3})
35.
A_{1}Ax(x) ≡ (∃y)[y ≤ x & Form(y) & x = (y Dis y) Imp y]
x is a formula derived by substitution in the axiomschema II, 1. Similarly A_{2}Ax, A_{3}Ax, A_{4}Ax are defined in accordance with the axioms II, 2 to 4.
36.
AAx(x) ≡ A_{1}Ax(x) ∨ A_{2}Ax(x) ∨ A_{3}Ax(x) ∨ A_{4}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 z & w Geb n,y & v Fr n,y]
z contains no variable bound in y at a position where v is free.
38.
L_{1}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(y ^{v}⁄_{z} )]}
x is a formula derived from the axiomschema III, 1 by substitution.
39.
L_{2}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 axiomschema III, 2 by substitution.
40.
RAx(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 axiomschema IV, 1 by substitution.
To the axiom V, 1 there corresponds a specific number z_{4} and we define:
41.
MAx(x) ≡ (∃n)[n ≤ x & x = n Th z_{4}]
42.
Ax(x) ≡ ZAx(x) ∨ AAx(x) ∨ L_{1}Ax(x) ∨ L_{2}Ax(x) ∨ RAx(x) ∨ MAx(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.
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 Gl x)]} & l(x) > 0
x is a proofschema (a finite series of formulas, where 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) = (∃y)y B x
x is a provable formula. (Bew(x) is the only one of the concepts 146 where it cannot be asserted that it is recursive.)
[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_{1} … x_{n}) there corresponds an nplace relationstring r (with the free variables^{[38]} u_{1}, u_{2}, … u_{n}) such that for every ntuple of numbers (x_{1} … x_{n}) the following hold:
R(x_{1} … x_{n}) ⇒ Bew{Sb[r ^{u1 … un} ⁄ _{Z(x1) … Z(xn)} ]} (3)
¬R(x_{1} … x_{n}) ⇒ Bew{Neg Sb[r ^{u1 … un} ⁄ _{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]}R(x_{1} … x_{n}) of the form: x_{1} = Φ(x_{2} … 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 Φ_{1} … Φ_{k} by the operations of substitution or recursive definition. Since, by the inductive assumption, everything is already proved for Φ_{1} … Φ_{k}, there exist corresponding relationstrings r_{1} … r_{k} such that (3) and (4) hold. The processes of definition whereby Φ is derived from Φ_{1} … Φ_{k} (substitution and recursive definition) can all be formally mapped to the system P. If this is done, we obtain from r_{1} … r_{k} a new relationstring r ^{[41]} , for which we can readily prove the validity of (3) and (4) by use of the inductive assumption. A relationstring r, assigned in this fashion to a recursive relation,^{[42]} will be called recursive.
We prove the proposition for all relations
We now come to the objective of our assertions:
Let c be any class of formulas. We denote by Flg(c) (set of consequences of c) the smallest set of formulas that contains all the formulas 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 classstring 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 classstring a.
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 classstrings 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 ^{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 relationstring 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 classstring with the free variable 19)
and
r = Sb(q ^{19}⁄_{Z(p)} ) (12)
(r is a recursive classstring with the free variable 17). ^{[43]}
Then
Sb(p ^{19}⁄_{Z(p)} ) = Sb ([17 Gen q] ^{19}⁄_{Z(p)} ) = 17 Gen Sb(q ^{19}⁄_{Z(p)} ) = 17 Gen r ^{[44]} (13)
(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)
Hence:
1. 17 Gen r is not cprovable.^{[45]} 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 cprovability of 17 Gen r there follows also that of Sb(r ^{17}⁄_{Z(n)} ). c would therefore be inconsistent (and, a fortiori, ωinconsistent).
2. Neg(17 Gen r) is not cprovable. Proof: As shown above, 17 Gen r is not cprovable, 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)} )], taken together with Bew_{c}[Neg(17 Gen r)] would conflict with the ω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 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 ^{17}⁄_{Z(n)} ), i.e. a formal proof of 17 Gen r would in fact lead to the actaul demonstration of an ωinconsistency.
We shall call a relation (class) of natural numbers R(x_{1} … x_{n}) decisionaldefinite, if there is an nplace relationstring r such that (3) and (4) hold (cf. Proposition V). In particular, therefore, by Proposition V, every recursive relation is decisionaldefinite. Similarly, a relationstring will be called decisionaldefinite, if it be assigned in this manner to a decisionaldefinite relation. It is, then sufficient, that for the existence of undecidable propositions, that the class c is assumed to be ωconsistent and decisionaldefinite. For the property of being decisionaldefinite 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 decisionaldefinite classstring (it is in fact sufficient that c is decisionaldefinite 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 counterexample nor to prove that it holds for all numbers. For, in proving that 17 Gen r is not cprovable, only the consistency of c is employed (cf. Propostion VI 1. “17 Gen r is not cprovable” ) and from ¬Bew_{c}(17 Gen r) it follows, according to (15), that for every number x, Sb(r ^{17}⁄_{Z(x)} ) is cprovable, and hence that Sb(r ^{17}⁄_{Z(x)} ) is not cprovable 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 cprovable. However c′ is not ωconsistent, since by ¬Bew_{c}(17 Gen r) and (15) we have:
(x) Bew_{c}Sb(r ^{17}⁄_{Z(x)} )
and hence we also have that:
(x) Bew_{c′}Sb(r ^{17}⁄_{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 typelift ). 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 ZermeloFraenkel 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]Unhomogeneous relations could also be defined in this manner, e.g. a relation between individuals and classes as a class of elements of the form: ((x_{2}),((x_{1}),x_{2})). As a simple consideration shows, all the provable propositions about relations in PM are also provable in this fashion.
[18a]Thus 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 metamathematics.
[21]As in PM I, *13, x_{1} = y_{1} is to be thought of as defined by x_{2}∀ (x_{2}(x_{1}) ⊃ x_{2}(y_{1})) (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 metamathematical concepts in the section [The Relations 146].)
[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 nonnegative whole numbers (or ntuples of such), respectively, and its values are nonnegative whole numbers.
[26]In what follows, small [italic] letters (with or without indices) are always variables for nonnegative 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_{1}, x_{2}) = Φ_{p}[Φ_{q}(x_{1}, x_{1}),Φ_{r}(x_{2})] (p, q, r < k). Not all the variables on the lefthand side must also occur on the right (and similarly in the recursion schema (2)).
[28]We include classes among relations (oneplace relations). Recursive relations R naturally have the property that for every specific ntuple of numbers it can be decided whether R(x_{1}…x_{n}) holds or not.
[29]For all considerations as to content (more especially also of a metamathematical kind) the Hilbertian symbolism is used,
cf. HilbertAckermann, Grundzüge der theoretischen Logik, Berlin 1928.
[30]We use [greek] letters χ, η, as abbreviations for given ntuple sets of variables, e.g. x_{1}, x_{2} … 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 ∀ [this does not appear in this translation] (otherwise the symbolism is Hilbertian).
[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)]^{2}. The prime numbers in n can therefore all be assumed smaller than Pr{[l(x)]^{2}}, their number ≤[l(x)]^{2} 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_{1} … 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 ntuple 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_{1} … 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 relationstring 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 cprovable” 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]}¬, (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
and the logical constants ∨,
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_{0} = Φ(x_{1} … 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_{1} … x_{n}) = ρ[χ_{1}(x_{1} … x_{n}), χ_{2}(x_{1} … x_{n}) … χ_{m}(x_{1} … x_{n})] ^{[51]}
(where p and all the x′s have degrees smaller than s) or
2. Φ(0,x_{2} … x_{n}) = Ψ(x_{2} … x_{n})
Φ(k + 1,x_{2} … x_{n}) = μ[k,Φ(k,x_{2} … x_{n}),x_{2} … x_{n}]
(where Ψ, μ are of lower degree than s).
In the first case we have:
x_{0} = Φ(x_{1} … x_{n}) ≡ (∃y_{1} … y_{m})[R(x_{0},y_{1} … y_{m}) & S_{1}(y_{1},x_{1} … x_{n}) & … & S_{m}(y_{m},x_{1} … x_{n})],
where R and S_{i} are respectively the arithmetical relations which, by the assumption of induction exist, are equivalent to x_{0} = ρ(y_{1} … y_{m}) and y = χ_{i}(x_{1} … x_{n}). In this case, therefore, x_{0} = Φ(x_{1} … x_{n}) is arithmetical.
In the second case we apply the following procedure: The relation x_{0} = Φ(x_{1} … x_{n}) can be expressed with the help of the concept “series of numbers” (f) ^{[52]} as follows.
x_{0} = Φ(x_{1} … x_{n}) ≡ (∃f){f_{0} = Ψ(x_{2} … x_{n}) & (k)[k < x_{1} ⇒ f_{k + 1} = μ(k,f_{k},x_{2} … x_{n})] & x_{0} = f_{x1}}
If S(y,x_{2} … x_{n}) and T(z,x_{1} … x_{n + 1}) are respectively the arithmetical relations, which exist by the assumption of induction, that are equivalent to
y = Ψ(x_{2} … x_{n}) and z = μ(x_{1} … x_{n + 1}),
the following then holds:
x_{0} = Φ(x_{1} … x_{n}) ≡ (∃f){S(f_{0},x_{2} … x_{n}) & (k)[k < x_{1} ⇒ T(f^{k + 1},k,f_{k},x_{2} … x_{n})] & x_{0} = 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 nonnegative 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_{0},f_{1} … f_{k1}. Let n be so determined tha.
n = f_{i}(mod(1 + (i + 1)l!)] for i = 0,1 … k1
which is possible, since every two of the numbers 1 + (i + 1)l! (i = 0,1 … k1) are relatively prime. For a prime number contained in two of these numbers would also be contained in the difference (i_{1}i_{2})l! and therefore, because i_{1}i_{2} < 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_{0},x_{1} … x_{n}) defined as follows.
P(x_{0} … x_{n}) ≡ (∃n,d){S([n]_{d + 1},x_{2} … x_{n}) & (k) [k < x_{1} ⇒T([n]_{1 + d(k + 2)},k,[n]_{1 + d(k + 1)},x_{2} … x_{n})] & x_{0} = [n]_{1 + d(x1 + 1)}}
which, according to (17) and Lemma 1, is equivalent to x_{0} = Φ(x_{1} … x_{n}) (we are concerned with the series f in (17) only in its course up to the x_{1} + 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]}Proposition VI there are undecidable arithmetical propositions.
referred to in
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^{53} 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 counterexample 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 onevalued 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 Φ_{1},Φ_{2} … Φ_{n}, such that Φ_{n} = Φ, Φ_{1}(x) = x + 1 and for every Φ_{k}(1 < k ≤ n) eithe.
1. (x_{2} … x_{m}) [Φ_{k}(0,x_{2} … x_{m}) = (Φ_{p}(x_{2} … x_{m})]
(x,x_{2} … x_{m}) {Φ_{k}[Φ_{1}(x),x_{2} … x_{m}] = (Φ_{q}[x,Φ_{k}(x,x_{2} … x_{m}),x_{2} … x_{m}]} (18)
p,q < k
or
2. (x_{1} … x_{m}) [Φ_{k}(x_{1} … x_{m}) = Φ_{r}(Φ_{i1}(χ_{1}) … Φ_{is}(χ_{s}))] ^{[60]} (19)
r < k, i_{v} < k (for v = 1, 2 … s)
or
3. (x_{1} … x_{m}) [Φ_{k}(x_{1} … x_{m}) = Φ_{1}(Φ_{1} … Φ_{1}(0))] (20)
In addition, we form the propositions:
(x) ¬[Φ_{1}(x) = 0] & (x y) [Φ_{1}(x) = Φ_{1}(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_{0} and form the conjunction C of all the formulas so obtained.
The formula (∃x_{0})C then has the required property, i.e
1. If (x) [Φ(x) = 0] is the case, then (∃x_{0})C is satisfiable, since when the functions Φ_{1}, Φ_{2} … Φ_{n} are substituted for Φ_{1}, Φ_{2} … Φ_{n} in (∃x_{0})C they obviously yield a correct proposition.
2. If (∃x_{0})C is satisfiable, then (x) [Φ(x) = 0] is the case.
Proof: Let Ψ_{1}, Ψ_{2} … Ψ_{n} be the functions presumed to exist, which yield a correct proposition when substituted for Φ_{1}, Φ_{2} … Φ_{n} in (∃x_{0})C. Let its domain of individuals be I. In view of the correctness of (∃x_{0})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 subclass of I, which contains a and is closed with respect to the operation Ψ_{1}(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 Ψ_{1} 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 Ψ_{1}′ and a, we can map the individuals of I′ in onetoone correspondence on the natural numbers, and this in such a manner that a transforms into 0 and the function Ψ_{1}′ into the successor function Φ_{1}. 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 numbervariable may naturally occur in to prefixes in place of x.
[51]It is not of course necessary that all x_{1} … 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_{0} being the first).
[53]These are the ωconsistent systems derived from P by addition of a recursively definable class of axioms.
[54]Cf. HilbertAckermann, 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 counterexample exists; but in virtue of Proposition IX the existence of this counterexample 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_{1}, x_{2} … x_{m}, e.g. x_{1} x_{3} x_{2}..
[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 cprovable; 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 cprovable,^{[65]} only the consistency of c was made use of, as appears from Propostion VI 1. “17 Gen r is not cprovable” ; 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)} )]
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]}(8.1), (9) and (10), by the relationstring 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.
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
In virtue of (24) w Imp (17 Gen r) is therefore provable in P^{[67]} (and a fortiori cprovable). Now if w were cprovable, 17 Gen r would also be cprovable 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 actaul derivation from c of a contradiction. The whole proof of Proposition XI can also be carried over word for word to the axiomsystem 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 cprovable, there will always be propositions which are undecidable (from c), namely w, so long as Neg(w) is not cprovable; in other words, one can replace the assumption of ωconsistency in Proposition VI by the following: The statement “c is inconsistent” is not cprovable. (Note that there are consistent c’s for which this statement is cprovable..
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.