# Why is the proof of Gödel's first incompleteness theorem no contradiction?

I consider the following version of Gödel's first incompleteness theorem:

Assume $F$ is a formalized system which contains Robinson arithmetic $Q$. Then a sentence $G_F$ of the language of $F$ can be mechanically constructed from $F$ such that:

- If $F$ is consistent, then $F$ $⊬$ $G_F$
- If $F$ is $1$-consistent, then $F$ $⊬$ $¬G_F$

In the proof we first use the Diagonalization Lemma and apply it to the negated provability predicate $¬Prov_F(x)$: this gives a sentence $G_F$ such that

(A) $F ⊢ G_F ↔ ¬Prov_F(⌈G_F⌉)$.

Where $⌈G_F⌉$ is the Gödel number of $G_F$. Thus, it can be shown, even inside $F$, that $G_F$ is true if and only if it is not provable in $F$.

It is not difficult to show that $G_F$ is neither provable nor disprovable in $F$, if $F$ only is $1$-consistent by assuming $F$ is provable, ... and so on and so forth.

But when we prove $G_F$ is unprovable didn't we also prove $G_F$, since A holds? That is, we have proved $G_F$ and at the same time we have shown we cannot prove $G_F$.

This seems contradictory to me, or am I missing something? I guess the answer must have to do with Tarski's undefinability of truth.

• I'm unfamiliar with your notation, but the key message is imo that although you may have proven $G_F$, you have done so outside the system. And if you were to formalize that proof, you would do so in a formal system which must exhibit some other incompleteness, even if it were powerful enough to prove $G_F$. – MvG Jun 21 '16 at 21:26

## 1 Answer

This is a great question, and highlights a common issue with Godel's theorem: where does the proof take place?

You're quite right that if the entire proof took place inside $F$, then this would be a contradiction. But it doesn't! It takes place in the slightly stronger theory $F+1Con(F)$ (actually, Rosser later improved this to $F+Con(F)$). That is:

• $F$ knows that, if $F$ is 1-consistent, then $G_F$ is true and not $F$-decidable.

• $F+1Con(F)$ knows that $G_F$ is true and not $F$-decidable.

• In particular, $G_F$ is $F+1Con(F)$-decidable, but not $F$-decidable.

• So there's no contradiction.

A couple comments:

• Rosser's improvement was the following. Instead of the Godel sentence $$\mbox{G_F="I am F-unprovable",}$$ Rosser used the sentence $$\mbox{R_F="For any F-proof of me, there is a shorter F-disproof of me."}$$ (Just like for $G_F$, the formulation of $R_F$ in the language of arithmetic uses Godel numbering and the fixed point theorem.) It's a good exercise to show that $R_F$ let's us bring the consistency assumption down to just $Con(F)$.

• Note that we can iterate the Godel (or Rosser) process! We can consider a sequence of stronger and stronger theories, starting with some $F$ and repeatedly adding the Godel (or Rosser) sentence. It turns out this leads to some deep ideas in computability theory; see e.g. https://mathoverflow.net/questions/12865/using-consistency-to-create-new-axioms-in-set-theory.

• The idea behind the linked post actually happened in the last century, caused by the Russell paradox (who shaves the barber etc). Russell tried to find a way around it, then some mathematicians found a contradiction in his new system, then a way was found around that, then they found another contradiction and so on. The saga was detailed in a history of mathematics book I redd. – user301988 Jun 21 '16 at 22:39
• Very good. That explains it to me. Still have to go through the second part though. – Zetaman Jun 22 '16 at 9:04