We will prove Gödel’s first incompleteness theorem by using some terms of Computational Theory and the fact that the halting problem is uncomputable.
First of all, some terminology.
We assume that every mathematical statement s can be represented as a bitstring. (Just choose an encoding — for instance ASCII and then convert it to bit representation). Therefore, every mathematical statement s belongs to the set .
Moreover, we are going to need a definition for what a program is. You can choose your favourite one, as long as we agree that it is a finite sequence of statements, where the statements are simple enough depending on you computational model (you don’t cheat here).
Now, let’s suppose that for each program A and bitstring x (its input), we have the statement “A(x) halts” (A(x) is going to finish its execution at some point). Let’s pick a convenient notation for this statement . We require and (they are mathematical statements). We also assume that every proof p can be represented as bitstring.
We have included explicitly the statements in S because they are going to help us in the proof by contradiction. We will create a machine that decides the halting problem if Gödel first incompleteness Theorem is not true.
Now, we have to agree on some function (our set of axioms) that determines whether a given proof is correct (proves a mathematical statement). We won’t put any limitation on this function. You can pick whatever you like. What we will see is that, no matter what you pick, there are some statements that can not be proven as long as we are consistent. More formally, let V be the function of your choice such that .
Now, some more assumptions which seem natural. First of all, we assume that all the proofs can be verified mechanically. That means, there is a Turing program V(< s, p >) which decides whether the proof is correct or not. This implies that the program V always halts.
One last thing before the actual proof. We say that statement s can be V-proven in case V(< s, p >) = 1 for some . Setting aside the notation, what we said is that s can be proven if there is a proof for that. Wow! Now, just to be clear, we say that V is inconsistent if we can prove both p and . Otherwise, it is consistent.
Like the annoying friends who, when you are going to the cinema, spoil to you how this ends, here comes the Gödel first incompleteness Theorem. It states, in summary, what the following proof is going to demonstrate.
Gödel first incompleteness Theorem
Let V be a consistent verification function. Suppose that for any Turing program A and any input x such that A(x) halts, can be V-proven. Then, there exists a Turing program A and an input x such that A(x) runs forever, and yet cannot be V-proven.
We recall that the halting problem can not be decided. Let’s assume that, in contrast to the theorem, if a program A never halts then can be proven. Then, we will see that we can give a program H which decides the halting problem, which can not be true.
Our program H takes as input the description of program A and its input x encoded as tuple. Then, H simulates A(x). In parallel, it also simulates V(< >), where it enumerates over all possible proofs p for . Let’s recall at this point that is the statement that A(x) does not halt.
Let’s see what can happen. If the simulation of A(x) ends at some point, H outputs 1. Otherwise, it will find eventually a proof for and it will output 0 (remember our assumption at the very beginning of this proof that if A(x) never halts, we will find a proof for that.).
Maybe, we already see intuitively that program H is able to decide whether A halts or not which can not be true. Let’s see that in more detail.
- A(x) halts. Then can be V-proven as we already saw. Since V is consistent, we can not also V-prove . Therefore, H(<τ(Α), x>) outputs 1.
- A(x) does not halt. Then, we will find eventually the proof p for . Therefore, H(<τ(Α), x>) outputs 0.
All in all, program H is able to decide whether A halts or not in the particular input x. Nevertheless, we know that the halting problem is not decidable. Therefore, there can not be such a program H which concludes our proof.
I was able to write this proof due to the course of Complexity Theory at ETH and the excellent notes that they provide us.
For an alternative, descriptive proof, you can check wikipedia.