# A Step by Step Guide to Gödel’s Incompleteness Proof:

7: Relations of Natural Numbers 24 to 46

7: Relations of Natural Numbers 24 to 46

Page last updated 01 Feb 2024

This guide is intended to assist in attaining a full understanding of Gödel’s proof. If there is any difficulty in following any part of the proof, please contact me and I will try to help. And if you have any suggestions as to how this guide might be improved, please contact me. This guide is intended to be read alongside the English translation of Gödel’s original proof which can be viewed online at English translation of Gödel’s original proof.

## Gödel’s Relations 24 - 46 of Natural Numbers

The number-theoretic relations are now becoming more complex as they correspond to more complex statements about formulas of the formal system **P**. It is not intended to cover every detail of these relations, but rather to concentrate on the main points and the thrust of the argument. It would be easy to get bogged down in such details and then fail to see the wood for the trees. As noted on the previous page, the names of the relations are mainly abbreviations of German words, see notes at the foot of this page for the words and the English translations.

### Relations 24-26: Assertions regarding variables of the formal system

These define number-theoretic relations that correspond to assertions as to whether a symbol is a free variable or a bound variable within a given symbol string.

24. **v Geb n,x**

This is an assertion regarding the natural numbers **v**, **n** and **x**, and it corresponds to the assertion:

at the **n ^{th}** symbol in the formula X, if V is a variable, and if it were to be at that position, it would be a bound variable

provided that **v = ψ[ V ]** and **x = φ[ X ]**.

Suppose we have a formula of the form **X = A (x _{1}∀ B) C**, where A, B and C are symbol strings of the formal system, and where

**x**is a variable, and

_{1}**∀**is the quantifier symbol for

*‘for all’*. Then the quantifier on the variable

**x**applies everywhere in the string B, but that quantifier does not apply to the string C. So the relation is asserting that the quantifier applies throughout the string B,

_{1}*of where the variable*

**regardless****x**might be in that string.

_{1}

**v Geb n,x** asserts that if **v = ψ[ V ]**, where V is a variable of the formal system, and **x = φ[ X ]**, where X is a formula, then if the **n ^{th}** prime number in

**x**is one of

**p**,

**q**,

**r**,

**s**,

**…**, then the corresponding variable V is bound (by the quantifier

**∀**) at the corresponding positions in the formula X.

**In Gödel’s paper…**

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

**v Fr n,x**is an assertion regarding the natural numbers

**v**,

**n**and

**x**, and

**v Fr n,x** corresponds to the assertion:

V is a variable, and it occurs as the **n ^{th}** symbol in the formula X, and it is free at that position

provided that **v = ψ[ V ]** and **x = φ[ X ]**

**In Gödel’s paper…**

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

**v Fr x**is an assertion regarding the natural numbers

**v**and

**x**, and

**v Fr x** corresponds to the assertion:

V is a variable, and it occurs as a free variable in the formula X

provided that **v = ψ[ V ]** and **x = φ[ X ]**.

**In Gödel’s paper…**

26.

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

**v** occurs in **x** as a *free variable*.

### Functions 27-31: Defining numbers that correspond to substitution in the formal system

The functions 27-30 lead up the function 31 which corresponds to the concept of the substitution of a free variable by a symbol or symbol string of the formal system.

27. **Su x( ^{n}/_{y}) ** 28.

**k St v,x**29.

**A(v,x)**30.

**Sb**31.

_{k}(x^{v}/_{y})**Sb(x**

^{v}/_{y})**Sb(x ^{v}/_{y})** is a function which is defined in terms of

**Su x(**,

^{n}/_{y})**k St v,x**,

**A(v,x)**and

**Sb**; these functions are not used anywhere else.

_{k}(x^{v}/_{y})

if **x = φ[ X ]**, **v = ψ[ V ]** and **y = φ[ Y ]**, then **Sb(x ^{v}/_{y})** corresponds to:

the operation of substituting the symbol V where it occurs as a free variable within the symbol string X, by the symbol string Y.

As an example, suppose that we have a formula X with only one free variable **x _{1}** at only one position in the formula. Then the Gödel number corresponding to that formula X will be like this:

**φ[ X ] = 2 ^{a} · 3^{b }· 5^{c} … · p^{17} ·**

