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.

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

A Step by Step Guide to Gödel’s Incompleteness Proof:
6: Gödel’s Relations of Natural Numbers 1 to 23


 

 


 

Note that (provided you have JavaScript enabled) clicking on (hideshow) will reveal further details, while clicking again will hide it. Also, clicking on (hideshow Gödel’s) will reveal relevant parts of Gödel’s text (shown in green), while clicking again will hide it. Please note that older browsers may not display some symbols correctly.

 

(like this)

 

(like this)

 

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 or as a PDF file at English translation of Gödel’s original proof, PDF fileGödel’s Proof - English translation.

 

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/functions. The relations/functions 1-45 are all primitive recursive; relation 46 is not defined as primitive recursive. Note that while in modern terminology, all variables of a relation are normally enclosed after the relation name in brackets (e.g. Rel(x, y) ), Gödel often places variables before and after the relation name (e.g. x Rel y) ). The names are mainly abbreviations of German words, see notes at the foot of this page for the words and the English translations.

 

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/functions, Gödel adds comments describing the relationship between symbol strings of the formal system that corresponds (by the Gödel numbering function) to the given relation between natural numbers. In the following, further notes are included to assist the reader. In these notes variables for symbols/symbol strings of the formal system 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/functions are purely number-theoretic - that is, that they only refer to natural numbers and variables whose domain is natural numbers. It is important not to use intuition to jump to conclusions, nor to make assumptions about the corresponding relationships between symbol strings of the formal system. Any such correspondence must follow in a logical manner.

 

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: here). 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] = 23.

 

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.

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/functions underpin the subsequent relations and functions. The details of the definitions are given below; clicking “show” will show the details for that definition.

 

1. x/y        (hideshow)

This is a relation that asserts that y is divisible by x with no remainder (hideshow Gödel’s).

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

 

x/y ≡ (∃z)[z ≤ x & x = y·z]

 

2. Prim(x)        (hideshow)

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, (hideshow Gödel’s)

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

 

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

 

3. n Pr x        (hideshow)

This is a function whose value is the nth largest prime number that is a factor of x (hideshow Gödel’s ).

e.g., 4 Pr [23 · 3 · 53 · 74 · 11 · 133]  =  7

(7 is the 4th largest prime factor of 23 · 3 · 53 · 74 · 11 · 133)

 

0 Pr x ≡ 0
(n + 1) Pr x ≡ εy[y ≤ x & Prim(y) & x/y & y > n Pr x]

 

4. n!        (hideshow)

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

 

5. Pr(n)        (hideshow)

This is a function whose value is the nth largest prime number (hideshow Gödel’s).

e.g., Pr(5) = 11 (the 5th largest prime is 11; the four smaller primes are 2, 3, 5 and 7)

 

Pr(0) ≡ 0
Pr(n + 1) ≡ εy[y ≤ {Pr(n)}! + 1 & Prim(y) & y > Pr(n)]

 

 

Relations/functions 6-23:
Relations/functions that correspond to the construction of symbol strings

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/relations are presented here in a different order to that given by Gödel; here they are grouped according to their similarity and purpose.

 

 

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

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 nth largest prime in the number x.

