Gödel’s proof is the (meta-)mathematical counterpart of the paradoxical statement This sentence is false. In his epic 1979 debut book Gödel, Escher, Bach Douglas Hofstadter intertwines computer science, math, art, biology with a simplified version of the proof. In 2007 he revisits these ideas in I Am a Strange Loop. Hofstadter writes:
… at age fourteen I ran across Ernest Nagel and James R. Newman’s little gem, Gödel’s Proof, and through it I fell under the spell of the paradox-skirting ideas on which Gödel’s work was centered.
Nagel and Newman provide a succinct version of Gödel’s proof. You can feel how deeply it had influenced Hofstadter. NNs’ book arms the reader with the essential history of mathematics and logic, then presents the proof without bells and whistles.
Gödel’s ‘sentence’ does not say it is false. It says that it cannot be proved, actually I cannot be proved. ‘Proved’ means: Derived from a set of a few axioms, following a few allowed rules of transformation. Axioms and rules form a rigorous axiomatic system.
Theorems look familiar, containing the symbols for and, or, if…then. But they can also be seen as mere strings of concatenated characters. Strings are manipulated by purely typographical rules. Before Gödel shattered their world, logicians as Bertrand Russell had hoped that churning out all strings reachable by following the rules would result in the complete set of all true theorems, whereas no false statement would be generated. However, Gödel’s special theorem cannot be proved. But because it says of itself that it cannot be proved, it is true. Any system powerful enough to potentially express all true theorems will be incomplete.
Manipulating strings according to rules is isomorphic to performing arithmetic transformation on large integer numbers. Maybe this is more obvious today, as we learned to think about words as streams of bits processed by computers. In the 1930s Karl Gödel used an ‘elaborate hack with prime numbers to program without programming’, as computer scientist Scott Aaronson says in his book Quantum Computing Since Democritus.
Gödel assigned integer numbers to each character, as well as to each ‘line’ in a proof, and to the whole chain of steps in a proof. A single number represents the code needed to proceed from axioms to a theorem. His assignment of so-called Gödel numbers is unambiguous: The numbers assigned are used as exponents of a series of the lowest successive prime numbers in ascending order. Each prime is raised to the power of the Gödel number of a symbol; then all these exponentiated primes are multiplied. Via factorization of the final Gödel number the original ‘plain text’ could be recovered.
The first few integers – 1–12 in NN’s account – become the Gödel numbers of constants and characters. For example, the equal sign is gödelized as 5, and the existential quantifier ∃ (There exists) as 4. In the formal system all integer numbers are represented as successors of zero using the shorthand s for successor of: Number 1 is s0, number 2 is ss0, etc. Only the strings s and 0 need to be gödelized.
Example – a string of symbols who are commonly understood as: There exists an x, so that x is the successor of y.
(∃x)(x = sy)
(, ), ∃, s and = are assigned integers lower equal than 12. x and y are variables, placeholders for integer numbers. An unlimited set of variables is available: They are associated with prime numbers higher than 12.
The string of symbols is encoded in a series of integers:
8, 4, 13 ,…
( ∃ x ) ( x = s y ) | | | | | | | | | | 8 4 13 9 8 13 5 7 17 9
The Gödel number of the whole string / statement is obtained by using these numbers as exponents of the first primes:
28 . 34 . 513 . …
In a sequence of several steps, a Gödel number is assigned to each statement; then the statements’ numbers are used as exponents of the series of the ascending prime numbers. A whole proof is encoded in a unique number.
If theorem with Gödel number z can be proved, there exists a proof with Gödel number x. The fact that something can be proved, turned into a relation between integers. NN explain that Gödel took great pains in his paper to show that the relation between these numbers is primitive recursive. A primitive recursive function behaves in a predictable way – it makes only use of loops with known upper bounds.
The powerful axiomatic system under consideration has been designed to speak about all theorems in number theory. It can also express the relation between the Gödel numbers of proof and theorem. This function involving numbers is translated into the formal language, replacing e.g. each number by ssssss[an enormous number of s]ssss0. NN denote this formal relation by Dem(x.z) (Dem for demonstration).
If a proof exists, there exists a Gödel number x so that the theorem with Gödel number z cam be demonstrated via x:
(x is a bound variable; it could be called anything. There is no relation to x as used in the first equation. I am sticking to NNs’ notation).
If z cannot be proved, there does not exist any proof with Gödel number x:
If a theorem should speaks about itself, you need to feed it its own number. But by inserting the Gödel number ‘into itself’ would make the string longer and thus its own Gödel number would change. To circumvent this, substitution has to be implemented in a multi-level process, and by describing its own number using a calculation, rather that writing down all the digits.
A substitution function Sub with three parameters is introduced:
- The Gödel number of the statement to be changed, say n. The statement with this is number is yet to be defined.
- The Gödel number of the (free) variable to the replaced by a number, e.g. 17 (for y)
- The number to be inserted for the variable. To obtain the desired loop, this should also be n.
As Dem, Sub is written in the formal language. n is shorthand for a string of [n times s]0. Its output is the Gödel number of the statement after the substitution. Sub(n,17,n) is a number as a function of numbers, all numbers encoded in the formal language. It is not a simple replace() function – Sub takes care of rearranging the prime numbers – of adding a lot of factors in the multiplication that represent the many s in the number n.
The following first statement is nearly Gödel’s statement. It says that there is no proof for the theorem whose Gödel number is expressed as Sub(y,17,y).
has Gödel number n
The functions Dem and Sub are expressions in the formal language. It a well-formed string with a Gödel number which we call n. y is a free variable. The statement does not talk about itself. Nothing has happened yet.
The variable y shall be replaced by the number n – this is where self-referentiality is obtained:
II) also called G) ~(∃x)Dem(x,Sub(n,17,n))
with n as a shorthand for [n times s]0
Going from statement I) with Gödel number n to statement G) – we did a substitution:
- Input: The statement I) which has Gödel number n
- The Gödel number of the character to be replaced: 17 – which is associated with y. (We do not replace the string ’17’ in between the two y’s as that ’17’ would be gödelized as sss…sss0)
- The number we insert instead: Number n.
What we did was what we expect Sub(n,17,n) to do. As an output we expect the Gödel number of the statement after the replacement: The output of Sub(n,17,n) is the Gödel number of statement G) written in den formal language!
But this number – called g by NN – is the number referred to in the Dem function in G: G says that there is no proof for the theorem with Gödel number expressed as Sub(n,17,n).
If you imagined that G could be proved, you’d say there exists a proof with Gödel number x for the theorem whose Gödel number expressed formally is the result of Sub(n,17,n):
This is the negation of G – we’ve demonstrated ~G- If G would be demonstratable, ~G would also be demonstrable. If the axiomatic system is consistent, a theorem and its negation cannot be both demonstratable. Thus G cannot be demonstratable.
But either G or ~G must be true – and which of them it is, can be decided on the meta level: G says of itself that it is not a provable theorem, whereas ~G states that G has a proof. What G says is true, although is cannot be proved directly within the system, but only by resorting to meta-mathematical reasoning about the system. Only on the meta level we use the isomorphism between the characters used in the formal system and our familiar interpretation in terms of logic.