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.

  • 1
    $\begingroup$ 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$. $\endgroup$
    – MvG
    Jun 21, 2016 at 21:26

1 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.

  • 1
    $\begingroup$ 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. $\endgroup$
    – user301988
    Jun 21, 2016 at 22:39
  • $\begingroup$ Very good. That explains it to me. Still have to go through the second part though. $\endgroup$
    – Zetaman
    Jun 22, 2016 at 9:04

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .