Incompleteness Ex Machina

Sebastian Oberhoff
[Link]@[Link]

December 31, 2018

Abstract
In this essay we’ll prove Gödel’s incompleteness theorems twice. First, we’ll prove them the good
old-fashioned way. Then we’ll repeat the feat in the setting of computation. In the process we’ll discover
that Gödel’s work, rightly viewed, needs to be split into two parts: the transport of computation into the
arena of arithmetic on the one hand and the actual incompleteness theorems on the other. After we’re
done there will be cake.

It is a profoundly erroneous truism, repeated by all copy-books and by eminent people when they are making
speeches, that we should cultivate the habit of thinking of what we are doing. The precise opposite is the case.
Civilization advances by extending the number of important operations which we can perform without thinking
about them. Operations of thought are like cavalry charges in a battle—they are strictly limited in number, they
require fresh horses, and must only be made at decisive moments.

Alfred North Whitehead

1 The Incompleteness Theorems On Fast-Forward

Kurt Gödel’s incompleteness theorems are clearly the most significant results in the history of mathematics
(fight me). The first establishes that no single “proper” formal system can fully settle all mathematical
questions; that truth and provability are distinct concepts. The second shows that such a formal system also
can’t prove itself free of contradiction. If it tries, its wings will melt and it will crash to the ground.
Gödel accomplished these triumphs as follows. Suppose we’re given a formal system1 F that is capable of
reasoning about elementary arithmetic. Then, as Gödel showed through a lot of toil, it is possible to construct
a sentence G which essentially says “I am not provable in F”. Once he had built this sentence he then simply
asked: can G be proven or disproven—that is decided—in F?

Suppose G is provable:
Either ¬G is also provable:
⇒ Both G and ¬G are provable in F. Any system in which such a situation arises is also called
inconsistent.
Or ¬G isn’t provable:
⇒ Because G is provable there exists some concrete proof of G which we can write out inside F.
This is done using a device called Gödel numbering which allows numbers to talk about proofs.
It’s complicated.
⇒ Because this proof leads to G this allows us to construct a new proof of «G is provable»2 =
¬G3 . But we’re assuming ¬G isn’t provable. We have arrived at a genuine contradiction, not
just an inconsistency. So this can’t happen. We’ll use the shorthand “” for this in the future.
1 For the purpose of this discussion every formal system is effectively axiomatized by definition. If you don’t know what that

means, don’t worry about it.

2 Whereas regular quotes (“”) perform their usual function, guillemets («») surround formal sentences denoted by their English

description. Also “=” doesn’t always have to mean exact equality. I also use it to relate sentences which are merely logically
equivalent, provided this is obvious.
3 Beware: the negation of G = «G isn’t provable», denoted ¬G, is not «¬G isn’t provable». It’s «G is provable». These are

very different sentences. Furthermore, it’s important to notice that ¬G isn’t being self-referential when it says “G is provable”.
¬G is really more like an evil twin that’s telling lies about its sibling (assuming the system F as a whole is honest).

1
 Suppose ¬G is provable: This is what it means to disprove G. Also, mind the fact that this case and the
previous aren’t mutually exclusive. That’s where I use either/or.
Either G is also provable:
⇒ F is inconsistent.
Or G isn’t provable:
⇒ Because ¬G is provable there exists some concrete proof of ¬G which we can write out inside
F.
⇒ But in order to force a contradiction we’ll have to find a proof of G = «G isn’t provable», not
«¬G is provable» (uh-oh).
⇒ We can’t seem to find a proof of G despite the fact that its existence is exactly what ¬G =
«G is provable» asserts.
⇒ We haven’t convicted F of an outright inconsistency. But something is still very, very wrong
with it.

