I just finished Douglas Hofstadter’s amazing book, Gödel, Escher, Bach which touches on (among many other things) formal systems, artificial intelligence, isomorphism, self-reference, and Gödel’s incompleteness theorem. The latter is what I’d like to talk about here. I want to preface all of this by saying that I probably only understand 20% of the logic which Hofstadter lays out, so critique is welcome. In fact, my reason for writing this post is to help myself better understand this seemingly paradoxical theorem (and also to evangelize this book, which is outstanding).
Gödel’s Incompleteness Theorem
The theorem states:
Any consistent formal system F within which a certain amount of elementary arithmetic can be carried out is incomplete; i.e., there are statements of the language of F which can neither be proved nor disproved in F.
Another way of saying this is that any sufficiently powerful formal system will have statements that it cannot prove or disprove. This represents a hole in the formal system, and no matter how many new rules and axioms are added some holes will always remain. Hofstadter uses a formal system he invented called Typographical Number Theory which I don’t want to get into here. Instead, think of gradeschool algebra which comes with some axioms (eg, \(a + b = b + a\), \(a(b+c) = ab + ac\)). This theorem suggests that there are true statements of albebra which cannot be proven within the framework of algebra. No matter how many axioms we add, there will always be a “hole” in our system in which truths can hide and never be proven.
Gödel Numbering
Gödel Numbering is a technique which allows a statement of mathematics to make meta-statements about itself. Without getting into the details, think of Gödel Numbering as a function \(G(x)\) which takes as input a statement of mathematics (\(x\)) and produces a unique number. The properties of that number alone (eg, primeness) allow us to determine if the statement \(x\) is provable by the axioms of mathematics or not. For example sake, let’s massively simplify things and pretend that any statement whose Gödel Number is prime is provable. We might have the following pairs of \(x\) and \(G(x)\)
| x | G(x) |
|---|---|
| 0=0 | 3 |
| 1=0 | 4 |
| a + b = b + a for any b and any a | 19 |
| a + 1 = a for some a | 20 |
In our super simplified system, the provable statements have prime Gödel Numbers and the unprovable statements do not. Real life is not this simple, unfortunately, but the idea is the same.
The Arithmoquine
Hofstadter introduces a function he calls an Arithmoquine, which replaces a free variable in a statement with the Gödel Number of the statement itself.
Let’s use this new Arithmoquine function to make a statement called \(A\) with a free variable \(x\):
A: The statement whose Gödel Number is x, when Arithmoquined, is not provable from the axioms of mathematics
This statement \(A\) has a Gödel Number like any other statement of mathematics. Let’s call its Gödel Number \(u\).
Now, the trick. Let’s Arithmoquine \(A\) and call it \(G\):
\(G\) = Arithmoquine(\(A\)): The statement whose Gödel Number is \(u\), when Arithmoquined, is not provable from the axioms of mathematics
Put another way
\(G\): A, when Arithmoquined, is not provable from the axioms of mathematics
Put another way
\(G\): \(G\) is not provable from the axioms of mathematics
Put yet another way
\(G\): I am not provable from the axioms of mathematics
Let’s assume \(G\) is a false statement. This implies that \(A\) is provable from the axioms of mathematics, meaning we have a provable statement in math which is false. We assume math is consistent, and can have no contradictions, therefore we reason from outside the system that \(G\) must be true. (nb, Hofstadter spends a lot of time going down this path, and introduces Supernatural Numbers as a way to resolve the contradiction with \(G\) being false)
If \(G\) is true, then by definition \(G\) is not provable. Here we have the hole, a true statement which we cannot prove. This might seem like less of a problem, as we can make a new formal system, mathematics+, and add \(G\) as an axiom. However, we can do the same trick again, and make another true but non-provable statement in mathematics+ where \(G\) is an axiom. This corner case never goes away, and no matter how hard we try (mathematics+, mathematics++, mathematics\(\infty\)+) we are left with an incomplete formal system, which will always have some true statements which cannot be proved.