Gödel’s incompleteness theorems have been hailed as “the greatest mathematical discoveries of the 20th century” — indeed, the theorems apply not only to mathematics, but all formal systems and have deep implications for science, logic, computer science, philosophy, and so on. In this post, I’ll give a simple but rigorous sketch of Gödel’s First Incompleteness Theorem. Formally, it states that:
Any consistent formal system within which a “certain amount of elementary arithmetic” can be carried out is incomplete; i.e., there are statements of the language of which can neither be proved nor disproved in .
This is a rigorous proof with a focus on software engineers and programmers. I based this post on this excellent lecture I found on YouTube a little while ago. When I first learned how to prove Gödel’s incompleteness theorems, it was in the context of a metalogic class that dealt with all kinds of confusing and deep topics like Henkin construction and transfinitary logic. But as it turns out, Gödel can be understood without much fanfare!
Introduction
We start on this journey by defining a couple of things. First, we define as a function that takes a positive integer and returns either 0
or 1
. Here’s an example of such an :
So, we see that or that . We can define however we want — as long as the output will either be a 0
or a 1
. Let be the set of all such functions .
We say that is computable if there exists a computer program (or proof) that takes as input and returns . It goes without saying that must complete within finite time and must be correct. So let’s look at some code. Is computable?
function isOdd(x) {
return (x % 2);
}
Looks like it! This program will always return 0
when is even and 1
when is odd. What about a more complicated example:
Is computable?
function isPrime(x) {
if(x < 2) return 0;
if(x == 2) return 1;
for(var i = 2; i < x; i++) {
if(x % i === 0) return 0;
}
return 1;
}
Courtesy of this Stack Overflow answer, it looks like it is. Let be the set of all computable functions in . We just found out (the hard way) that and are in — that is, they are computable.
But here’s the big question: are all functions in computable? Or, equivalently:
If , then Gödel was wrong, so we need to figure out a clever way to show that . In other words, we need to show that there are some functions that take positive integers as input and return either a 0
or a 1
that we simply cannot implement.
The Set-up
So how do you show that some functions are not computable? Well, let’s do it the old-fashioned way. Since we’re already using JavaScript, let’s just print out every single JavaScript program. Ever. To make things easy, we can order them alphabetically and by length (in lexicographical order). To make things even easier, we can just throw out programs that loop infinitely or don’t return a 1
or a 0
. When all is said and done, we’re left with an infinite number of programs that probably start out like this:
function F1(x) {
return 0;
}
function F2(x) {
return 1;
}
And further down the line…
function Fn(x) {
return 1 - 1;
}
And further down the line…
function Fn(x) {
return x / x;
}
And further down the line…
function Fn(x) {
return (x % 2); // hey, this is the isOdd function from before!
}
And even further down the line…
function Fn(x) {
return (x % 2) / 1;
}
And even further down the line…
function Fn(x) {
let someRandomVariable = x ^ x;
let abcd = someRandomVariable / y;
if (abdc > -12) return 0;
return 1;
}
You get the picture. Now we have every single possible program written in JavaScript that outputs 0
or 1
. In other words, we just populated : we now have a program that goes with every single computable function. Let’s put them in a big table called . The column headings indicate inputs (positive integers) and the rows indicate computable functions (and, implicitly, the programs that implement them).
1 | 2 | 3 | 4 | 5 | 6 | 7 | … | n | … | |
---|---|---|---|---|---|---|---|---|---|---|
… | … | |||||||||
… | … | |||||||||
… | ||||||||||
1 | 0 | 1 | 0 | 1 | 0 | 1 | … | … | ||
… | ||||||||||
0 | 1 | 1 | 0 | 1 | 0 | 1 | … | … | ||
… | ||||||||||
… | … | |||||||||
… |
You’ll notice that and also made it in our table (as fo and fp, respectively). So far, so good. It seems that we thought of everything. But let’s define a new function:
Where is the th function in table . First, let’s make sure we’re convinced that is well-formed. The input is an integer. will return either a 0
or a 1
, given that has a row populated in . And finally, or , so both cases are well-formed.
Therefore, is in , but is it in ?
The Proof
Seeing why can’t be in is pretty straightforward. Suppose is . Like we’ve seen so far, can either be 0
or 1
. But if , then . So, we have:
Whoops. Okay, so it wasn’t . That would be too easy. What about ? If , then . So, we have:
As it turns out, any computable function we pick out of (and implicitly ) will disagree with at at least one output. And therefore, we have the amazing finding that:
Conclusion
In other words, there are some things, like , we can’t prove or disprove in formal systems. Given that we’ve been working with JavaScript in this post, it makes sense that it’s impossible to reference the program’s own lexicographic index in . With that said, you might be tempted to think that there might be a way to “get around” this limitation; if your language was clever enough, perhaps. I’ll eventually write about Gödel’s Second Incompleteness Theorem, which drives the nail in the coffin: there’s no way to get around this.