# Godel's first Incompleteness Proof

This is a slightly formatted and annotated version of Goedel's first Incompleteness Theorem. For an introduction and outline, see the Wikipedia page: Proof sketch for Goedel's first incompleteness theorem.

It has been translated from the original German into English, and special symbols converted into their nearest HTML equivalents.

Goedel's original footnotes are indicated with numbers like this^{1}
and the text for them appears at the end of each of the four sections
of the paper. Three-digit numbers in brackets like [173] are the page
numbers in the original published article (pages 173-198 of volume 38
of the journal Monatshefte fuer Mathematik und Physik).

In addition, I have added occasional notes in a distinct font and color, and these notes are interspersed with the text.

[173]

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 may therefore be surmised that these axioms and rules of inference are
also sufficient to decide all mathematical questions which can in any way at
all be expressed formally in the systems concerned. It is shown below that this is
not the case, and that in both the systems mentioned there are in fact relatively
simple problems in the theory of ordinary whole numbers^{4}
which
[174]cannot be decided from the axioms. This situation is not due in some way to the
special nature of the systems set up, but holds for a very extensive class of formal
systems, including, in particular, all those arising from the addition of a finite
number of axioms to the two systems mentioned,^{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 formulae of a formal system — we
restrict ourselves here to the system PM — are, looked at from outside, finite
series of basic signs (variables, logical constants and brackets or separation
points), and it is easy to state precisely just which series of basic signs
are meaningful formulae and which are not.^{6} Proofs, from
the formal standpoint, are likewise nothing but finite series of formulae (with
certain specifiable characteristics). For metamathematical purposes it is naturally
immaterial what objects are taken as basic signs, and we propose to use natural
numbers^{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. 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", "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 as to content — states: v is a provable
formula. We now obtain an undecidable proposition of the system PM, i.e. a
proposition A, for which neither A nor not-A are provable, in the following
manner:

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

n ε K ≡ ~(Bew [R(n); n])^{11a} (1)

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

S = R(q)

holds for some determinate natural number q. We now show that the
proposition [R(q); q]^{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 ~(n ε K),
i.e. Bew [R(q); q] would hold good. [R(q); q]
would thus be provable at the same time as its negation, which again is impossible.

The analogy between this result and Richard's antinomy leaps to the eye; there is
also a close relationship with the "liar" antinomy,^{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 which asserts its own
unprovability.^{15} The method of proof just exhibited can
clearly
[176]be applied to every formal system having the following features: firstly,
interpreted as to content, it disposes of sufficient means of expression to define
the concepts occurring in the above argument (in particular the concept "provable
formula"); secondly, every provable formula in it is also correct as regards
content. The exact statement of the above proof, which now follows, will have among
others the task of substituting for the second of these assumptions a purely formal
and much weaker one.

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

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

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

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

^{4} I.e., more precisely, there are undecidable
propositions in which, besides the logical constants ~
(not), ∨ (or), (x) (for all) and = (identical with), there
are no other concepts beyond + (addition) and . (multiplication), both referred to
natural numbers, and where the prefixes (x) can also refer only to natural numbers.

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

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

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

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

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

^{10} It would be very simple (though rather laborious)
actually to write out this formula.

^{11} Perhaps according to the increasing sums of their
terms and, for equal sums, in alphabetical order.

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

^{12} Again there is not the slightest difficulty in
actually writing out the formula S.

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

^{14} Every epistemological antinomy can likewise be used
for a similar undecidability proof.

^{15} In spite of appearances, there is nothing circular
about such a proposition, since it begins by asserting the unprovability of a wholly
determinate formula (namely the q-th in the alphabetical arrangement with a definite
substitution), and only subsequently (and in some way by accident) does it emerge
that this formula is precisely that by which the proposition was itself expressed.

2

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

The basic signs of the system P are the following: I. Constants: "~" (not), "∨" (or), "∀" (for all), "0" (nought), "S" (the successor of), "(", ")" (brackets).

II. Variables of first type (for individuals, i.e. natural numbers including 0):
"x_{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 two-termed and many-termed functions (relations) are
superfluous as basic signs, since relations can be defined as classes of ordered
pairs and ordered pairs again as classes of classes, e.g. the ordered pair a,b
by ((a),(a,b)), where (x,y) means the class whose only elements are
x and y, and (x) the class whose only element is
x.^{18}

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

a, Sa, SSa, SSSa ... etc.

where a is either 0 or a variable of first type. In the former case we call such a
sign a number-sign. For n > 1 we understand by a sign of
n-th type the same as variable of n-th type.
Combinations of signs of the
form a(b), where b is a sign of n-th and a a sign of (n+1)-th
type, we call elementary formulae. The class of formulae we define as
the smallest class^{19} containing all elementary formulae
and, also, along with any a and b the following: ~(a),
(a)∨(b), x∀(a)
(where x is any given variable).^{18a} We term
(a)∨(b) the disjunction of a and
b, ~(a) the negation and
(a)∨(b) a generalization of a. A formula in
which there is no free variable is called a propositional formula (free
variable being defined in the usual way). A formula with just n free
individual variables (and otherwise no free variables) we call an n-place
relation-sign and for n = 1 also a class-sign.

By Subst a(v|b) (where a stands for a formula, v
a variable and b a sign of the same type as v) we understand the
formula derived from a, when we replace v in it, wherever it is free,
by b.^{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.

The following formulae (I-V) are called axioms (they are set out with the
help of the customarily defined abbreviations:
., ⊃,
≡, (∃x),
=,^{21}

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

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

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

≡ is the equivalence or biconditional operator. Gödel's definition of this is the standard one (which can be verified by looking at its definition in the metamathematics function 32 on page 184):

(a ≡ b) :: ((a ⊃ b) ∧ (b ⊃ a)).

When ∧ and ⊃ are expanded this becomes:

(a ≡ b) :: ~(~(~a ∨ b) ∨ ~(~b ∨ a))

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

= is the equal relation. As specified in Gödel's footnote, the definition of (a=b) is via a class variable:

(a = b) :: a_{2} ∀ (a_{2}(a) ⊃ a_{2}(b))

or (given the definition of ⊃ above)

(a = b) :: a_{2} ∀ (~(a_{2}(a)) ∨ a_{2}(b))

and subject to the usual conventions
about omission of brackets)^{22}:

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

I.

1. ~(Sx_{1} = 0)

Zero is the successor of no number. Expanded into the basic signs, the axiom is:

~(a_{2} ∀ (~(a_{2}(x_{1})) ∨ a_{2}(0)))

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

2. Sx_{1} = Sy_{1} ⊃ x_{1} = y_{1}

If x+1 = y+1 then x=y. Expanding the ⊃ operator we get:

~(Sx_{1} = Sy_{1}) ∨ (x_{1} = y_{1})

And expanding the = operators we get:

~(a_{2} ∀ (~(a_{2}(Sx_{1})) ∨ a_{2}(Sy_{1})))
∨ (a_{2} ∀ (~(a_{2}(x_{1})) ∨ a_{2}(y_{1})))

3. x_{2}(0).x_{1} ∀ (x_{2}(x_{1}) ⊃ x_{2}(fx_{1})) ⊃ x_{1} ∀ (x_{2}(x_{1}))

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

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

1. p ∨ p ⊃ p

2. p ⊃ p ∨ q

3. p ∨ q ⊃ q ∨ p

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

III. Every formula derived from the two schemata

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

2. v ∀ (b ⊃ a) ∨ b ⊃ v ∀ (a)

by making the following substitutions for a, v, b, c
(and carrying out in I the operation denoted by "Subst"): for a
any given formula, for v any variable, for b any formula in which v
does not appear free, for c a sign of the same type as v, provided that
c contains no variable which is bound in a at a place where v is
free.^{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 which does not contain u free. This axiom represents the axiom of reducibility (the axiom of comprehension of set theory).

V. Every formula derived from the following by type-lift (and this formula itself):

1. x_{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.

A formula c is called an immediate consequence of a and b,
if a is the formula (~(b)) ∨ (c),
and an immediate consequenee of a, if c is the formula v ∀ (a),
where v denotes any given variable. The class of provable formulae is
defined as the smallest class of formulae which contains the axioms and is closed
with respect to the relation "immediate consequence of".^{24}

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

[179] "0" ... 1

"S" ... 3

"~" ... 5

"∨" ... 7

"∀" ... 9

"(" ... 11

")" ... 13

Furthermore, variables of type n are given numbers of the form p^{n}
(where p is a prime number > 13). Hence, to every finite series of basic signs
(and so also to every formula) there corresponds, one-to-one, a finite series of
natural numbers. These finite series of natural numbers we now map (again in
one-to-one correspondence) on to natural numbers, by letting the number
2^{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 in one-to-one correspondence, not only to every
basic sign, but also to every finite series of such signs. We denote by
Φ(a) the number corresponding to the basic sign or
series of basic signs a.

Here is an example Gödel number for a string of symbols: The smallest theorem in the formal system is "0=0", which expands to:

a_{2} ∀ (~(a_{2}(0)) ∨ a_{2}(0))

This formula has 16 basic signs, and its Gödel number is
2^{172}3^{9}5^{11}7^{5}11^{11}13^{172}17^{11}19^{1}23^{13}29^{13}31^{7}37^{172}41^{11}43^{1}47^{13}53^{13}
≈ 1.97231222789×10^{1015}.

Suppose now one is given a class or relation
R(a_{1},a_{2},...a_{n}) of basic signs or series of
such. We assign to it that class (or relation) R'(x_{1},x_{2},...x_{n})
of natural numbers, which holds for x_{1}, x_{2}, ... x_{n}
when and only when 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 those classes and relations of
natural numbers which have been assigned in this fashion to such previously defined
metamathematical concepts as "variable", "formula",
"propositional formula", "axiom", "provable formula",
etc. The proposition that there are undecidable problems in the system P would
therefore read, for example, as follows: There exist propositional formulae
a such that neither a nor the negation of a are provable
formulae.
We now introduce a parenthetic consideration having no immediate connection with
the formal system P, and first put forward the following definition: A
number-theoretic function^{25}
φ(x_{1},x_{2},...x_{n}) is said
to be recursively defined by the number-theoretic functions
υ(x_{1},x_{2},...x_{n-1})
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)

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

A number-theoretic function φ is called
recursive, if there exists a finite series of number-theoretic functions
φ_{1}, φ_{2},
... φ_{n} which ends in φ
and has the property that every function φ_{k}
of the series is either recursively defined
[180]by two of the earlier ones, or is derived
from any of the earlier ones by substitution,^{27} or,
finally, is a constant or the successor function x+1. The length of the
shortest series of φ_{i}, which belongs to a
recursive function φ, is termed its degree.
A relation R(x_{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}.

The following propositions hold:

I. Every function (or relation) derived from recursive functions (or relations) by the substitution of recursive functions in place of variables is recursive; so also is every function derived from recursive functions by recursive definition according to schema (2).

II. If R and S are recursive relations, then so also are ~R, R ∨ S (and therefore also R & S).

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

(a & b) :: ~((~(a)) ∨ (~(b)))

III. If the functions φ(χ)
and υ(η) are
recursive, so also is the relation: φ(χ) = υ(η).^{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 != O

[181] γ(x,y) = 0, if x = y; γ(x,y) = 1, if x != y

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

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

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

Χ(0,η) = 0

Χ(n+1,η) = (n+1).a + Χ(n,η).α(a)^{31}

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,η) is already the case, the corresponding Χ(x,η) is constant and = 0). Therefore:

υ(χ,η) = C(φ(χ),η)

S(χ,η) ≡ R[υ(χ,η)),η)]

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

The functions x+y, x.y, x^{y}, and also the relations
x < y, x = y are readily found to be recursive;

x+y represents the sum of x and y; x.y represents their
product and x^{y} is x raised to the power of y. Each of these
can be defined as a recursive function expressed in terms of a
statement involving x, y and z which is true if and only if
x+y=z (and similarly for the multiplication and exponentiation
functions).

One possible definition for the addition function x+y=z is:

x+y=z ~ (y=0 & z=x) ∨ ∃a [ ∃b [ y=Sa & z=Sb & x+a=b ] ]

Roughly translated into English, this definition states:

"x+y=z is equivalent to the statement: (y=0 and z=x) or there are values for a and b such that (y=a+1, z=b+1, and x+a=b)."

For example, if x=3, y=0 and z=3 then we are saying "3+0=3 because y=0 and z=x".

As another example consider x=3, y=1 and z=4. We can't use the first part because y is not zero, so we use the second part: "3+1=4 because there are values of a and b satisfying the conditions y=a+1, z=b+1 and x+a=b". In particular, the first two conditions are true when a=0 and b=3, which then makes the third part x+a=b equivalent to the statement 3+0=3, the meaning of which is described in the previous example.

Similarly, when x=3, y=2 and z=5, the statement of x+y=z is expressed in terms of 3+1=4. In this manner we are using the principle of mathematical induction to recursively definine all truthful statements of the form 3+y=z.

Stated more abstractly, the definition of addition is saying:

"x+0=x for any x; and if x+a=b, then x+(a+1)=(b+1)."

If that were translated into symbols, it would be:

x ∀ [ x+0=x ]

x ∀ [ a ∀ [ b ∀ [ x+a=b ⊃ x+Sa=Sb ] ] ]

However this cannot be used as a basis of a recursive definition of the addition function because the second part places no limits on the variables a and b and it invokes the addition function twice.

A similar definition for multiplication is:

x.y=z ~ (y=0 & z=0) ∨ ∃a [ ∃b [ y=Sa & z=x+b & x.a=b ] ]

and its interpretation parallels that given for the addition definition. A similar definition for exponentiation is:

x^{y}=z ~ (y=0 & z=1) ∨
∃a [ ∃b [ y=Sa & z=x.b & x^{a}=b ] ]

and again its interpretation parallels that given for the addition definition.

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

[182]

1.
x/y ≡ (∃z)[z ≤ x & x = y.z]^{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} & not x/(n Pr x)^{y+1}]

n Gl x is the n-th term of the series of numbers assigned to the number x (for n > 0 and n not greater than the length of this series).

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

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

8.
x * y ≡ ε z [z ≤ [Pr{l(x)+l(y)}]^{x+y} & (n)[n ≤ l(x) → n Gl z = n Gl x] & (n)[0 < 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 number-series consisting only of the number x (for x > 0).

10. E(x) ≡ R(11) * x * R(13)

E(x) corresponds to the operation of "bracketing" [11 and 13 are assigned to the basic signs "(" and ")"].

11.
n Var x ≡ (∃z)[13 < 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.

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

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

Neg(x) is the negation of x.

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

[183]

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

x Dis y is the disjunction of x and y.

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

15. x Gen y ≡ R(x) * R(9) * E(y)

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

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

16. 0 N x ≡ x

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

n N x corresponds to the operation: "n-fold prefixing of the sign 'S' before x."

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

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

18.
Typ_{1}'(x) ≡ (∃m,n){m,n ≤ x & [m = 1 ∨ 1 Var m] & x = n N [R(m)]}^{34b}

x is a sign of first type.

19.
Typ_{n}(x) ≡ [n = 1 & Typ_{1}'(x)] ∨ [n > 1 & (∃v){v ≤ x & n Var v & x = R(v)}]

x is a sign of n-th type.

20.
Elf(x) ≡ (∃y,z,n)[y,z,n ≤ x & Typ_{n}(y) & Typ_{n+1}(z) & x = z * E(y)]

x is an elementary formula.

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

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

22. FR(x) ≡ (n){0 < n ≤ l(x) → Elf(n Gl x) ∨ (∃p,q)[0 < p,q < n & Op(n Gl x,p Gl x,q Gl x)]} & l(x) > 0

x is a series of formulae of which each is either an elementary formula or arises from those preceding by the operations of negation, disjunction and generalization.

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

24. v Geb n,x ≡ Var(v) & Form(x) & (∃a,b,c)[a,b,c ≤ x & x = a * (v Gen b) * c & Form(b) & l(a)+1 ≤ n ≤ l(a)+l(v Gen b)]

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

[184]

25. v Fr n,x ≡ Var(v) & Form(x) & v = n Gl x & n ≤ l(x) & not(v Geb n,x)

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

26. v Fr x ≡ (∃n)[n ≤ l(x) & v Fr n,x]

v occurs in x as a free variable.

27.
Su x(n|y) ≡ ε z {z ≤ [Pr(l(x)+l(y))]^{x+y} & [(∃u,v)u,v ≤ x & x = u * R(b Gl x) * v & z = u * y * v & n = l(u)+1]}

Su x(n|y) derives from x on substituting y in place of the n-th term of x (it being assumed that 0 < n ≤ l(x)).

28. 0 St v,x ≡ ε n {n ≤ l(x) & v Fr n,x & not (∃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) at which v is free in x (and 0, if there is no such place.)

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

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

30.
Sb_{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

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

x ⊃ y :: (~ (x)) ∨ (y).

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

Con is the boolean "and" operation, written with the symvol ∧. So this definition is:

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

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

Aeq is the biconditional "if and only if" operator, commonly represented by the symbol ↔. "Aeq" comes from the German "Aequivalenz" meaning "equivalence". So this definition would be written:

x ↔ y :: (x ⊃ y) ∧ (y ⊃ x)

which expands to

~((~((~(x)) ∨ (y))) ∨ (~((~(y)) ∨ (x))))

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

The Ex is commonly written with the ∃ symbol, so the definition is:

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

33.
n Th x ≡ ε n {y ≤ x^{(xn)} & (k) ≤ l(x) → (k Gl x ≤ 13 & k Gl y = k Gl x) ∨ (k Gl x > 13 & k Gl y = k Gl x.[1 Pr(k Gl x)]^{n})]}

n Th x is the n-th type-lift of x (in the case when x and n Th x are formulae).

To the axioms I, 1 to 3, there correspond three determinate numbers, which we denote by z_{1}, z_{2}, z_{3}, and we define:

34.
Z — Ax(x) ≡ (x = z_{1} ∨ x = z_{2} ∨ x = z_{3})

[185]

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 axiom-schema II, 1. Similarly A_{2}-Ax, A_{3}-Ax, A_{4}-Ax are defined in accordance with the axioms II, 2 to 4.

36.
A-Ax(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 x & w Geb n,y & v Fr n,y]

z contains no variable bound in y at a position where v is free.

38.
L_{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(v|z)]}

x is a formula derived from the axiom-schema 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 axiom-schema III, 2 by substitution.

40. R-Ax(x) ≡ (∃u,v,y,n)[u, v, y, n ≤ x & n Var v & (n+1) Var u & u Fr y & Form(y) & x = u ∃x {v Gen [[R(u)*E(R(v))] Aeq y]}]

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

To the axiom V, 1 there corresponds a determinate
number z_{4} and we define:

41.
M-Ax(x) ≡ (∃n)[n ≤ x & x = n Th z_{4}]

42.
Ax(x) ≡ Z-Ax(x) ∨ A-Ax(x) ∨ L_{1}-Ax(x) ∨ L_{2}-Ax(x) ∨ R-Ax(x) ∨ M-Ax(x)

x is an axiom.

43. Fl(x y z) ≡ y = z Imp x ∨ (∃v)[v ≤ x & Var(v) & x = v Gen y]

x is an immediate consequence of y and z.

[186] 44. Bw(x) ≡ (n){0 < n ≤ l(x) → Ax(n Gl x) ∨ (∃p,q)[0 < p,q < n & Fl(n Gl x, p Gl x, q Cl x)]} & l(x) > 0

x is a proof-schema (a finite series of formulae, of which each is either an axiom or an immediate consequence of two previous ones).

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

x is a proof of the formula y.

46. Bew(x) = (Ey)y B x

x is a provable formula. [Bew(x) is the only one of the concepts 1-46 of which it cannot be asserted that it is recursive.]

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

Proposition V: To every recursive relation R(x_{1} ... x_{n})
there corresponds an n-place relation-sign r (with the free
variables^{38} u_{1}, u_{2},
... u_{n}) such that for every n-tuple of numbers (x_{1} ... x_{n})
the following hold:

R(x_{1} ... x_{n}) → Bew{Sb[r (u_{1} ... u_{n})|(Z(x_{1}) ... Z(x_{n})]} (3)

~R(x_{1} ... x_{n}) → Bew{Neg Sb[r (u_{1} ... u_{n})|(Z(x_{1}) ... Z(x_{n})]} (4)

We content ourselves here with indicating the proof of this proposition in
outline, since it offers no difficulties of principle and is somewhat involved.^{39}
We prove the proposition for all relations 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 relation-signs r_{1} ... r_{k}
such that (3) and (4) hold. The processes of
definition whereby φ is derived from φ_{1} ... φ_{k}
(substitution and re-
[187]cursive definition) can all be formally mapped in the system
P. If this is done, we obtain from r_{1} ... r_{k}
a new relation-sign r^{41}, for which we can
readily prove the validity of (3) and (4) by
use of the inductive assumption. A relation-sign r, assigned in this
fashion to a recursive relation,^{42} will be called
recursive.

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

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

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

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

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

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

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

Bw_{c}(x) ≡ (n)[n ≤ l(x) → Ax(n Gl x) ∨ (n Gl x) ε c ∨

(Ep,q){0 < p,q < n & Fl(n Gl x, p Gl x, q Gl x)}] & l(x) > 0 (5)

(cf. the analogous concept 44)

x B_{c} y ≡ Bw_{c}(x) & [l(x)] Gl x = y (6)

Bew_{c}(x) ≡ (∃y)y B_{c} x (6.1)

(cf. the analogous concepts 45, 46)

The following clearly hold:

(x)[Bew_{c}(x) ≡ x ε Flg(c)] (7)

(x)[Bew(x) → Bew_{c}(x)] (8)

[188] We now define the relation:

Q(x,y) ≡ ~{x B_{c}[Sb(y 19|z(y))]}. (8.1)

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

~{x B_{c} [Sb(y 19|Z(y))]} → Bew_{c}[Sb(q 17|Z(x) 19|Z(y))]. (9)

x B_{c} [Sb(y 19|Z(y))] → Bew_{c}[Neg Sb(q 17|Z(x) 19|Z(y))]. (10)

We put

p = 17 Gen q (11)

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

r = Sb(q 19|Z(p)) (12)

(r is a recursive class-sign with the free variable 17).^{43}

Then

Sb(p 19|Z(p)) (13)
= Sb ([17 Gen q] 19|z(p))
= 17 Gen Sb(q 19|z(p))
= 17 Gen r^{44}

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

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

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

x B_{c} (17 Gen r) → Bew_{c}[Sb(r 17|Z(x))] (15)

x B_{c} (17 Gen r) → Bew_{c}[Neg Sb(r 17|Z(x))] (16)

[189]
Hence:
1. 17 Gen r is not c-provable.^{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 c-provability 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 c-provable. Proof: As shown
above, 17 Gen r is not c-provable, i.e. (according to
6.1) the following holds: (n) n B_{c}(17 Gen r).
Whence it follows, by (15), that (n) Bew_{c}[Sb(r 17|Z(n))],
which together with Bew_{c}[Neg(17 Gen r)] would conflict
with the ω-consistency of c.

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

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

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

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

We shall call a relation (class) of natural numbers R(x_{1} ... x_{n})
calculable [entscheidungsdefinit], if there is an n-place relation-sign
r such that (3) and (4) hold (cf.
Proposition V). In particular, therefore, by Proposition V,
every recursive relation is calculable. Similarly, a relation-sign will be
called calculable, if it be assigned in this manner to a calculable relation.
It is, then, sufficient for the existence of undecidable propositions, to assume of
the class c that it is ω-consistent and calculable.
For the property of being calculable carries over from c to x B_{c} y
(cf. (5), (6))
[190]and to Q(x,y)
(cf. 8.1), and only these are applied in the above proof. The
undecidable proposition has in this case the form v Gen r, where
r is a calculable class-sign (it is in fact enough that c should
be calculable in the system extended by adding c).

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

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

A special case of Proposition VI is that in which the class c consists of a finite number of formulae (with or without those derived therefrom by type-lift). Every finite class α 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 signs are replaced in any fashion by natural numbers).

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

Hence in every formal system that satisfies assumptions 1 and 2 and is
ω-consistent, undecidable propositions exist of the form
(x) F(x), where F is a recursively defined property of
natural numbers, and so too in every extension of such
[191]a system made by
adding a recursively definable ω-consistent class of
axioms. As can be easily confirmed, the systems which satisfy assumptions 1 and 2
include the Zermelo-Fraenkel and the v. Neumann axiom systems of set theory,^{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}

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

^{17} It is presupposed that for every variable type
denumerably many signs are available.

^{18} Unhomogeneous relations could also be defined in
this manner, e.g. a relation between individuals and classes as a class of elements
of the form: ((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} With regard to this definition (and others like it
occurring later), cf. J. Lukasiewicz and A. Tarski, 'Untersuchungen über den
Aussagenkalk

### uuml;l', Comptes Rendus des s

eacute;ances de la Soei

### eacute;t

eacute; des Sciences et des Lettres de Varsovie XXIII, 1930, Cl. 111.

^{20} Where v does not occur in a as a free
variable, we must put Subst a(v|b) = a. Note that
"Subst" is a sign 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 still

1. eliminate the abbreviations 2. add the suppressqd brackets.

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

^{23} c is therefore either a variable or 0 or a
sign of the form S ... S_{u}
where u is either 0 or a variable of type 1. With regard to the concept
"free (bound) at a place in a" cf. section I A5 of the work cited in
footnote 24.

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

^{25} I.e. its field of definition is the class of
non-negative whole numbers (or n-tuples of such), respectively, and its values
are non-negative whole numbers.

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

^{27} More precisely, by substitution of certain of the
foregoing functions in the empty places of the preceding, e.g.
φ_{k}(x_{1},x_{2}) = φ_{p}[φ_{q}(x_{1},x_{1}),φ_{r}(x_{2})] (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_{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.
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_{1}, x_{2} ... x_{n}.

^{31} We take it to be recognized that the functions
x+y (addition) and x.y (multiplication) are recursive.

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

^{33} The sign ≡ is used to
mean "equivalence by definition", and therefore does duty in definitions
either for = or for ~ [not the negation
symbol] (otherwise the symbolism is Hilbertian).

^{34} Wherever in the following definitions one of the
signs (x), (∃x), ε 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 limitation n ≤ (Pr[l(x)]^{2}^{x.[l(x)]2}
means roughly this: The length of the shortest series of formulae belonging to
x can at most be equal to the number of constituent formulae of x.
There are however at most l(x) constituent formulae of length 1, at most
l(x)-1 of length 2, etc. and in all, therefore, at most ^{1}/_{2}[l(x){l(x)+1}] ≤ [l(x)]^{2}.
The prime numbers in n can therefore all be assumed smaller that Pr{[l(x)]^{2}},
their number ≤[l(x)]^{2} and their
exponents (which are constituent formulae of x) ≤x.

^{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] z|y] 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 allotted. 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 there follows immediately its validity
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 naturally defined, not by the roundabout route of indicating its content, but by
its purely formal constitution.

^{42} Which thus, as regards content, expresses the
existence of this relation.

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

^{44} The operations Gen and Sb are
naturally always commutative, wherever they refer to different variables.

^{45} "x is c-provable" signifies:
x ε Flg(c), which, by (7),
states the same as Bew_{c}(x).

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

^{46} Thus the existence of consistent and not
ω-consistent c's can naturally be proved only on
the assumption that, in general, consistent c's do exist (i.e. that P
is consistent).

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

^{48} Cf. Problem III in D. Hilbert's lecture: 'Probleme
der Grundlegung der Mathematik', Math. Ann. 102.

^{48a} The true source of the incompleteness attaching
to all formal systems of mathematics, is to be found — as will be shown in Part
II of this essay — in the fact that the formation of ever higher types can be
continued into the transfinite (cf. D. Hilbert 'Über das Unendliche', Math.
Ann. 95, p. 184), whereas in every formal system at most denumerably many types
occur. It can be shown, that is, that the undecidable propositions here presented
always become decidable by the adjunction of suitable higher types (e.g. of type
ω for the system P). A similar result also holds
for 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_{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

[192]
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 inductive assumption exist, 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 by the inductive assumption exist — 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 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_{0},f_{1} ... f_{k-1}.
Let n be so determined that

n = f_{i}(mod(1+(i+1)l!)] for i = 0,1 ... k-1

[193]
which is possible, since every two of the numbers 1+(i+1)l! (i = 0,1 ... k-1)
are relatively prime. For a prime number contained in two of these numbers would also
be contained in the difference (i_{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}
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^{53}
there are undecidable problems of the restricted predicate calculus^{54}
(i.e. formulae of the restricted predicate calculus for which neither universal
validity nor the existence of a counter-example is provable).^{55}

[194] This is based on

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

We regard the restricted predicate calculus (r.p.c.) as consisting of those
formulae which are constructed out of the basic signs: ~,
∨, (x), =; x, y ...
(individual variables) and F(x), G(x,y), H(x,y,z) ...
(property and relation variables)^{56} where (x) and
= may relate only to individuals. To these signs 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 signs of the r.p.c., also contains
variables of the third kind, will be called a formula in the wider sense (i.w.s.).^{58}
The concepts of "satisfiable" and "universally valid" transfer
immediately to formulae i.w.s. and we have the proposition that for every formula
i.w.s. A we can give an ordinary formula of the r.p.c. B such that the
satisfiability of A is equivalent to that of B. We obtain B from
A, by replacing the variables of the third kind φ(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 φ, υ
... are strictly one-valued with respect to the first empty place.

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

Since F is recursive, there is a recursive function Φ(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)
either

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

[195] 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 formulae (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 formulae 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 formulae (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 Υ_{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 formulae (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 one-to-one 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
correct-
[196]ness 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 restated within the system P, the
equivalence between a proposition of the form (x) F(x) (F
recursive) and the satisfiability of the corresponding formula of the r.p.c. is
therefore provable in P, and hence the undecidability of the one follows from
that of the other, whereby Proposition IX is proved.^{62}

^{49} Here, and in what follows, zero is always included
among the natural numbers.

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

^{51} It is not of course necessary that all 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. Hilbert-Ackermann, Grundzüge der
theoretischen Logik. In the system P, formulae of the restricted predicate
calculus are to be understood as those derived from the formulae of the restricted
predicate calculus of PM on replacement of relations by classes of higher
type, as indicated on [176].

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

^{56} D. Hilbert and W. Ackermann, in the work already
cited, do not include the sign = in the restricted predicate calculus. But for
every formula in which the sign = occurs, there exists a formula without this
sign, which is satisfiable simultaneously with the original one (cf. the article
cited in footnote 55).

^{57} And of course the domain of the definition must
always be the whole domain of individuals.

^{58} Variables of the third kind may therefore occur at
all empty places instead of individual variables, e.g. 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 theorems 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 formulae, then the propositional formula which states that c
is consistent is not c-provable; in particular, the consistency of P is
unprovable in P,^{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 formulae, selected once and for all for purposes of the following
argument (in the simplest case it may be the null class). For proof of the fact that
17 Gen r is not c-provable,^{65}
only the consistency of c was made use of, as appears from 1, page 59; i.e.

Wid(c) → ~Bew_{c}(17 Gen r) (23)

i.e. by (6.1):

Wid(c) → (x) ~[x B_{c} (17 Gen r)]

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

Wid(c) → (x) ~[x B_{c} Sb(p 19|Z(p))]

[197] i.e. by (8.1):

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

We now establish the following: All the concepts defined (or assertions
proved) in Sections 2^{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-sign
q, and Q(x,p), therefore, by r [since by (12)
r = Sb(q 19|Z(p))] and the proposition (x) Q(x,p)
by 17 Gen r.

In virtue of (24) w Imp (17 Gen r) is
therefore provable in P^{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 effective derivation from
c of a contradiction. The whole proof of Proposition XI
can also be carried over word for word to the axiom-system of set theory M,
and to that of classical mathematics A,^{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 [198]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. There too, the mere outline proof we have given of Proposition XI will be presented in detail.

^{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 formulae.

^{65} r naturally depends on c (just as
p does).

^{66} From the definition of "recursive" on [179] up to the proof of Proposition VI inclusive.

^{67} That the correctness of 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.

(Received: 17. xi. 1930.)

This page was written in the "embarrassingly readable" markup language RHTF, and was last updated on 2017 Feb 02. s.11