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

6: Relations of Natural Numbers 1 to 23

6: Relations of Natural Numbers 1 to 23

## Page Contents

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 1- 45 of Natural Numbers

Note again that in Gödel’s paper the epsilon symbol **ε** is used in several definitions; the meaning of the term **ε** (see also Epsilon notation ε) is given by:

**εx R(x, y)** is a function with the free variable **y**, and whose value is *the smallest number* **x** *for which the relation* **R(x, y)** *holds*, and if there is no such smallest number, then the value of **εx R(x, y)** is **0**.

In the section entitled *“Relations 1‑46”* Gödel defines various relations/

Some of these functions (nos. 3, 4, 5, 16, 30) are recursively defined in terms of the value of the function itself. For example, the function 4 is the factorial function mentioned in the previous page.

For most of the relations/**P** are represented by colored capital letters, e.g. X, Y. (Footnote:
Note that these variables are in a language that is a meta-language to the formal system.)

It is crucial to remember that all these relations/

It should be noted that in some cases, a corresponding number is obtained not by the Gödel numbering function **φ** but by the **ψ** function (as referred to previously, see The Psi function). This does not present any problems, since given a number obtained via the **ψ** function for a symbol, one can always obtain the Gödel number by applying the Gödel numbering function **φ** to that single symbol. For example **ψ( f ) = 3**, and

**φ[**.

*f*] = 2^{3}

**NB**: when the term ‘symbol’ is used below, unless otherwise indicated, that can mean either a single basic symbol of the system **P** or a variable of the system **P**. Also note that some of the ‘formulas’ used in the examples are not actually proper formulas of the system **P**; this is only so that the examples are not overly long.

### Relations/functions 1-5:

Basic Arithmetical Concepts.

Basic Arithmetical Concepts.

These are basic arithmetical concepts, principally concerning properties of prime numbers. Since the Gödel numbering method is based on the fact that every natural number has a unique factorization into its constituent prime factors, these relations/

1. **x/y**

This is a relation that asserts that **y** is divisible by **x** with no remainder .

e.g. the relation **72/6** applies, but **73/6** does not apply.

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

1.

x/y ≡ (∃z)[z ≤ x & x = y · z]^{[33]}

**x** is divisible by **y**.^{[34]}

2. **Prim(x)**

This is a relation that asserts that **x** is a prime number. i.e: **x** is one of **2**, **3**, **5**, **7**, **11**, **13**, **17**, **19**, **23**, **…**

e.g. the relation **Prim(7)** applies, but **Prim(8)** does not apply.

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

2.

**Prim(x) ≡ ¬(∃z)[z ≤ x & z ≠ 1 & z ≠ x & x/z] & x > 1**

**x** is a prime number.

3. **n Pr x**

This is a function whose value is the **n ^{th}** largest prime number that is a factor of

**x**.

e.g. **4 Pr [ 2 ^{3} · 3 · 5^{3} · 7^{4} · 11 · 13^{3} ] = 7**

(**7** is the **4 ^{th}** largest prime factor of

**2**)

^{3}· 3 · 5^{3}· 7^{4}· 11 · 13^{3}

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

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

This is the factorial function as mentioned previously in this guide. Its value is given by multiplying together **n** and all the natural numbers that are smaller than **n** (except zero).

e.g.** 4! = 4 · 3 · 2 · 1**

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

4.

**0! ≡ 1**

**(n + 1)! ≡ (n + 1).n!**

5. **Pr(n)**

This is a function whose value is the **n ^{th}** largest prime number.

e.g. **Pr(5) = 11** (the **5 ^{th}** largest prime is

**11**; the four smaller primes are

**2**,

**3**,

**5**and

**7**)

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

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

### Relations/functions 6‑23:

Relations/functions that correspond to the construction of symbol strings

Relations/

We now move from basic arithmetical definitions to the definition of functions that correspond to operations on symbols and symbol strings of the formal system - and to the definition of relations that correspond to assertions regarding symbol strings of the formal system.

The formulas of the formal system are combinations of the symbols of the system that satisfy certain conditions. One of the goals of these relations and functions is to lead to the definition of relation 23, which corresponds to the assertion that a given symbol string is a formula of the formal system.

It will be noted that the functions/

#### Functions 6, 7, 9: Basic string operations

These are basic functions that correspond to:

6. **n Gl x**: the operation of obtaining the symbol at a particular position in a symbol string

7. **l(x)**: the operation of counting the number of symbols in a symbol string

9. **R(x)**: the operation of obtaining the Gödel number of a single symbol

6. **n Gl x**

This is a function which is defined in terms of the function **n Pr x** above, and gives the value of the smallest factor of the exponent of the **n ^{th}** largest prime in the number

**x**.

e.g. **5 Gl [ 2 ^{3} · 3^{3} · 5^{1} · 7^{11} · 11^{19} · 13^{3} ]**

**= 19**(the

**5**largest prime in

^{th}**x**is

**11**, and its exponent is

**19**)

If **x** is the Gödel number of the formula X, i.e: **x = φ[ X ]**, then **n Gl x** corresponds to:

the symbol at the **n ^{th}** position in the symbol string X

e.g. if X** = ff 0(y_{1})**, then

**x = φ[ X ] = 2**

^{3}· 3^{3}· 5^{1}· 7^{11}·**11**

^{19}· 13^{3}then **5 Gl [ 2 ^{3} · 3^{3} · 5^{1} · 7^{11} · 11^{19} ·**

**13**to correspond to:

^{3}] = 19the operation of obtaining the **5 ^{th}** symbol of the symbol string

**, which is**

*ff*0(y_{1})**y**

_{1}where **19 = ψ[ y _{1} ]**.

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

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

This is a function whose value is the number of unique prime factors in **x**.

e.g. **l(2 ^{3} · 3^{3} · 5^{3} · 7^{1})** =

**4**(there are only four unique prime factors:

**2**,

**3**,

**5**,

**7**).

If **x** is the Gödel number of the formula X, i.e: **x = φ[ X ]**, then **l(x)** corresponds to:

the operation of counting the number of individual symbols/variables in the formula X

e.g. if **X = fff 0**, then

**x = φ[ X ] = 2**, then

^{3}· 3^{3}· 5^{1}· 7^{1}**l(2 ^{3} · 3^{3} · 5^{1} · 7^{1}) = 4** corresponds to:

the operation of counting the number of symbols in ** fff 0**, which is

**4**.

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

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

9. **R(x)**

This is a function which raises **2** to the power of **x**, e.g. **R(19) = 2 ^{19}**

So **R(x) = φ[ X ]**

where **x = ψ[ X ]** (as given by **ψ** - the Psi function - the function that assigns a unique number to a symbol X of the formal system), and where X is a single symbol or a variable of the formal system **P** .

e.g. if X** = (**, then **x = ψ[ ( ] = 11**, and

**R(x) = 2 ^{11 }**corresponds to:

the operation of obtaining the Gödel number of the symbol **(**, which is **φ[ ( ] = R(ψ[ ( ]) = 2 ^{11}**

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

9.

**R(x) ≡ 2 ^{x}**

**R(x)** corresponds to the number-series consisting only of the number **x** (for x > 0).

#### Function 8: Defining numbers that correspond to a concatenation of two strings

**x * y** corresponds to the operation of concatenating (joining together) two symbol strings.

8. **x * y**

This function can be thought of as ‘shifting’ up the prime factors of the second number **y**. It is probably easiest to understand this function by an example.

**[ 2 ^{3} ] * [ 2^{3} · 3^{3} · 5^{3} · 7^{1} ] =**

**2**

^{3}· 3^{3}· 5^{3}· 7^{3}· 11^{1}

And **x * y = φ[ XY ]**, where **x = φ[ X ]** and **y = φ[ Y ]**

i.e: **φ[ X ] * φ[ Y ] = φ[ XY ]**

that is, if **x= φ[ X ]** and **x= φ[ Y ]**, then the function** x * y** corresponds to:

the operation of concatenating X and Y

where X and Y are symbol strings of the formal system **P** .

e.g. if **X = f** and

**Y =**, then

*fff*0**x = φ[ X ] = 2**, and

^{3}**y = φ[ Y ] = 2**

^{3}· 3^{3}· 5^{3}· 7^{1}then **2 ^{3 } * 2^{3} · 3^{3} · 5^{3} · 7^{1} =**

**2**corresponds to:

^{3}· 3^{3}· 5^{3}· 7^{3}· 11^{1}the operation of concatenating the symbol strings * f* and

**to give**

*fff*0**.**

*ffff*0

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

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.

#### Functions 16, 17: Defining numbers that correspond to simple strings

These are functions that correspond to:

16. **n N x**: the operation of **n** repetitions of prefixing a symbol string by the symbol **f**

17. **Z(n)**: the operation of **n** repetitions of prefixing the symbol **0** by the symbol **f**

16. **n N x**

**0 N x = φ[ X ]**

**1 N x = φ[ f X ]**

**2 N x = φ[ ff X ]**

**…**

**…**

**n N x = φ[ fff…ff X ]**, where there are

**n**occurrences of

**f**that is, if **x = φ[ X ]**, then the value of **n N x** corresponds to:

the operation of prefixing **n** repeated occurrences of the symbol ** f** in front of the symbol string X

e.g. if X is ** f 0**, and

**φ[**

*f*0 ] = 2^{3}· 3^{1}then **3 N (2 ^{3} · 3^{1}) = 2^{3} · 3^{3} · 5^{3} · 7^{3} · 11^{1}** corresponds to:

the operation of prefixing ** f 0** by three instances of

**, which gives**

*f***.**

*ffff*0

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

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 symbol *‘f ’* before **x**.”

17. **Z(n)**

For this function,

**Z(n) = n N R(1)**, and **R(1) = 2 ^{1}**, so

**Z(n) = n N 2 ^{1}= φ[ fff…ff 0 ]**

where there are **n** occurrences of * f*, since by the Gödel numbering function,

**2**corresponds to the formal symbol for zero, which is

^{1}**0**. So the value of

**Z(n)**corresponds to:

the operation of prefixing **n** repeated occurrences of the symbol ** f** in front of the symbol

**0**

e.g. **Z(5) = φ[ fffff 0 ] = 2^{3} · 3^{3} · 5^{3} · 7^{3} ·**

**11**corresponds to:

^{3}· 13^{1}the operation of obtaining the Gödel number of *fffff* 0

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

17.

**Z(n) ≡ n N [R(1)]**

**Z(n)** is the *number-string* for the number **n**.

**Note:** Gödel is being rather disingenuous here in simply asserting that “**Z(n)** is the *number-string* for the number **n**”, without giving any further details. By that assertion he is asserting that **Z(n) = φ[ n ]**, i.e: that **Z(n)** is the same as the Gödel numbering function for the number **n**. But the domain of the variable of the Gödel numbering function **φ** is *all* symbol strings of the formal system, whereas the domain of the function **Z** is the domain of natural numbers. To make the assertion means that the domain of the common variable **n** would have to be restricted to symbol strings of the format **0, f 0, ff 0, fff 0, …**, and it would not be allowable, for example to have an equality between

**5**and

**, since if such equality were permissible, we would have**

*fffff*0**φ[ 5 ]**which is not a valid expression. Furthermore, the symbols for zero and the successor symbol for the formal system could be any symbols, for example,

**3**and

**7**, which would rule out using the symbols

**3**and

**7**for three and seven, as is conventional for number-theoretic relations. Gödel’s stipulation requires that his number-theoretic relations must necessarily use precisely the same format for natural numbers as the formal system in question - which begs the question as to why the two systems should be interdependent in this manner. Gödel claims that any formal system (if it includes sufficient arithmetic) can be used in place of his system

**P**- which means that the formal system, and the symbols it uses,

*be independent of the meta-language. We will discuss this matter in more detail later when considering Gödel’s Proposition V.*

**must**

#### Functions 10, 13, 14, 15: Defining numbers that correspond to complex strings

These functions correspond to operations that build up more complex symbol strings from simpler ones. They correspond to:

10. **E(x)**: the operation of putting brackets around a symbol string

13. **Neg(x)**: the operation of creating the negation of a symbol string

14. **x Dis y**: the operation of joining two symbol strings by the ‘or’ symbol **∨**

15. **x Gen y**: the operation of prefixing a symbol string by a variable and the ‘for all’ symbol **∀**

10. **E(x)**

This function can be thought of as multiplying the number **x** by an ‘initial’ **2 ^{11}**, and ‘shifting’ each of the exponents of the prime factors of the number

**x**up to the next largest prime, and then multiplying the result by a ‘final’ next largest prime with an exponent of

**13**. The exponent of the ‘initial’

**2**is

**11**, since

**11**is the matching number for the opening bracket (

**11 = ψ[ ( ]**), and the exponent of the ‘final’ prime is

**13**, since

**13**is the matching number for the closing bracket (

**13 = ψ[ ) ]**). It is probably easiest to understand this function by an example:

**E(2 ^{3} · 3^{3} · 5^{3} · 7^{3} · 11^{1})**

**= 2**

^{11}· 3^{3}· 5^{3}· 7^{3}· 11^{3}· 13^{1}· 17^{13}In this example **17** is the additional ‘final’ next largest prime (with the exponent of **13**).

Note that **E(x) = φ[ ( X ) ]**

where **x = φ[ X ]**, and where X is a symbol string of the formal system **P**.

See Function 8, which gives that

**φ[ ( X ) ] = φ[ ( ] * φ[ X ] * φ[ ) ]**

that is, if **x = φ[ X ]** then the value of **E(x)** corresponds to:

the operation of putting brackets on either side of the symbol string X

e.g. if **X = ffff 0**, and

**φ[**, then

*ffff*0 ] = 2^{3}· 3^{3}· 5^{3}· 7^{3}· 11^{1}**E(x) = φ[ ( X ) ] = φ[ ( ffff 0) ] =**

**2**corresponds to:

^{11}· 3^{3}· 5^{3}· 7^{3}· 11^{3}· 13 · 17^{13}the operation of enclosing the symbol string ** ffff 0** by brackets to give

**(**.

*ffff*0)

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

10.

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

**E(x)** corresponds to the operation of “bracketing” [**11** and **13** are assigned to the basic symbols “**(**” and “**)**”].

13. **Neg(x)**

This function can be thought of as multiplying the number **x** by an ‘initial’ **2 ^{5} · 3^{11}**, and ‘shifting’ each of the exponents of the prime factors of the number

**x**up to the next largest prime, and then multiplying the result by a ‘final’ next largest prime with an exponent of

**13**. The exponent of the ‘initial’

**2**is

**5**, since

**5**is the matching number for the negation symbol (

**5 = ψ[ ¬ ]**), and the exponent of the ‘initial’

**3**is

**11**, since

**11**is the matching number for the opening bracket (

**11 = ψ[ ( ]**); the exponent of the ‘final’ prime is

**13**, since

**13**is the matching number for the closing bracket (

**13 = ψ[ ) ]**). It is probably easiest to understand this function by an example:

**Neg(2 ^{3} · 3^{3} · 5^{3} · 7^{3} · 11^{1}) =**

**2**

^{5}· 3^{11}· 5^{3}· 7^{3}· 11^{3}· 13^{3}·**17**

^{1 }· 19^{13}In this example **19** is the additional ‘final’ next largest prime (with the exponent of **13**).

And **Neg(x) = φ[ ¬(X) ]**

where X is a string of symbols of the formal system **P**, and **¬**, **(** and **)** are symbols of the formal system **P**.

Function 8 above gives that

**φ[ ¬ ] * φ[ ( ] * φ[ X ] * φ[ ) ] =** **φ[ ¬(X) ]**

that is, if **x = φ[ X ]** then the value of **Neg(x)** corresponds to:

the operation of putting the symbol **¬** in front of the symbol string X

i.e: creating the negation of the formula X

e.g. if **X = ffff 0**, and

**φ[**

*ffff*0 ] = 2^{3}· 3^{3}· 5^{3}· 7^{3}· 11^{1}then **Neg(x) = φ[ ¬( ffff 0) ] =**

**2**

^{5}· 3^{11 }· 5^{3}· 7^{3}· 11^{3}· 13^{3}·**17**corresponds to:

^{1 }· 19^{13}the operation of enclosing the symbol string ** ffff 0** by brackets and prefixing that by the negation symbol to give

**¬(**.

*ffff*0)

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

13.

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

**Neg(x)** is the *negation* of **x**.

14. **x Dis y**

**x Dis y = φ[ (X) ∨ (Y) ]**

where X and Y are symbol strings of the formal system **P**, and **∨** is a symbol of the formal system **P**.

Function 8 above gives that

**φ[ ( ] * φ[ X ] * φ[ ) ] * φ[ ∨ ] *** **φ[ ( ] * φ[ Y ] * φ[ ) ]** **= φ[ (X) ∨ (Y) ]**

that is, if **x = φ[ X ]** and **y = φ[ Y ]**, then the value of **x Dis y** corresponds to:

the operation of concatenating the symbol string (X), the symbol **∨**, and the symbol string (Y).

i.e: creating a formula by joining two formulas by the ‘or’ symbol **∨**

e.g. if **X = f 0**, and

**φ[**, and

*f*0 ] = 2^{3}· 3^{1}**Y =**, and

*ff*0**φ[**, then

*ff*0 ] = 2^{3}· 3^{3}· 5^{1}**x Dis y = φ[ ( f 0) ∨ (ff 0) ] =**

**2**

^{11}· 3^{3 }· 5^{1}· 7^{13}· 11^{7}· 13^{11}·**17**corresponds to:

^{3 }· 19^{3}· 23^{1}· 29^{13}the operation of enclosing the symbol strings ** f 0** and

**by brackets and interposing the symbol**

*ff*0**∨**between them to give

**(**.

*f*0) ∨ (*ff*0)

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

14.

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

**x Dis y** is the *disjunction* of **x** and **y**.

15. **x Gen y**

For this function,

**x Gen y = φ[ X ∀ (Y) ]**

where X and Y are symbol strings of the formal system **P**, and **∀** is a symbol of the formal system **P**.

Function 8 above gives that

**φ[ X ] * φ[ ∀ ] * φ[ ( ] * φ[ Y ] *** **φ[ ) ] = φ[ X ∀ (Y) ]**

that is, if **x = φ[ X ]** and **y = φ[ Y ]**, then the value of **x Gen y** corresponds to:

the operation of concatenating the symbol string X, the symbol **∀**, and the symbol string (Y).

i.e: creating the generalization of a formula by prefixing it with a variable and the *‘For all’* symbol (though note that in this function X is not restricted to being a variable - it can be any symbol string of the system **P**; the definition of what constitutes a variable is given by Relation 12) .

e.g. if X is a **type 1 variable**, and **x = φ[ z _{1} ]**, and

**Y**is some formula, where

**y = φ[ Y ]**, then

**x Gen y = 2 ^{23} · 3^{9} · … =**

**2**corresponds to:

^{ψ[ z1 ]}· 3^{ψ[ ∀ ]}· …the operation of bracketing the formula Y and prefixing it by **z _{1}∀**

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

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

#### Relations 11, 12: Assertions regarding variables of the formal system

Relations 11. **n Var x** and 12. **Var(x)** correspond to the assertion that a particular symbol is a variable (reminder: we refer to a variable of the formal system as a ‘single’ symbol, although it is actually composed of two or more symbols).

11. **n Var x**

This is a relation, which asserts that **x = p ^{n}**, where

**p**is a prime number greater than

**13**.

e.g. the relation **1 Var 17** applies; **2 Var 23 ^{2}** applies;

**2 Var 19**does not apply (since the exponent of

**19**is not

**2**).

The relation **n Var x** is an assertion regarding natural numbers **n** and **x**, and corresponds to the assertion:

the symbol string X is a **type n** variable of the formal system **P**

where **x = ψ[ X ]**.

Note that **n Var x** defines a correspondence to a variable of the formal system by the use of the **ψ** function rather than using the **φ** function directly. The **n** defines the type of the corresponding variable X.

e.g. if X is the variable **x _{3}** of the formal system, and

**ψ[ x**

_{3}] = 17then **3 Var 17 ^{3}** corresponds to:

the assertion that the symbol string **x _{3}** is a

**type 3 variable**.

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

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 Var x**), i.e: it asserts that

**x = p**, where

^{n}**p**is a prime number greater than

**13**, and

**n > 0**.

The relation **Var(x)** is an assertion regarding a natural number **x**, and corresponds to the assertion:

the symbol string X is a variable of the formal system **P**

where **x = ψ[ X ]**.

Similar to the definition for **n Var x**. **Var(x)** also defines a correspondence to a variable of the formal system by the use of the **ψ** function.

e.g. if X is the variable **y _{2}** of the formal system, and

**ψ[ y**, then

_{2}] = 19^{2}**Var 19**corresponds to:

^{2}the assertion that the symbol string **y _{2}** is a

**variable**of the formal system

**P**.

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

12.

**Var(x) ≡ (∃n)[n ≤ x & n Var x]**

**x** is a *variable*.

#### Relations 18, 19: Assertions regarding Type n strings of the formal system

Relations 18. **Typ _{1}′(x)** and 19.

**Typ**correspond to the assertion that a particular combination of symbols is a string of the formal system.

_{n}(x)

18. **Typ _{1}′(x) ** 19.

**Typ**

_{n}(x)**Typ _{1}′(x)** is not used anywhere else, its only role is in the definition of the relation

**Typ**.

_{n}(x)**Typ _{n}(x)** asserts that either

**x = 2**, or

^{3}· 3^{3}· … · p^{q}**x = 2**, where

^{pn}**p**,

**q**and

**n**must satisfy certain conditions.

**Typ _{1}′(x)** asserts that either:

**x = 2 ^{3} · 3^{3} · … · p^{1}**, where

**p**is some prime number; this corresponds to:

X is a symbol string of the form **0, f 0, ff 0, fff 0, …**,

where **x = φ[ X ]**.

or

**x = 2 ^{3} · 3^{3} · … · p^{q}**, where

**p**is some prime number and

**q**is some prime number greater than 13; this corresponds to:

X is a symbol string of the form **x _{1}**,

**,**

*f*x_{1}**,**

*ff*x_{1}**,**

*fff*x_{1}**…**, or

**y**,

_{1}**,**

*f*y_{1}**,**

*ff*y_{1}**,**

*fff*y_{1}**…**, etc,

where **x = φ[ X ]**.

For **Typ _{n}(x)**, for the case when

**n = 1**, the case is simply

**Typ _{1}(x) = Typ_{1}′(x)**

when **n > 1**, **Typ _{n}(x)** asserts that:

**x = 2 ^{pn}**, or

**x = (2**, where

^{p})^{n}**p**is some prime number greater than

**13**; this corresponds to:

X is a **string of type n** (which is the same as a **variable of type n**)

where **x = φ[ X ]**.

See Type n string definition for the definition of a **type n string/ variable**.

So, **Typ _{n}(x)** is an assertion regarding a natural number

**x**, and corresponds to the assertion:

the symbol string X is a **type n string** of the formal system **P**

where **x = φ[ X ]**.

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

18.

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

**x** is a *string of first type*.

19.

**Typ _{n}(x) ≡ [n = 1 & Typ_{1}′(x)] ∨ [n > 1 & (∃v){v ≤ x & n Var v & x = R(v)}]**

**x** is a *string of n^{th} type.*

#### Relations 20 - 23: Assertions regarding formulas of the formal system

Relations 20. **Elf(x)** and 21. **Op(x, y, z)** correspond to the assertion that a particular combination of symbols is a particular type of formula of the formal system. **FR(x)** is a relation which corresponds, though not directly by Gödel numbering, to the notion of a series of formulas. These relations are not used elsewhere; their only purpose is for the definition of **Form(x)**.

Relation 23. **Form(x)** corresponds to the assertion that a particular combination of symbols is a formula of the formal system. It is defined in terms of **Elf(x)**, **Op(x, y, z)** and **FR(x)**.

20. **Elf(x) ** 21. **Op(x, y, z) ** 22. **FR(x) ** 23. **Form(x)**

**Elf(x)** is a relation that corresponds to the assertion:

the symbol string X is an elementary formula of the formal system **P.**

where **x = φ[ X ]**. See elementary formula.

**Op(x, y, z)** is a relation that corresponds to the assertion:

the symbol string X of the formal system **P** is of the form

**¬(Y)**, or

**(Y) ∨ (Z)**, or

**x∀(X)**,

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

See the formulas following the section elementary formula.

**FR(x)** is a relation which asserts that:

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

**x** corresponds to a ‘*series of formulas*’ (which may be a ‘*proof-schema*’), in that the prime factors of **x** have exponents that are the Gödel numbers of formulas, where each formula is either an elementary formula or a formula built up from elementary formulas. See Formula definition for definition of a formula of the system **P**.

**NB**: It is important to observe that this is not a direct correspondence by Gödel numbering as in the previous relations - 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.

Also note that where the function **n Gl x** occurs in the definition of **FR(x)**, it does *not* correspond to giving a single symbol of the formal system, which was the case in the previous relations - it corresponds to giving a symbol string of the formal system **P**.

**Form(x)** is a relation which asserts that:

the symbol string X is a formula of the formal system **P**

where **x = φ[ X ]**, and **x** is the exponent of the largest prime **p** in a number **n**, where:

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

**… p**

^{φ[ Ym ]}

See Formula definition for definition of a formula of the system **P**.

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

20.

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

**x** is an *elementary formula*.

21.

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

22.

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

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

23.

Form(x) ≡ (∃n){n ≤ (Pr[l(x)^{2}])^{x · [l(x)]2} & FR(n) & x = [l(n)] Gl n}^{[35]}

**x** is a *formula* (i.e: last term of a *series of formulas* **n***)*.

Footnotes:

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.