**j**

^{u}· k^{w}· l^{y }· m^{z }· …where **p**, **j**, **k**, **l**, **m**, **q**, **r**, **s** and **t** are all prime numbers in order of size, and the values of the exponents **a**, **b**, **c**, **…**, **17**, **u**, **w**, **y**, **z**, **…** are given by the function **ψ** on the individual symbols/variables of the formula X, where **17 = ψ[ x _{1} ]**.

If the symbol string which will be substituted is say, ** ffff 0**, then

**φ[ ffff 0 ] = 2^{3} · 3^{3 }· 5^{3} · 7^{3} · 11^{1}**

**Sb(x ^{v}/_{y}) = 2^{a} · 3^{b}· 5^{c} … · p^{3} ·**

**j** · l

^{3}· k^{3}^{3 }· m

^{1}· q

^{u}· r

^{w}· s

^{y }· t

^{z}· …

This corresponds to the substitution of the **type 1 variable x _{1}** by the

**type 1 string**

*ffff*0

Gödel states that the function **Sb(x ^{v}/_{y})** corresponds to the concept

**Subst a(v|b)**, as defined in the definition of the system

**P**, where Gödel stated:

“**Sb(x ^{v}/_{y})** is the concept

**Subst a(v|b)**”

“By **Subst a(v|b)** (where **a** stands for a formula, **v** a variable and **b** a string of the same type as **v**) we understand the formula derived from **a**, when we replace **v** in it, wherever it is free, by **b**. Where **v** does not occur in **a** as a free variable, we must put **Subst a(v|b) = a**. Note that ‘**Subst**’ is a term belonging to metamathematics.”

Note that any Gödel number may be substituted for the variable **y**, so that the function **Sb** corresponds to the substitution of a free variable by *any symbol string* of the formal system. **Subst** defines that **b** must be of the same string type as the variable **v**. Hence where **Sb** is used in the following functions/relations, there must be the added stipulation to that effect.

Note that, depending on what version of the translation you are using, **Sb** may be represented in this format:

which is the format used in Gödel’s original paper.

**In Gödel’s paper…**

27.

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

Su x( ^{n}⁄_{y} ) derives from **x** on substituting **y** in place of the **n**^{th} term of **x** (it being assumed that 0 < n ≤ l(x)).

28.

**0 St v,x ≡ εn {n ≤ l(x) & v Fr n,x & ¬ (∃p)[n < p ≤ l(x) & v Fr p,x]}**

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

k St v,x is the **(k + 1)** ^{th} place in **x** (numbering from the end of *formula* **x**) where **v** is *free* in **x** (and **0**, if there is no such place.)

29.

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

**A(v,x)** is the number of places where **v** is *free* in **x**.

30.

**Sb _{0}(x ^{v}⁄_{y} ) ≡ x**

Sb_{k + 1}(x ^{v}⁄_{y} ) ≡ Su {Sb_{k}(x ^{v}⁄_{y} )} ( ^{k St v, x}⁄_{y} )

31.

Sb(x ^{v}⁄_{y} ) ≡ Sb_{A(v,x)}(x ^{v}⁄_{y} )^{[36]}

**Sb(x ^{v}⁄_{y} )** is the concept Subst a(

^{v}⁄

_{b}), defined above.

^{[37]}

### Relations/functions 32-42:

Assertions as to which numbers correspond to the axioms of the formal system

Assertions as to which numbers correspond to the axioms of the formal system

Functions 32 and 33 define some axioms of the formal system. Relations 34-42 inclusive are relations that use the previously defined relations/

32. **x Imp y, x Con y, x Aeq y, v Ex y**

These define the logical equivalent of *‘implies’*, *‘and’*, *‘equivalence’*, and *‘there exists’* (see also the axioms of the system P)

**In Gödel’s paper…**

32.

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

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

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

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

33. **n Th x**

Given that **x** is a Gödel number corresponding to a formula, then **n Th x** is a function that gives the Gödel number of the formula that is the **n ^{th}** type-lift of the formula

**x**(see Type-lift).

**In Gödel’s paper…**

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

34. **Z–Ax(x)**