These deductions, as well as the ones in the proofs to follow, are deliberately written in such a painstaking
style in order to make the similarities between the first and second set of proofs as plain as possible. These
are the decisive moments of our battle.
Now, it would be nice to say that we’ve proven that, if our formal system F is consistent, then G is
undecidable. Unfortunately our second case wasn’t strong enough. So, just as Gödel did in 1931, we’ll have
to settle for a weaker formulation:
Theorem 1 (First Incompleteness Theorem – Original Version). Let F be an honest4 formal system capable
of reasoning about elementary arithmetic. Then F is incomplete; it contains a sentence that can neither be
proven nor disproven in F.
Proof. We just did that.
Okay, I pulled a fast one there. Crucially, I skipped over a rather important concept: honesty. What
exactly do I mean by that?
As the name suggests, an honest formal system is a formal system that speaks the truth. We can believe
the claims it makes. In particular, if our F is honest and proves ¬G = «G is provable», then, just as ¬G says,
it really is the case that G is provable. This is how we can force a contradiction out of the second case.
But honesty is a stronger assumption than consistency. An honest formal system is always consistent.
After all, an inconsistent formal system contains a sentence S such that both S and ¬S is provable.5 One
of these must be telling a lie. However, a consistent formal system isn’t necessarily honest. Just take the
following real life example: Some people claim that imperial units are an acceptable system of measurement.
These people are dishonest. They claim something that’s so patently false Whitehead would’ve demanded
their heads. But if they’re clever about it, a few of them can still maintain the internal consistency of their
deceptions.
The way this might show up in our formal system F is like so: It is conceivable that we can prove ¬G = «G
is provable» while G in fact isn’t provable. This would lead to a curious situation I’ll call sub-inconsistency 6
where for any n ∈ N the sentence «G doesn’t have a proof shorter than n» = G can be proven in F by just
going through all possible proofs up to length n and pointing out that none of them do the trick. Yet the
summarizing sentence «G doesn’t have a proof shorter than n for any n ∈ N» = G is not only unprovable
but flat out contradicted by ¬G. This is why Gödel had to assume honesty (or at least super-consistency) in
his original proof. Basically, he had to seize F by the collar and shout: “No games, dammit!”
Okay, but isn’t there a less violent way to prevent this kind of sub-terfuge? Indeed there is. In 1936 J.
Barkley Rosser found a way to demonstrate the improved
Theorem 2 (First Incompleteness Theorem – Rosser’s Version). Let F be a consistent formal system capable
of reasoning about elementary arithmetic. Then F is incomplete.
4 The traditional term is “sound”. But when explaining this concept to my mother I had to admit that “honesty” is much

more fitting. Also, I’ve been burned by overloaded usage of the term “soundness” in the past.
5 Notice how this mirrors incompleteness which says that for some sentence S neither S nor ¬S is provable.
6 Also known under the name “ω-inconsistency”. Let’s spare our horses.

2
Proof. In hindsight Rosser’s trick is quite simple. Instead of formalizing “I am not provable” he formalized
the sentence “For every proof of me there exists a shorter disproof”. Let’s refer to this sentence as R and see
how R can help us.
Suppose R is provable:
⇒ There exists some shortest proof r of R.
Either there is a proof of ¬R that’s shorter than r:
⇒ F is inconsistent. 
Or there isn’t:
⇒ We can go through all strings up to the length of r and determine that none of them are a
proof of ¬R.
⇒ We can write out this list inside F and point out that all longer strings are at least as long as
r.
⇒ This allows us to construct a new (longer) proof of «There exists a proof of R with no shorter
disproof (namely r)» = ¬R.
⇒ F is inconsistent. 
Suppose ¬R is provable:
⇒ There exists some shortest proof r 0 of ¬R.
Either there is a proof of R that’s shorter than r 0 :
⇒ F is inconsistent. 
Or there isn’t:
⇒ We can go through all strings up to the length of r 0 and determine that none of them are a
proof of R.
⇒ We can write out this list inside F and point out that all longer strings are at least as long as
r 0.
⇒ This allows us to construct a new (longer) proof of «For every proof of R there exists a shorter
disproof (namely r 0 )» = R.
⇒ F is inconsistent. 

Whereas Gödel’s original proof was limping on one leg, Rosser’s version is perfectly balanced, as all things
should be, allowing the stronger result.
Finally, there’s one more summit to conquer in this mathematical Himalaya. That’s the Second Incom-
pleteness Theorem.
Theorem 3 (Second Incompleteness Theorem). Again, let F be a consistent formal system capable of rea-
soning about elementary arithmetic. Then F can’t prove its own consistency.

Perhaps the fact that this theorem speaks of consistency, not honesty, makes you a little suspicious. Is this
another one of Rosser’s upgrades? No. For the Second Incompleteness Theorem Gödel only needed half of his
First Incompleteness Theorem. And as luck would have it this was exactly the half that spoke of consistency.
Proof. Let’s assume for the purpose of contradiction that F can prove its own consistency

⇒ The first half of the proof for the First Incompleteness Theorem can be read as a proof by contradiction
that if F is consistent, then G isn’t provable.
⇒ Using the fact that «G isn’t provable» = G, this can be stated more concisely as “F is consistent =⇒
G”.

3
 ⇒ As Gödel himself pointed out with some hand-waving, there wasn’t actually anything in the reasoning
