Copyright © James R Meyer 2012 - 2017 www.jamesrmeyer.com
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 file.
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.
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.
This is an assertion regarding the natural numbers v, n and x, and it corresponds to the assertion:
at the nth 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 (x1∀ B) C, where A, B and C are symbol strings of the formal system, and where x1 is a variable, and ∀ is the quantifier symbol for ‘for all’. Then the quantifier on the variable x1 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, regardless of where the variable V might be in that string.
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 nth 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 (hideshow Gödel’s).
“The variable v is bound at the nth place in x.”
v Fr n,x corresponds to the assertion:
V is a variable, and it occurs as the nth symbol in the formula X, and it is free at that position
“The variable v is free at the nth place in x.”
v Fr x corresponds to the assertion:
V is a variable, and it occurs as a free variable in the formula X
“v occurs in x as a free variable.”
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.
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 Sbk(x v|y); these functions are not used anywhere else.
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 x1 at only one position in the formula. Then the Gödel number corresponding to that formula X will be like this :
φ[X] = 2a · 3b · 5c … · p17 · ju · kw · ly · mz · …
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 = ψ[x1].
If the symbol string which will be substituted is say, ffff0, then
φ[ffff0] = 23 · 33 · 53 · 73 · 111
Sb(x v|y) = 2a · 3b · 5c … · p3 · j3 · k3 · l3 · m1 · qu · rw · sy · tz · …
This corresponds to the substitution of the type 1 variable x1 by the type 1 sign ffff0
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. 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 sign as the variable v. Hence where Sb is used in the following functions/relations, there must be the added stipulation to that effect (hideshow Gödel’s).
“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 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. 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.”
Note that, depending on what version of the translation you are using, Sb may be represented in this format:
which is the format using in Gödel’s original paper.
Functions 32 and 33 define some axioms of the formal system. Relations 34-42 inclusive are relations that use the previously defined relations/functions to define which Gödel numbers correspond to the axioms of the formal system.
These define the logical equivalent of ‘implies’, ‘and’, ‘equivalence’, and ‘there exists’ (see also the axioms of the system P)
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 nth type-lift of the formula x (see Type-lift).
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 (hideshow Gödel’s).
“To the axioms I, 1 to 3, there correspond three determinate numbers, which we denote by z1, z2, z3.”
Relation 35, A1-Ax(x) defines that x is a Gödel number that corresponds to an axiom defined by Axiom Schema II.1. Similarly for A2-Ax(x), A3-Ax(x) and A4-Ax(x) for axioms defined by the Axiom Schemas 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
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]
This relation is only used in the definition of relation 38 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.”
“z contains no variable bound in y at a position where v is free.”
This relation asserts that X is an axiom given by the Axiom Schema III.1, where x = φ[X].
This relation asserts that X is an axiom given by the Axiom Schema III.1, where x = φ[X].
This relation asserts that X is an axiom given by the Axiom Schema IV.1, where x = φ[X].
This relation 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. (hideshow Gödel’s)
“To the axiom V, 1 there corresponds a determinate number z4.”
This relation asserts that x is a number that corresponds by Gödel numbering to an axiom of the formal system P.
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.
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
“x is an immediate consequence of y and z”
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 axiom or a formula given by the rules of inference of th 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].
“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)”
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φ[ Y ]
Note that, as for relation 44 above, there is no symbol string of the formal system P where x = φ[X].
“x is a proof of the formula y”
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φ[ 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.]”
Below is a list of names used for various relations in the text, which are mostly abbreviations of German words; translations are provided below:
|E||Einklammern||= include in brackets|
|Elf||Elementarformel||= elementary formula|
|Fl||unmittelbare Folge||= immediate consequence|
|Flg||Folgerungsmenge||= set of consequences|
|FR||Reihe von Formeln||= series of formulae|
|Pr||Primzahl||= prime number|
|Prim||Primzahl||= prime number|
|R||Zahlenreihe||= number series|
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 …
There is now a new page on Lebesgue measure theory and how it is contradictory.
There is now a new page Halbach and Zhang’s Yablo without Gödel which demonstrates the illogical assumptions used by Halbach and Zhang.
It has come to my notice that, when asked about the demonstration of the flaw in his proof (see A Fundamental Flaw in an Incompleteness Proof by Peter Smith PDF), Smith refuses to engage in any logical discussion, and instead attempts to deflect attention away from any such discussion. If any other reader has tried to engage with Smith regarding my demonstration of the flaw, I would be interested to know what the outcome was.
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).
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.
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.
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:
– and a page relating specifically to the Gödel mind-machine debate:
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.
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 - 2017