Logic and Language

Logic and Language

Copyright © James R Meyer 2012 - 2018 https://www.jamesrmeyer.com

This page is keyboard accessible:

• Use**Tab**, **Shift + Tab **keys to traverse the main menu. To enter a sub-menu use the **Right Arrow** key. To leave a sub-menu use the **Left Arrow** or the **Escape** key.

• The**Enter** or the **Space** key opens the active menu item.

• To skip the menu and move to the main content, press**Tab** after the page loads to reveal a skip button.

• To get back to the top of the page anytime, press the**Home** key.

• For more information, click here: Accessibility Close this tip.

• Use

• The

• To skip the menu and move to the main content, press

• To get back to the top of the page anytime, press the

• For more information, click here: Accessibility Close this tip.

Note: Full functionality of this web page requires JavaScript to be enabled in your browser.

This is an English translation of Gödel’s Proof of Incompleteness (Footnote: Gödel, Kurt. "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I." Monatshefte für mathematik und physik 38, no. 1 (1931): 173-198.) and which is based on Meltzer’s English translation of the original German. The original German text can be viewed at:

Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I.

Notes:

In this translation, text in italics enclosed in square brackets are 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).

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

- 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 I-IV
- The Relations 1-46
- 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} 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 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:

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 definitions 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 be applied to every formal system having the following features: firstly, interpreted as to content, it disposes of sufficient means of expression to define the concepts occurring in the above argument
(in particular the concept "provable formula"); secondly, every provable formula in it is also correct as regards content. The exact statement of the above proof, which now follows, will have among others the task of substituting for the second
of these assumptions a purely formal and much weaker one.

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

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

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

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

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

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

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

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

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

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

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

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

The bar-sign indicates negation. [Replaced with **~**.]

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

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

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

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

**2**

*[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 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), "*f*" (the successor of), "**(**", "**)**"
(brackets).

II. Variables of first type (for individuals, i.e. natural numbers including 0): "**x _{1}**", "

Variables of second type (for classes of individuals): "**x _{2}**", "

Variables of third type (for classes of classes of individuals): "**x _{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}

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

**a**, ** fa**,

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

Combinations of signs of the form **a(b)**, where **b** is a sign of **n ^{th}** and

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

*[Axioms of the formal system P]*

The following formulae (I-V) are called **axioms** (they are set out with the help of the customarily defined abbreviations: **.**, **⊃** , **≡**, **(∃x)**, **=** ^{21} and subject to the usual conventions about omission of brackets):^{22}

I.

1. ~(*f*x_{1} = 0)

2. *f*x_{1} = *f*y_{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 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.

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.

*[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 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 Gödel numbering system]**

The basic signs of the system **P** are now ordered in one-to-one 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

**[Recursion]**

We now introduce a parenthetic consideration having no immediate connection with the formal system **P**, and first put forward the following definition: A number-theoretic function^{25} **Φ(x _{1},x_{2},…x_{n})** is said to be

Φ(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 number-theoretic function **Φ** is called recursive, if there exists a finite series of number-theoretic functions **Φ _{1}, Φ_{2}, …
Φ_{n}** which ends in

R(x_{1},x_{2},…x_{n}) ≡ [Φ(x_{1},x_{2},…x_{n}) = 0] ^{29}

**[Propositions I-IV]**

The following propositions hold:

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

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

**III.** If the functions **Φ(χ)** and **Ψ(η)** are recursive, so also is the relation: Φ(χ) =
Ψ(η). ^{30}

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

S(χ,η) ~ (∃x)[x ≤ Φ(χ) & R(x,η)]

T(χ,η) ~ (x)[x ≤ Φ(χ) ⇒ R(x,η)]

and likewise the function **Ψ**

Ψ(χ,η) = εx [x ≤ Φ(χ) & R(x,η)]

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

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

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

namely

**α(0) = 1; α(x) = 0 for x ≠ 0**

**β(0,x) = β(x,0) = 0; β(x,y) = 1, if x, y both ≠ O**

**γ(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 Relations 1-46]**

The functions **x+y**, **x.y**, **x ^{y}**, and also the relations x < y, x = y are readily found to be recursive; starting from these concepts, we now define a series of functions
(and relations)

1.

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

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: "**n**-fold prefixing of the sign ‘*f*’ 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]**

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

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**) 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(

32.

**x Imp y ≡ [Neg(x)] Dis y**

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

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

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

33.

**n Th x ≡ ε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}**,

34.

**Z–Ax(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 axiom-schema II, 1. Similarly **A _{2}-Ax**,

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

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

**[Proposition V]**

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}**,

R(x_{1} … x_{n}) ⇒ Bew{Sb[r ^{u1 … un} ⁄_{Z(x1) … Z(xn)} ]}
(3)

~R(x_{1} … x_{n}) ⇒ Bew{Sb[r ^{u1 … un} ⁄_{Z(x1) … Z(xn)} ]}
(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

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.

**[Proposition VI]**

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)

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

~{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)} ) = 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 *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:

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

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)) 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. Propostion VI 1. “*17 Gen r is not c-provable*”)
and from ~Bew_{c}(17 Gen r) it follows, according to (15), that for every number **x**, Sb(r ^{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 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}

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

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

Unhomogeneous relations could also be defined in this manner, e.g. a relation between individuals and classes as a class of elements of the form: **((x _{2}),((x_{1}),x_{2}))**. As a simple consideration shows, all
the provable propositions about relations in

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

With regard to this definition (and others like it occurring later), cf. J. Lukasiewicz and A. Tarski, ‘Untersuchungen über den Aussagenkalkül’, *Comptes Rendus
des séances de la Soeiété des Sciences et des Lettres de Varsovie* XXIII, 1930, Cl. 111.

Where **v** does not occur in **a** as a free variable, we must put Subst a( ^{v}⁄_{b} ) = a. Note that "**Subst**" is a sign belonging to metamathematics.

As in **PM** I, *13, x_{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.)

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 suppressed brackets.

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

**c** is therefore either a variable or 0 or a sign of the form *f* … ** f_{u}** where

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

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

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

More precisely, by substitution of certain of the foregoing functions in the empty places of the preceding, e.g. Φ_{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)).

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.

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