we used to prove this that we couldn’t carry out just as well in F. So «F is consistent =⇒ G» is
actually a theorem in F.
⇒ We’re assuming that F can prove «F is consistent». So by modus ponens7 F can also prove G.
⇒ But G can’t be proven. 

Moral of the story: if you declare yourself a very stable genius, you’re not.[1]

2 The Rise Of The Machines

We now come to the dramatic turn in our story. Namely, we’re about to demand that our formal system F
can reason about algorithms8 , not just elementary arithmetic. And then we’ll reprove all three of the previous
results on top of that.
What could possibly provoke such heresy? Well, you may recall that in the prequel we relied quite heavily
on the fact that both G and R could somehow be constructed in F. But we never actually performed these
constructions. We also liberally made assertions of the form: “we can list out all proofs up to length n inside
F”. But F is about numbers, not formal sentences. How is all of this ultimately accomplished?
The reality is that I hand-waved these details for a reason. They are non-trivial in the extreme (ideal
exercises for the reader!). That’s because, from a modern perspective, Gödel basically had to teach pro-
gramming to formal systems that were about arithmetic. And he had to do it half a decade before the first
models of computation were even devised. This is where all the tough technical work had to be done. The
incompleteness theorems themselves were mere victory laps at the end.
This delimitation between the different parts of Gödel’s work is frequently passed over without comment
but will become even more apparent as we move on. In fact, setting the record straight on this matter is really
the main point of this essay. By placing computation—for example in the form of Turing machines—directly
into the bedrock of our formal system our task will become orders of magnitude simpler. Gödel had to scale a
vertical cliff to convince his peers that “s is a proof of S” could be expressed within the confines of arithmetic.
We on the other hand, aided by the ski lift built by Turing and his apostles, can see at a glance that the same
could be checked by a computer. Let’s exploit that.
Anybody who still harbors a nostalgic longing for “elementary arithmetic” can then take on the separate
task of showing how to ponder computation in the realm of the natural numbers. Perhaps one can also
study computation starting from a different base camp such as knot theory. Who knows? (I’m completely
clueless regarding knot theory.) Meanwhile, we will have the incompleteness theorems above the clouds all to
ourselves.

3 To Halt Or Not To Halt

Alright, here we go. The only ingredient we need to prepare is the unsolvability of the Halting Problem due
to Alan Turing in 1936.
Lemma 1 (Unsolvability Of The Halting Problem). There’s no algorithm that can determine for another
arbitrary algorithm A whether A(A) (A running on its own source code) halts.

Proof. Suppose H solves the Halting Problem. Then one could create the following algorithm:
7 Modus ponens is the inference rule that from X and «X =⇒ Y» follows Y.
8 Algorithm, Turing machine, and computer program are basically synonyms in my vocabulary.

4
H(A) {
i f H(A) = f a l s e {
halt ;
}
i f H(A) = true {
i n f i n i t e loop ;
}
}

Question: does H(H) halt?

Either H(H) halts: Or H(H) doesn’t halt:
⇒ H(H) returns true ⇒ H(H) returns false.
⇒ H(H) doesn’t halt.  ⇒ H(H) halts. 

Either way we get a contradiction.

Easy peasy. As you’d expect of a mere lemma. We’re now ready for the First Incompleteness Theorem.

Theorem 4 (First Incompleteness Theorem – Original Version By Computation). Let F be an honest formal
system capable of reasoning about algorithms. Then F is incomplete.
Proof. Suppose F was complete. Then we could solve the Halting Problem using the following algorithm:
H(A) {
for s ∈ a l l p o s s i b l e s t r i n g s 9 {
i f s i s a p r o o f i n F t h a t A(A) doesn ’ t h a l t {
return f a l s e ;
}
i f s i s a p r o o f i n F t h a t A(A) h a l t s {
return true ;
}
}
}

Because F is complete this search will eventually hit upon a proof of either «A(A) halts» or «A(A) doesn’t
halt». And because F is honest, we’ll be able to trust its judgment. That determines whether or not A(A)
halts. But, as we saw only a moment ago, it’s impossible to solve the Halting Problem. So F couldn’t have
been complete.

That certainly went by a lot faster than my last reading of Gödel, Escher, Bach. Though, if you’ve ever
had the incompleteness theorems explained to you by a computer scientist, then you probably saw this proof
coming a mile away. And for good reason. It’s a very elegant little proof; deserving of its popularity.

4 Welcome To The World Of Mirrors

Nevertheless, this isn’t the proof I want to use going forward. The reasons are threefold:
• The jump from honesty to consistency is rather tricky.
• The Second Incompleteness Theorem doesn’t follow naturally at all.
• The parallels to Gödel’s and Rosser’s original proofs are lost. (This one’s the biggie.)

