Gödel’s First Incompleteness Theorem for Programmers

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 S$S$ within which a “certain amount of elementary arithmetic” can be carried out is incomplete; i.e., there are statements of the language of S$S$ which can neither be proved nor disproved in S$S$.

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 F$F$ as a function that takes a positive integer and returns either 0 or 1. Here’s an example of such an F$F$:

isOdd(x)={0x is even1x is odd$$isOdd\left(x\right)=\{\begin{array}{cc}0& x\text{is even}\\ 1& x\text{is odd}\end{array}$$

So, we see that isOdd(2)=0$isOdd\left(2\right)=0$ or that isOdd(38943981)=1$isOdd\left(38943981\right)=1$. We can define F$F$ however we want — as long as the output will either be a 0 or a 1. Let Q$Q$ be the set of all such functions F$F$.

We say that F$F$ is computable if there exists a computer program (or proof) P$P$ that takes as input x$x$ and returns F(x)$F\left(x\right)$. It goes without saying that P$P$ must complete within finite time and must be correct. So let’s look at some code. Is isOdd(x)$isOdd\left(x\right)$ computable?

function isOdd(x) {
  return (x % 2);
}

Looks like it! This program will always return 0 when x$x$ is even and 1 when x$x$ is odd. What about a more complicated example:

isPrime(x)={0x is not prime1x is prime$$isPrime\left(x\right)=\{\begin{array}{cc}0& x\text{is not prime}\\ 1& x\text{is prime}\end{array}$$

Is isPrime$isPrime$ 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 A$A$ be the set of all computable functions in Q$Q$. We just found out (the hard way) that isOdd$isOdd$ and isPrime$isPrime$ are in A$A$ — that is, they are computable.

But here’s the big question: are all functions in Q$Q$ computable? Or, equivalently:

A?=Q$$A\stackrel{?}{=}Q$$

If A=Q$A=Q$, then Gödel was wrong, so we need to figure out a clever way to show that A⊂Q$A\subset Q$. In other words, we need to show that there are some functions that take positive integers x$x$ 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 F$F$ 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 A$A$: we now have a program that goes with every single computable function. Let’s put them in a big table called T$T$. 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	…
f1$f_1$	f1(1)$f_1\left(1\right)$	f1(2)$f_1\left(2\right)$	f1(3)$f_1\left(3\right)$	f1(4)$f_1\left(4\right)$	f1(5)$f_1\left(5\right)$	f1(6)$f_1\left(6\right)$	f1(7)$f_1\left(7\right)$	…	f1(n)$f_1\left(n\right)$	…
f2$f_2$	f2(1)$f_2\left(1\right)$	f2(2)$f_2\left(2\right)$	f2(3)$f_2\left(3\right)$	f2(4)$f_2\left(4\right)$	f2(5)$f_2\left(5\right)$	f2(6)$f_2\left(6\right)$	f2(7)$f_2\left(7\right)$	…	f2(n)$f_2\left(n\right)$	…
…
fo$f_o$	1	0	1	0	1	0	1	…	fo(n)$f_o\left(n\right)$	…
…
fp$f_p$	0	1	1	0	1	0	1	…	fp(n)$f_p\left(n\right)$	…
…
fi$f_i$	fi(1)$f_i\left(1\right)$	fi(2)$f_i\left(2\right)$	fi(3)$f_i\left(3\right)$	fi(4)$f_i\left(4\right)$	fi(5)$f_i\left(5\right)$	fi(6)$f_i\left(6\right)$	fi(7)$f_i\left(7\right)$	…	fi(n)$f_i\left(n\right)$	…
…

You’ll notice that isOdd$isOdd$ and isPrime$isPrime$ 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)$$\overline{f}\left(i\right)=1-f_i\left(i\right)$$

Where fi$f_i$ is the i$i$th function in table T$T$. First, let’s make sure we’re convinced that ˉf$\overline{f}$ is well-formed. The input i$i$ is an integer. fi(i)$f_i\left(i\right)$ will return either a 0 or a 1, given that fi$f_i$ has a row populated in T$T$. And finally, 1–0=1$1–0=1$ or 1–1=0$1–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.