We use [greek] letters **χ**, **η**, as abbreviations for given **n**-tuple sets of variables, e.g. **x _{1}**,

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

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

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

Wherever in the following definitions one of the signs **(x)**, **(∃x)**, **ε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.

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.

m,n ≤ x stands for: m ≤ x & n ≤ x (and similarly for more than two variables).

The limitation **n ≤ (Pr[l(x)] ^{2x.[l(x)]2}** means roughly this: The length of the shortest series of formulae belonging to

Where **v** is not a *variable* or **x** not a *formula*, then Sb(x ^{v}⁄_{y} ) = x.

Instead of Sb[Sb[x ^{v}⁄_{y} ] ^{w}⁄_{z} ] we write: Sb(x ^{v}⁄_{y} ^{w}⁄_{z} ) (and similarly for more than two *variables*).

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.

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

From this there follows immediately its validity for every recursive relation, since any such relation is equivalent to 0 = Φ(x_{1} …
x_{n}), where **Φ** is recursive.

In the precise development of this proof, **r** is naturally defined, not by the roundabout route of indicating its content, but by its purely formal constitution.

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

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

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

"**x** is *c-provable*" signifies: x ∈ Flg(c), which, by (7), states the same as **Bew _{c}(x)**.

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

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

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

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

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

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})**

(where

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

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

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

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

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

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

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

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}

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

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

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 Φ

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 Φ

Owing to the correctness of (21) for **Ψ _{1}′** and

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}

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

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

It is not of course necessary that all x_{1} … x_{n} should actually occur in **χ _{i}** [cf. the example in footnote 27].

**f** signifies here a variable, whose domain of values consists of series of natural numbers. **f _{k}** denotes the

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

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

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

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

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

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

I.e. forming the conjunction.

χ_{i}(i = 1 … s) represents any complex of the variables x_{1}, x_{2} …
x_{m}, e.g. x_{1} x_{3} x_{2}.

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

**Proposition IX** naturally holds also for the axiom system of set theory and its extensions by recursively definable ω-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 Propostion VI 1. “*17 Gen r is not c-provable*”;
i.e.

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

i.e. by (6.1):

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

By (13), 17 Gen r = Sb(p ^{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} 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 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.

**C** is consistent (abbreviated as **Wid(c)**) is defined as follows: Wid(c) = (∃x) [Form(x) & ~Bew_{c}(x)].

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

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

From the definition of "recursive" on up to the proof of Proposition VI inclusive.

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

Cf. J. v. Neumann, ‘Zur Hilbertschen Beweistheorie’, *Math. Zeitschr.* 26, 1927.

Copyright © James R Meyer 2012 - 2018

https://www.jamesrmeyer.com