We can do better. Watch this:

9 If it wasn’t clear: we’re iterating in increasing length. This procedure is sometimes also jokingly referred to as the British

Museum algorithm because it’s akin to using chimps in front of typewriters in an attempt to reproduce all the books in the
British Museum.

5
Proof. Consider the following algorithm:
P(A) {
for s ∈ a l l p o s s i b l e s t r i n g s {
i f s i s a p r o o f i n F t h a t A(A) doesn ’ t h a l t {
halt ;
}
}
}

I now claim that «P(P) doesn’t halt» is undecidable in F. Let’s call this sentence G̈ because it’s the perfect
analogue of Gödel’s G.10 The critical new feature of G̈ is that its construction has become just a small matter
of programming. If we go through the alternatives, we find:
Suppose G̈ is provable:
Either¬G̈ is also provable:
⇒ F is inconsistent. 
Or ¬G̈isn’t provable:
⇒ Because G̈ is provable P(P) will eventually find such a proof after some sequence of steps which
we can write out in F.
⇒ Because this sequence leads to a terminal state this gives a proof of «P(P) halts» = ¬G̈. 
Suppose ¬G̈ is provable:
Either G̈ is also provable:
⇒ F is inconsistent. 
Or G̈ isn’t provable:
⇒ Because ¬G̈ is provable P(P) will eventually find such a proof after some sequence of steps
which we can write out in F.
⇒ But in order to halt P(P) will have to find a proof of G̈ = «P(P) doesn’t halt», not ¬G̈ (uh-oh).
⇒ P(P) doesn’t seem to halt despite the fact that this is exactly what ¬G̈ = «P(P) halts» asserts.
⇒ F is dishonest. 

Is anybody else experiencing déjà vu? Note that, whereas in the previous proof we only established the
existence of undecidable sentences in F, here we actually have a concrete undecidable sentence on our hands.
And we didn’t even need the Halting Problem!
Moreover, almost miraculously, the two cases for G̈’s provability run into the exact same problems as G.
In the first case F plants its Face squarely in inconsistency. In the second one the precise correlation between
the information that F communicated and the facts insofar as they can be determined and demonstrated is
such as to cause epistemological problems of sufficient magnitude as to lay upon the logical and semantic
resources of the English language a heavier burden than they can reasonably be expected to bear. It told a
lie.[2]
Upon closer inspection, we’re even dealing with the same kind of lie:
sub-inconsistency
After all, if G̈ isn’t provable, then one can still prove that P(P) hasn’t halted after n steps for every n ∈ N
by just writing out n steps of the computation in F and noting that it’s still running. But the summarizing
sentence «P(P) hasn’t halted after n steps for any n ∈ N» = G̈ is mysteriously absent. If F then goes on to
prove ¬G̈ = «P(P) halts», this will be a false promise. Yet we’re unable to catch it red-handed.
And if you thought that was neat, just wait until you see Rosser’s trick. As you may recall, this one worked
by patching the asymmetry between the two cases in Gödel’s original argument. Let’s see what happens if
we try the same here.
10 You can think of the two dots as Clark Kent’s glasses.

6
Theorem 5 (First Incompleteness Theorem – Rosser’s Version By Computation). Let F be a consistent
formal system capable of reasoning about algorithms. Then F is incomplete.
Proof. Consider the following algorithm:
B(A)11 {
for s ∈ a l l p o s s i b l e s t r i n g s {
i f s i s a p r o o f i n F t h a t A(A) doesn ’ t h a l t {
halt ;
}
i f s i s a p r o o f i n F t h a t A(A) h a l t s {
i n f i n i t e loop ;
}
}
}

This time our undecidable sentence is (you guessed it) R̈ = «B(B) doesn’t halt».
Suppose R̈ is provable:

⇒ There exists some shortest proof r̈ of R̈.

Either there is a proof of ¬R̈ that’s shorter than r̈:
⇒ F is inconsistent. 
Or there isn’t:
⇒ B(B) will go through all strings shorter than r̈ and determine that none of them are a proof of
¬R̈.
⇒ We can write out this computation in F and point out that B(B) will then find r̈ and enter a
terminal state.
⇒ This gives a (longer) proof of «B(B) halts» = ¬R̈.
⇒ F is inconsistent. 
Suppose ¬R̈ is provable:

⇒ There exists some shortest proof r̈ 0 of ¬R̈.