These relations assert that **x** is the Gödel number of one of the Axioms **I.1-3**. Gödel asserts that there are numbers that correspond by Gödel numbering to each of these three axioms; he does this rather than give in detail how these numbers could be defined, but clearly these numbers could be calculated from the axioms by obtaining the equivalent formulation in the symbols of the formal system, and then applying the Gödel numbering function.

**In Gödel’s paper…**

To the axioms I, 1 to 3, there correspond three specific numbers, which we denote by **z _{1}**,

**z**,

_{2}**z**, and we define:

_{3}

34.

**Z-Ax(x) ≡ (x = z _{1} ∨ x = z_{2} ∨ x = z_{3})**

35. **A _{1}-Ax(x)**,

**A**,

_{2}-Ax(x)**A**,

_{3}-Ax(x)**A**36.

_{4}-Ax(x)**A-Ax(x)**(

Relation 35, **A _{1}-Ax(x)** defines that

**x**is a Gödel number that corresponds to an axiom defined by Axiom Schema

**II.1**. Similarly for

**A**,

_{2}-Ax(x)**A**and

_{3}-Ax(x)**A**for axioms defined by the Axiom Schemas

_{4}-Ax(x)**II.2-4**.

Relation 36, **A-Ax(x)** defines that **x** is a Gödel number that corresponds to one of the axioms given by the Axiom Schemas **II.1-4**

**In Gödel’s paper…**

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**are defined in accordance with the axioms II, 2 to 4.

_{4}-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)**

The relation **Q(z,y,v)** is only used in the definition of relation 38 (**L _{1}-Ax(x)**) and not elsewhere. It corresponds to the assertion:

the symbol string Z does not have any variable bound at any position which is not under the influence of a quantifier on the variable V.”

provided that **z = φ[ Z ]**, **y = φ[ Y ]**, **v = ψ[ V ]**.

**In Gödel’s paper…**

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

**L**40.

_{2}-Ax(x)**R-Ax(x)**41.

**M-Ax(x)**

The relations **L _{1}-Ax(x)**,

**L**and

_{2}-Ax(x)**R-Ax(x)**assert that

**X**is an axiom given by the Axiom Schemas

**III.1**,

**III.2**and

**IV.1**respectively, where

**x = φ[ X ]**.

The relation **M-Ax(x)** asserts that **x** is a number that corresponds by Gödel numbering to either the base axiom of the Axiom Schema **V.1**, or to a type-lift of the base axiom. As for relation 34, **Z–Ax(x)**, Gödel asserts that there is a number that corresponds to the base axiom of Axiom Schema **V.1**, rather than defining it in detail; this number (and the numbers for type-lifts) could be defined from the axiom by obtaining the equivalent formulation in the symbols of the formal system, and then applying the Gödel numbering function.

**In Gödel’s paper…**

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 specific number **z _{4}** and we define:

41.

**M-Ax(x) ≡ (∃n)[n ≤ x & x = n Th z _{4}]**

42. **Ax(x)**

This relation asserts that **x** is a number that corresponds by Gödel numbering to an axiom of the formal system **P**.

**In Gödel’s paper…**

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

### Relations 43-46:

Proofs in the formal system

The relations 43-46 deal with defining the number-theoretic relations that correspond to the concepts of the rules of inference of the system, the concept of a proof-schema, and the concept of a formula being provable in the system.

43. **Fl(x y z)**

This is an assertion regarding the natural numbers **x**, **y** and **z**, and it corresponds to the assertion:

the formula X is derived by the rules of inference from the formulas Y and Z

where **x = φ[ X ]**, **y = φ[ Y ]**, **z = φ[ Z ]** and X, Y and Z are symbol strings of the formal system **P**.

**In Gödel’s paper…**

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

This relation is defined in terms of the previous relation **Fl(x y z)**; it is an assertion that:

**x = 2 ^{φ[ X1 ]} · 3^{φ[ X2 ]} · 5^{φ[ X3 ]} · … p^{φ[ Xn ]}**

**x** corresponds to a series of formulas, in that the prime factors of **x** have exponents that are the Gödel numbers of formulas. By trhe reference to **Fl(x y z)**, each formula is either an axiom or a formula given by the rules of inference of the system applied to axioms or proven formulas.

