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 '16 at 21:26

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.