Either there is a proof of R̈ that’s shorter than r̈ 0 :
⇒ F is inconsistent. 
Or there isn’t:
⇒ B(B) will go through all strings shorter than r̈ 0 and determine that none of them are a proof
of R̈.
⇒ We can write out this computation in F and point out that B(B) will then find r̈ 0 and enter
an infinite loop.12
⇒ This gives a (longer) proof of «B(B) doesn’t halt» = R̈.
⇒ F is inconsistent. 

I feel like I’m watching a reboot (in more than one sense). We can even recognize the phenomenon of
finding either shorter or longer disproofs and proofs; pure satisfaction.
Alright, time for the grand finale.
11 I picked the letters P and B because they visually somewhat resemble the programs they denote. (Also, this is why I placed

the “doesn’t halt” case first.)

12 Proving that a program runs forever raises the specter ( ) of sub-inconsistency. But rest assured. Any formal system capable

of reasoning about algorithms can prove that “while true {}” runs forever; otherwise it ought to be ashamed of itself.

7
Theorem 6 (Second Incompleteness Theorem By Computation). One last time, let F be a consistent formal
system capable of reasoning about algorithms. Then F can’t prove its own consistency.
We could continue using B for the Second Incompleteness Theorem. But that would be ugly. Gödel didn’t
need Rosser’s help for his proof. Neither shall we.
Proof. Let’s assume for the purpose of contradiction that F can prove its own consistency

⇒ The first half of our new proof for the First Incompleteness Theorem can be read as a proof by contra-
diction that if F is consistent, then P(P) doesn’t halt.
⇒ Using the fact that «P(P) doesn’t halt» = G̈, this can be stated more concisely as “F is consistent =⇒
G̈”.
⇒ Now we simply observe (with some faith) that there wasn’t actually anything in the reasoning we used
to prove this that we couldn’t carry out just as well in F. So «F is consistent =⇒ G̈» is actually a
theorem in F.
⇒ We’re assuming that F can prove «F is consistent». So by modus ponens F can also prove G̈.
⇒ But then P(P) will eventually find this proof and halt. 

5 Taking Off The Glasses

At this point I can’t even tell the difference between the classical approach and the algorithmic retelling
anymore. Can you? All these proofs are the exact same as before! In fact, the relation is so strong that I
was able to write the latter ones by copy-pasting wholesale and then tinkering a little. Clearly, this can’t be
coincidence. There must be a deeper reason for this overabundance of similarities. And there is. Perhaps
you’ve already caught on long ago. Or perhaps Clark Kent’s glasses fooled you too. Drum whirl please.
Recall once more what G̈ says. It says “P(P) doesn’t halt”. But P(P) isn’t just executing some simple
infinite loop. It’s looking for something. It’s scouring the proofs in F for a proof of «P(P) doesn’t halt» =
G̈. G̈’s claim that P(P) will never find a proof of G̈ is echoing G’s claim that the original computers, you and
me, will never find a proof of G. In other words, G̈ is also proclaiming to the world:
“I am not provable!”
Exercise: Take off R̈’s glasses as well.
This means I could’ve organized this presentation very differently. I could’ve just made these observations
right away and then said: “Now reread the first section. ”. I’ve been wasting your time!

6 Refactoring The Incompleteness Theorems

Gödel was programming the integers. That is that. And he didn’t even know it at the time; truly impressive.
I think this feat deserves to be encapsulated with its own theorem. Perhaps we can come together and save
posterity from the grim fate of also only realizing this much later in their lives. It’s for the kids. And for the
horses.

Theorem 7 (Turing Completeness of Elementary Arithmetic). Every formal system capable of reasoning
about elementary arithmetic can also reason about algorithms.
I’ll leave the details to smarter people. After all, I did recently score in the bottom 7% of the GRE’s
analytical writing section (come on!).

(Thank you so much for your attention! The cake I promised in the abstract is on its way. Please stand by.)

8
References
[1] Donald Trump, Twitter on 6. January 2018 (I just want to be able to say that Donald Trump has been cited when discussing
the fundamentals of mathematics.)
[2] Yes, Prime Minister, The Tangled Web
[3] Algorithm B also appears in Scott Aaronson’s Quantum Computing since Democritus where he uses it to give a pseudo
proof of the Second Incompleteness Theorem. It was in plugging the holes in Aaronson’s argument that these ideas took their
origin.

Closing Credits
I’d like to thank Scott Aaronson for his feedback as well as for being gracious enough to post this essay on his blog. Additionally,
Cristopher Moore has provided many helpful comments. Finally, I strongly urge you to read Cristopher Moore and Stephan
Mertens’ book The Nature of Computation. It’s what made me fall in love with computer science.