9. Gödel’s incompleteness theorem

This is a famous theorem by the German logician Gödel about logical systems which sometimes creates a lot of confusion on social media: some view it as a proof that we can’t understand the universe or for the existence of god. It says nothing of the sort but it is a very important theorem about logical systems like Lean , which we have been using in this course hence it seems a good idea to disperse the speculation and tell you what it says and what is the idea of its proof (without going into details).

_images/goedel.jpeg

Kurt Gödel (1906 - 1978)

When using Lean we have already seen the symbol ⊢ (pronounced turnstyle) like in:

P : Prop,
h : P
⊢ P

here Γ ⊢ P means that the proposition P is provable from the assumptions Γ. We write ⊢ P to indicate that P is provable without assumptions. Now we may ask wether for any proposition P we can prove it or its negation, that is we can prove ⊢ P or prove ⊢ ¬ P. Note that this is not the same as excluded middle which just says that for any proposition we can prove ⊢ P ∨ ¬ P. And indeed there are famous open questions like wether we can prove P=NP and nobody knows wether we can prove ⊢ P=NP or ⊢ ¬ (P=NP) and we cannot even be sure that we can prove either in Lean.

The German Mathematician Hilbert was aware of this issue and he formulated a goal: to find a logical system that is complete which means for any mathematical proposition we can either prove it or its negation. Clearly, if some system is incomplete, ie. we are unable to prove a proposition we believe to be true then we just need to add some axioms to avoid this problem. After adding enough axioms we should reach completeness.

_images/hilbert.jpg

David Hilbert (1862 - 1943)

However Gödel showed this is impossible if we just make some modest assumptions about the system we use. In the moment we will just assume we are using Lean but indeed Gödel just used predicate logic and Peano Arithmetic which is much less powerful then Lean. However, Gödel’s proof also applies to Lean as we will see.

The key insight to Gödel’s theorem is that a system is incomplete if it can talk about itself. In Lean we can define a type Formula : Type representing formulas as trees as we have seen. For any proposition P which we can form in Lean we have a translation ⌈ P ⌉ : Formula which is the internal representation of the proposition. We can also define a predicate:

Prove : Formula → Prop

which says that a formula is provable and we have that:

⊢ P ↔ ⊢ Prove(⌈ P ⌉)

I won’t go into the details of defining Prove here but just hint that we need to define an inductively defined relation like Perm and that we do need to define it for any sequence of assumptions, that is we define ProveAss : Assumptions →  Formula → Prop.

The translation also works for predicates: Given P : Formula → Prop we obtain ⌈ P ⌉ : Formula such that:

⊢ P q ↔ ⊢ Prove2(⌈ P ⌉, q)

where Prove2 :  Formula →  Formula → Prop.

Now I can define a weird predicate:

def Weird : Formula → Prop
| p := ¬ Prove2(p ,  p)

That is Weird p says that p is the code of a predicate which is not provable if applied to its own code. What happens if we apply Weird to its own code?:

⊢ Weird ⌈ Weird ⌉
=  ⊢  ¬ Prove2(⌈Weird⌉ , ⌈Weird⌉)
↔  ⊢  Prove2(¬  ⌈Weird⌉ , ⌈Weird⌉)
↔ ⊢ ¬ (Weird ⌈Weird⌉)

Let’s write G = Weird ⌈ Weird ⌉ we can prove G iff we can prove its negation! This is not a contradiction but it shows that we can neither prove G nor ¬ G if we assume that our system is consistent (that is ⊢ False):

¬ ⊢ G
¬ ⊢ ¬G

Because if we can prove ⊢ G then we can also prove ⊢ ¬G and hence we prove ⊢ False which would contradict consistency. The reasoning for ⊢ ¬G is symmetric.

G is called a Gödel sentence. This shows that a system which can talk about itself cannot be complete because we can always construct G - and it doesn’t matter how many axioms we add. This was the end for Hilbert’s programme.

Now I have sketched the incompleteness proof for Lean but Gödel formulated it for a much simpler system: Peano Arithmetic (PA), which is predicate logic with equality and the axioms for natural numbers (e.g. 0 ≠ succ n , inj_succ and induction for natural numbers). We also need to assume two functions add and mult (as we have defined them). Gödel showed that formulas can be encoded as natural numbers (which is no surprise for computer scientists since numbers are just sequences of bits) and that Prove can be encoded as a predicate over natural numbers. Actually he didn’t even needed to use induction to derive incompleteness. And any system which extends thus very primitive system (called Robinson Arithmetic) is incomplete.

However, there are complete logical systems. If we leave out multiplication we arrive at a system that is called Pressburger Arithmetic and this is complete and actually decidable (which is a consequence). Another simpler example is the logic of booleans (indeed we have seen how to eliminate the quantifiers).

What I have discussed here is Gödel’s first incompleteness theorem. The 2nd incompleteness theorem is more or less a corollary: once we have Prove the system can state its own consistency ¬ Prove(False) and the 2nd incompleteness theorem states that this is a Gödel sentence, i.e. a system cannot prove its own consistency.

Let me sketch the idea we say CONS = ¬ Prove(False). Let’s assume ⊢ CONS which entails Prove(CONS). Now internalizing Prove we get:

⊢ Prove(Prove(P)) ↔ Prove(P)

and now doing Goedel’s proof internally we obtain:

⊢ prove(CONS → ¬(Prove(G)))

but since we assume Prove(CONS) we can show:

⊢ Prove(¬(Prove(G)))
↔ ⊢ Prove(Prove(¬ G))
→ ⊢ Prove(¬ G)
→ ⊢ ¬ G

Which contradicts that G is a Gödel sentence. Hence our assumption ⊢ CONS is false.

However, to derive Goedel’s proof internally we need to use induction. In the context of arithmetic we only need a limited form of induction which is induction over decidable predicates and this system is called primitive recursive arithmetic or PRA.