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.

Featuring: the ghost of ~sub-inconsistency~

This kind of logic always makes my head spin a bit, but these results are surprisingly important for understanding some of the concerns driving (post-)modern mathematics. Thinking about them in terms of programs definitely makes the results feel a bit more natural!

This is not so much an academic paper as it is a blog post written in LaTeX. If you already know about Gödel, it's a pretty good read; if not, but you know a bit about programming, you'd probably be best served by skimming through section 1, reading sections 2-6, then looking back through 1 if you're still curious about anything there.