e.g., 5 Gl [23 · 33 · 51 · 711 · 1119 · 133] = 19 (the 5th largest prime in 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 nth position in the symbol string X (hideshow Gödel’s)

 

n Gl x ≡ εy[y ≤ x & x/(n Pr x)y & ¬(x/(n Pr x)y + 1 ) ]

 

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

 

e.g., if X = ff0(y1), then x = φ[X] = 23 · 33 · 51 · 711 · 1119 · 133

then 5 Gl [23 · 33 · 51 · 711 · 1119 · 133] = 19 to correspond to:

the operation of obtaining the 5th symbol of the symbol string ff0(y1), which is y1

where 19 = ψ[y1].

 

7. l(x)        (hideshow)

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

e.g., l(23 · 33 · 53 · 71) = 4 (there are only four unique prime factors: 2357)

 

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 (hideshow Gödel’s)

 

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

 

e.g., if X = fff0, then x = φ[X] = 23 · 33 · 51 · 71

then l(23 · 33 · 51 · 71) = 4 corresponds to:

the operation of counting the number of symbols in fff0, which is 4.

 

9. R(x)         (hideshow)

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

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 (hideshow Gödel’s).

 

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

 

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

and R(x) = 211 corresponds to:

the operation of obtaining the Gödel number of the symbol (, which is φ[ ( ] = R(ψ[ ( ]) = 211

 

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

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.

e.g., [23] * [23 · 33 · 53 · 71] = 23 · 33 · 53 · 73 · 111

 

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 (hideshow Gödel’s).

 

x * y ≡ εz[z ≤ [Pr{l(x) + l(x)}]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.”

 

e.g., if X = f and Y = fff0, then x = φ[X] = 23, and y = φ[Y] = 23 · 33 · 53 · 71

then 23  *  23 · 33 · 53 · 71 = 23 · 33 · 53 · 73 · 111 corresponds to:

the operation of concatenating the symbol strings f and fff0 to give ffff0.

 

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

For this function,

0 N x = φ[X]

1 N x = φ[fX]

2 N x = φ[ffX]

n N x = φ[fff…ffX], 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 (hideshow Gödel’s)

 

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

 

e.g., if X is f0, and φ[f0] = 23 · 31

then 3 N (23 · 31) = 23 · 33 · 53 · 73 · 111 corresponds to:

the operation of prefixing f0 by three instances of f, which gives ffff0.

 

17. Z(n)         (hideshow)

For this function,

Z(n) = n N R(1), and

R(1) = 21, so

Z(n) = n N 21= φ[fff…ff0], where there are n occurrences of f, since by the Gödel numbering function, 21 corresponds to the formal symbol for zero, which is 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 (hideshow Gödel’s)

 

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

 

e.g., Z(5) = φ[fffff0] = 23 · 33 · 53 · 73 · 113 · 131 corresponds to:

the operation of obtaining the Gödel number of fffff0

 

 

Note: Gödel is being rather disingenuous here in simply asserting that “Z(n) is the number-sign 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, f0, ff0, fff0, … , and it would not be allowable, for example to have an equality between 5 and fffff0, since if such equality were permissible, we would have φ[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, must be independent of the meta-language. We will return to this matter later when considering Gödel’s Proposition V.

 

 

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

This function can be thought of as multiplying the number x by an ‘initial’ 211, 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.g., E(23 · 33 · 53 · 73 · 111) = 211 · 33 · 53 · 73 · 113 · 131 · 1713

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 (hideshow Gödel’s)

 

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 ‘)’].”

 

e.g., if X = ffff0, and φ[ffff0] = 23 · 33 · 53 · 73 · 111

then E(x) = φ[ ( X ) ] = φ[(ffff0)] = 211 · 33 · 53 · 73 · 113 · 13 · 1713 corresponds to:

the operation of enclosing the symbol string ffff0 by brackets to give (ffff0).

 

13. Neg(x)         (hideshow)

This function can be thought of as multiplying the number x by an ‘initial’ 25 · 311, 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:

e.g., Neg(23 · 33 · 53 · 73 · 111) = 25 · 311 · 53 · 73 · 113 · 133 · 17· 1913

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 (hideshow Gödel’s)

 

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

 

Neg(x) is the negation of x.”

 

e.g., if X = ffff0, and φ[ffff0] = 23 · 33 · 53 · 73 · 111

then Neg(x) = φ[ ~(ffff0)] = 25 · 311 · 53 · 73 · 113 · 133 · 17· 1913 corresponds to:

the operation of enclosing the symbol string ffff0 by brackets and prefixing that by the negation symbol to give ~(ffff0).

 

14. x Dis y         (hideshow)

For this function,

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 (hideshow Gödel’s)

 

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

 

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

 

e.g., if X = f0, and φ[f0] = 23 · 31, and Y = ff0, and φ[ff0] = 23 · 33 · 51, then

x Dis y = φ[(f0) ∨ (ff0)] = 211 · 3· 51 · 713 · 117 · 1311 · 17· 193 · 231 · 2913 corresponds to:

the operation of enclosing the symbol strings f0 and ff0 by brackets and interposing the symbol between them to give (f0) ∨ (ff0).

 

15. x Gen y         (hideshow)

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) (hideshow Gödel’s).

 

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

 

e.g., if X is a type 1 variable, and x = φ[z1], and Y is some formula, where y = φ[Y]

then x Gen y = 223 · 39 · …      = 2ψ[z1] · 3ψ[∀] · … corresponds to:

the operation of bracketing the formula Y and prefixing it by z1

 

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

This is a relation, which asserts that pn, where p is a prime number greater than 13.

e.g., the relation 1 Var 17 applies; 2 Var 232 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. (hideshow Gödel’s)

 

n Var x ≡ (∃z)[13 < z ≤ x & Prim(z) & x = zn] & n ≠ 0

 

x is a variable of nth type.”

 

e.g., if X is the variable x3 of the formal system , and ψ[x3] = 17

then 3 Var 173 corresponds to:

the assertion that the symbol string x3 is a type 3 variable.

 

12. Var(x)         (hideshow)

This is a relation whose definition follows directly from the previous relation (n Var x), i.e., it asserts that x = pn, where 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 (hideshow Gödel’s)

 

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

 

x is a variable”

 

e.g., if X is the variable y2 of the formal system, and ψ[y2] = 192

then Var 192 corresponds to:

the assertion that the symbol string y2 is a variable of the formal system P.

 

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

Relations 18. Typ1′(x) and 19. Typn(x) correspond to the assertion that a particular combination of symbols is a sign of the formal system.

 

18. Typ1′(x)   19. Typn(x)         (hideshow)

 

Typ1′(x) is not used anywhere else, its only role is in the definition of the relation Typn(x).

Typn(x) asserts that either x = 23 · 33 · … · pq, or x = 2pn, where p, q and n must satisfy certain conditions.

 

Typ1′(x) asserts that either (hideshow Gödel’s):

x = 23 · 33 · … · p1, where p is some prime number; this corresponds to :

X is a symbol string of the form 0f0ff0fff0,

where x = φ[X].

or

x = 23 · 33 · … · pq, 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 x1, fx1, ffx1, fffx1, , or y1, fy1, ffy1, fffy1, , etc,

where x = φ[X].

 

Typ1'(x) ≡ (∃m,n){m,n ≤ x & [m = 1 ∨ 1 Var m] & x = n N [R(m)]}

 

Typ1′(x): x is a sign of first type.

 

 

 

For Typn(x), for the case when n = 1, the case is simply

Typ1(x) = Typ1′(x)

 

when n > 1, Typn(x) asserts that:

x = 2pn, or x = (2p)n, where p is some prime number greater than 13; this corresponds to:

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

where x = φ[X].

See type n sign definition: here for the definition of a type n sign/variable.

 

So, Typn(x) is an assertion regarding a natural number x, and corresponds to the assertion:

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

where x = φ[X]. (hideshow Gödel’s).

 

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

 

Typn(x)x is a sign of nth 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)         (hideshow)

 

Elf(x) is a relation that corresponds to the assertion (hideshow Gödel’s):

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

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

 

Elf(x) ≡ (∃y,z,n)[y,z,n ≤x & Typn(y) & Typn+1(z) & x = z * E(y)]

 

x is an elementary formula.

 

Op(x, y, z) is a relation that corresponds to the assertion (hideshow Gödel’s):

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.

 

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

 

FR(x) is a relation which asserts that (hideshow Gödel’s)

 

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. Each formula is either an elementary formula or a formula built up from elementary formulas. See formula definition: here for definition of a formula of the system P. 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.

 

NB: This is not a direct correspondence by Gödel numbering as in the previous relations, and there is no symbol string of the formal system P where x = φ[X].

 

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 which is either an elementary formula or arises from those preceding by the operations of negation, disjunction and generalization.”

 

Form(x) is a relation which asserts that (hideshow Gödel’s)

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:

 

n =  2φ[ Y1 ] · 3φ[ Y2 ] · 5φ[ Y3 ] · …   pφ[ X ]

 

See formula definition: here for definition of a formula of the system P.

 

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 formula (i.e. last term of a series of formulae 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

 


 

 


Diverse opinions and criticisms are welcome, but messages that are frivolous, irrelevant or devoid of logical basis will be blocked (comments will be checked before appearing on this site). Difficulties in understanding the site content are usually best addressed by contacting me by e-mail. Note: you will be asked to provide an e-mail address - this will only be used to notify you of replies to your comments - it will never be used for any other purpose, will never be displayed and does not require verification. Comments are common to the entire website, so please indicate what section of the site you are commenting on.

 

If you cannot see any comments below, it may be that a plug-in on your browser is blocking Disqus comments from loading. Avast anti-virus in particular is known to do this, especially with Internet Explorer and Safari. See Disqus Browser plug-in/extension conflicts or Why isn’t the comment box loading?.

 

 

Please wait for comments to load …  

 

The Lighter Side

 

NEWS

There’s something about Gödel by Francesco Berto

There is a new addition to the page Yet another flawed incompleteness proof, where Berto’s proof of incompleteness in his book There’s something about Gödel comes under scrutiny.

 

 

Easy Footnotes

I found that making, adding or deleting footnotes in the traditional manner proved to be a major pain. So I developed a different system for footnotes which makes inserting or changing footnotes a doddle. You can check it out at Easy Footnotes for Web Pages (Accessibility friendly).

 

 

O’Connor’s “computer checked” proof

I have now added a new section to my paper on Russell O’Connor’s claim of a computer verified incompleteness proof. This shows that the flaw in the proof arises from a reliance on definitions that include unacceptable assumptions - assumptions that are not actually checked by the computer code. See also the new page Representability.

 

 

New page on Chaitin’s Constant

There is now a new page on Chaitin’s Constant (Chaitin’s Omega), which demonstrates that Chaitin has failed to prove that it is actually algorithmically irreducible.

 

 

Updated: Diagonal Lemma

Flawed proofs of the Diagonal Lemma by Panu Raatikainen and Vann McGee have been added to the Diagonal Lemma web page.

Previous Blog Posts  

 

16th Mar 2015 Bishops Dancing with Pixies?

 

23rd Feb 2015 Artificial Intelligence

 

31 Mar 2015 Cranks and Crackpots

 

30 Apr 2015 The Chinese Room

 

Links  

 

For convenience, there are now two pages on this site with links to various material relating to Gödel and the Incompleteness Theorem

 

– a page with general links:

Gödel Links

 

– and a page relating specifically to the Gödel mind-machine debate:

Gödel, Minds, and Machines

 

Printer Friendly

 

All pages on this website are printer friendly, and will print the main content in a convenient format. Note that the margins are set by your browser print settings.


Note: for some browsers JavaScript must be enabled for this to operate correctly.

 

Comments

 

Comments on this site are welcome, please see the comment section.

 

Please note that this web site, like any other is a collection of various statements. Not all of this web site is intended to be factual. Some of it is personal opinion or interpretation.

 

If you prefer to ask me directly about the material on this site, please send me an e-mail with your query, and I will attempt to reply promptly.

 

Feedback about site design would also be appreciated so that I can improve the site.

 


Copyright © James R Meyer 2012 - 2016  
www.jamesrmeyer.com