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 SS within which a “certain amount of elementary arithmetic” can be carried out is incomplete; i.e., there are statements of the language of SS which can neither be proved nor disproved in SS.
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 FF as a function that takes a positive integer and returns either 0
or 1
. Here’s an example of such an FF:
isOdd(x)={0x is even1x is oddisOdd(x)={0x is even1x is odd
So, we see that isOdd(2)=0isOdd(2)=0 or that isOdd(38943981)=1isOdd(38943981)=1. We can define FF however we want — as long as the output will either be a 0
or a 1
. Let QQ be the set of all such functions FF.
We say that FF is computable if there exists a computer program (or proof) PP that takes as input xx and returns F(x)F(x). It goes without saying that PP must complete within finite time and must be correct. So let’s look at some code. Is isOdd(x)isOdd(x) computable?
function isOdd(x) {
return (x % 2);
}
Looks like it! This program will always return 0
when xx is even and 1
when xx is odd. What about a more complicated example:
isPrime(x)={0x is not prime1x is primeisPrime(x)={0x is not prime1x is prime
Is isPrimeisPrime 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 AA be the set of all computable functions in QQ. We just found out (the hard way) that isOddisOdd and isPrimeisPrime are in AA — that is, they are computable.
But here’s the big question: are all functions in QQ computable? Or, equivalently:
A?=QA?=Q
If A=QA=Q, then Gödel was wrong, so we need to figure out a clever way to show that A⊂QA⊂Q. In other words, we need to show that there are some functions that take positive integers xx 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 FF 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 AA: we now have a program that goes with every single computable function. Let’s put them in a big table called TT. 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 | … | |
---|---|---|---|---|---|---|---|---|---|---|
f1f1 | f1(1)f1(1) | f1(2)f1(2) | f1(3)f1(3) | f1(4)f1(4) | f1(5)f1(5) | f1(6)f1(6) | f1(7)f1(7) | … | f1(n)f1(n) | … |
f2f2 | f2(1)f2(1) | f2(2)f2(2) | f2(3)f2(3) | f2(4)f2(4) | f2(5)f2(5) | f2(6)f2(6) | f2(7)f2(7) | … | f2(n)f2(n) | … |
… | ||||||||||
fofo | 1 | 0 | 1 | 0 | 1 | 0 | 1 | … | fo(n)fo(n) | … |
… | ||||||||||
fpfp | 0 | 1 | 1 | 0 | 1 | 0 | 1 | … | fp(n)fp(n) | … |
… | ||||||||||
fifi | fi(1)fi(1) | fi(2)fi(2) | fi(3)fi(3) | fi(4)fi(4) | fi(5)fi(5) | fi(6)fi(6) | fi(7)fi(7) | … | fi(n)fi(n) | … |
… |
You’ll notice that isOddisOdd and isPrimeisPrime 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:
ˉf(i)=1−fi(i)¯f(i)=1−fi(i)
Where fifi is the iith function in table TT. First, let’s make sure we’re convinced that ˉf¯f is well-formed. The input ii is an integer. fi(i)fi(i) will return either a 0
or a 1
, given that fifi has a row populated in TT. And finally, 1–0=11–0=1 or 1–1=01–1=0, so both cases are well-formed.
ˉf(i)=will return 0 or 1⏞1−fi(i)⏟will return 0 or 1
Therefore, ˉf is in Q, but is it in T?
The Proof
Seeing why ˉf can’t be in T is pretty straightforward. Suppose ˉf is f2. Like we’ve seen so far, f2(2) can either be 0
or 1
. But if f2(2)=0, then ˉf(2)=1−f2(2)=1−0=1. So, we have:
f2(2)≠ˉf(2)
Whoops. Okay, so it wasn’t f2. That would be too easy. What about f421? If f421(421)=1, then ˉf(421)=1−f421(421)=1−1=0. So, we have:
f421(421)≠ˉf(421)
As it turns out, any computable function we pick out of T (and implicitly A) will disagree with ˉf at at least one output. And therefore, we have the amazing finding that:
A⊂Q
Conclusion
In other words, there are some things, like ˉf, 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 T. 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.