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

Question

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.

Answer 1

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.