**NB**: As for relation 22, this is *not* a direct correspondence by Gödel numbering and there is no symbol string of the formal system **P** where **x = φ[ X ]** - the exponents of the prime factors of **x** are Gödel numbers, rather than **x** itself being a Gödel number - in this case the number **x** does *not* correspond by Gödel numbering to a series of formulas nor to a proof schema of the formal system **P**, i.e**:**

**x** ≠ **φ** (series of formulas of the formal system **P**).

**x** ≠ **φ** (proof-schema of the formal system **P**).

For more on this, see Corresponding Relations in Part 4 of this guide.

**In Gödel’s paper…**

44.

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

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

45. **x B y**

This is an assertion regarding the natural numbers **x** and **y** and it corresponds to the assertion that:

the symbol string Y is a formula of the formal system **P** and there is a proof-schema for Y that corresponds to the number **x** by an appropriate relation.

where **y = φ[ Y ]**.

**y** corresponds to the exponent of the largest prime **p** in the number **x**, where:

**x = 2 ^{φ[ X1 ]} · 3^{φ[ X2 ]} · 5^{φ[ X3 ]} ·**

**… p**

^{φ[ Xn ]}Note that, as for relation 44 above, there is no symbol string of the formal system **P** where **x = φ[ X ]**.

**In Gödel’s paper…**

45.

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

**x** is a *proof* of the *formula* **y**.

46. **Bew(x)**

This is an assertion regarding the natural numbers **x** and **y** and it corresponds to the assertion:

X is a provable formula of the system **P**

i.e: there exists a proof-schema (a series of formulas) that is a proof of the formula X

where **x = φ[ X ]**, and there exists a number **w** such that **x** is the exponent of the largest prime **p** in the number **w**, where:

**w = 2 ^{φ[ Y1 ]} · 3^{φ[ Y2 ]} · 5^{φ[ Y3 ]} ·**

**… p**

^{φ[ Yn ]}

**In Gödel’s paper…**

46.

**Bew(x) = (∃y)y B x**

**x** is a *provable formula*. (**Bew(x)** is the only one of the concepts 1‑46 where it cannot be asserted that it is recursive.)

Below is a list of names used for various relations in the text, which are mostly abbreviations of German words; translations are provided below:

A | Anzahl | = | number |

Aeq | Aequivalenz | = | equivalence |

Ax | Axiom | = | axiom |

B | Beweis | = | proof |

Bew | Beweisbar | = | provable |

Bw | Beweisfigur | = | proof-schema |

Con | Conjunktion | = | conjunction |

Dis | Disjunktion | = | disjunction |

E | Einklammern | = | include in brackets |

Elf | Elementarformel | = | elementary formula |

Ex | Existenz | = | existence |

Fl | unmittelbare Folge | = | immediate consequence |

Flg | Folgerungsmenge | = | set of consequences |

Form | Formel | = | formula |

Fr | frei | = | free |

FR | Reihe von Formeln | = | series of formulae |

Geb | gebunden | = | bound |

Gen | Generalisation | = | generalization |

Gl | Glied | = | term |

Imp | Implikation | = | implication |

l | Lange | = | length |

Neg | Negation | = | negation |

Op | Operation | = | operation |

Pr | Primzahl | = | prime number |

Prim | Primzahl | = | prime number |

R | Zahlenreihe | = | number series |

Sb | Substitution | = | substitution |

St | Stelle | = | place |

Su | Substitution | = | substitution |

Th | Typenerhohung | = | type-lift |

Typ | Typ | = | type |

Var | Variable | = | variable |

Wid | Widerspruchsfreiheit | = | consistency |

Z | Zahlzeichen | = | number-symbol |

Rationale: Every logical argument must be defined in some language, and every language has limitations. Attempting to construct a logical argument while ignoring how the limitations of language might affect that argument is a bizarre approach. The correct acknowledgment of the interactions of logic and language explains almost all of the paradoxes, and resolves almost all of the contradictions, conundrums, and contentious issues in modern philosophy and mathematics.Site MissionPlease see the menu for numerous articles of interest. Please leave a comment or send an email if you are interested in the material on this site.

Interested in supporting this site?You can help by sharing the site with others. You can also donate at

_{}where there are full details.