The incompleteness theorems appear mysterious to many people, from sheer confusion of the statements themselves, to wrongfully applying the theorems to scenarios way out proportion, such as (dis)proving the existence of god. It doesn’t help that when actually *learning* about the theorems in a logic course, most details are usually admitted. This is probably not the case at all universities, of course, but I have now personally experienced two different approaches to Gödel’s theorems:

- Spend most of the time on the recursion theory prerequisites to the theorems, without actually covering the theorems themselves, save for the statements;
- Skip the recursion theory and only give an informal argument of the incompleteness theorems without really showing why we should care about recursiveness.

The reason for not giving a full account of the theorems is of course the perennial enemy of lecturers: time. What I’ll try to do in this post is still *not* to give a complete account of the proofs, but try to explain how it all fits together. Fill in the gaps that I’ve at least encountered during my studies, which can then hopefully help others stitch together whichever parts they might have learned throughout their studies. Here we go.

I’m going to focus on the first incompleteness theorem, since the second one is really a corollary to the first one. Let’s start with the statement itself.

First Incompleteness Theorem (Gödel ’31).Let be a language. Then any consistent recursive set of -sentences such that , is incomplete.

Let’s start off by examining the statement. We have to figure out what is, what we mean by *recursive* and what is. Firstly, is simply the language of arithmetic, where is the symbol for the successor function, and is the symbol for exponentiation. So far so good.

To define recursiveness we first define *recursive functions*. Before we do that, the intuitive idea behind any recursive set is that we (in principle) can sit down and write a computer program, which takes an object as input and after a finite amount of time will answer whether is in our set or not. Now, the simplest way to define what **recursive functions** are is probably that it’s the smallest set of functions containing the functions:

- Successor ;
- Addition ;
- Multiplication ;
- Exponentiation ;
- The characteristic functions and of equality = and less-than <;
- Constant functions for all ;
- Projections , given as ;

and furthermore closed under composition and *minimalisation*, where the latter means that if is recursive such that whenever there exists satisfying , then the function given as

is recursive as well. We can also talk about **recursive relations **, which is simply when the characteristic function of the relation is recursive.

But we’re not really talking about sets of natural numbers in the statement of the theorem; we’re talking about *sets of -sentences*. To fix this, we encode all symbols in our language , and all sentences of these symbols as numbers. This can be done in many different ways, and any such encoding is called a *Gödel encoding*. Writing for the encoded version of , we then say is recursive if is.

Now, why do we care about recursiveness in the incompleteness context? I’ll get to that, hang on. First, let’s clarify what is. It’s the following (weak) system of axioms in the language of arithmetic, from Enderton’s book:

- (S1) ;
- (S2) ;
- (L1) ;
- (L2) ;
- (L3) ;
- (A1) ;
- (A2) ;
- (M1) ;
- (M2) ;
- (E1) ;
- (E2) .

It’s a fair amount of axioms, but they should all be “intuitively true” when thinking about the standard interpretation of the symbols in . The specific choice of system is **not important**: all we need is a reasonably strong system which is *finite*.

Okay, so now we at least know what we’re working with. The next (tedious) part, which is the one I’ll skip here, is proving that basically everything in our formula-toolbox is recursive: the set of terms, set of formulas, set of variables, substitution and provability. This last one gives us a recursive relation , where expresses the fact that encodes a proof from of an -formula , and encodes .

Having happily skipped that part, the next part is explaining why we care about recursiveness. For a relation we say that an -formula **represents** in if, letting be the free variables of and letting ,

- If holds then , and
- If fails then .

Here is the -term with many ‘s. That represents can be seen as a syntactic strengthening of being definable over the standard model of arithmetic. Indeed, if was replaced by the theory of that model, then representability would coincide with definability. Now, here’s the reason why we care about recursiveness.

Lemma (aka why recursiveness is useful).Every relation is recursive iff it’s representable in .

Now we can move on to the (in my mind) fun bits of the argument.

There are (at least) two proofs of the first incompleteness theorem floating about. There’s Gödel’s original method, consisting of constructing an explicit sentence which witnesses the incompleteness of , i.e. that and , and the abstract method which only shows that such a sentence exists. The abstract method, which doesn’t construct an explicit witness to the incompleteness, does a detour through Tarski’s Undefinability Theorem and is quite slick, but I’ll stick with Gödel’s constructive approach here instead, to emphasise that we’re really just formalising the liar paradox.

The crucial lemma is then the following, from which the incompleteness theorem is a simple corollary. The lemma essentially says that we can construct self-referential sentences in our weak system .

Fixed-point lemma.Let be an -formula. Then there exists an -sentence such that.

**Proof. **Let be a variable and define a function as whenever for an -formula , and otherwise.

By the above-mentioned results, this function is recursive and hence also representable in , meaning that we get an -formula such that for any -formula we get that

,

just by definition of representability (where we identify with its graph). We may assume that and , so that we wind up with

for every . Define now and note that only has free. Our desired formula is then

.

Note here that says “if is the Gödel number of the sentence ‘ is true of itself’ then is true of “. But since also says that “ is true of itself”, what is really saying is that holds of ! Now, putting together (1) and (2) we get that

.

It remains to show that actually works, which is shown in the following technical claim.

Claim..

Proof of claim.:

- .
:

This finishes the proof of the fixed-point lemma. **QED**

Using the lemma, we can now prove the (first) incompleteness theorem.

**Proof of the first incompleteness theorem.** Recall that we have a recursive relation , where expresses the fact that encodes a proof from of an -formula , and encodes . This is then also representable in , so we get an -formula representing it in . Define then

,

intuitively meaning “ is provable”. More precisely, implies that , by definition of representability. The fixed-point lemma grants us an -sentence such that

,

i.e. says that “I am not provable from “. Now, if then by the above, but we also get that by (1), contradicting the consistency of .

Next, assuming we get that by (1). Using the consistency of we get an -model . By definition of it holds that for some . The soundness theorem then implies that and representability then yields that for some deduction of from . This means that , contradicting the consistency of again. **QED**

Aaaand that finishes this (quite long) post. Hope this is useful to some of you!