Making sense of Goedel's First Incompleteness Theorem

Question

In Stanford Encyclopedia of Philosophy they say that (for a formal system F) by the Diagonalization Lemma a sentence G can be constructed: $F \vdash G_F$ $\leftrightarrow$ $\lnot Prov(⌈G_F⌉)$. This sentence G basically says that F proves $G_F$ iff the Goedelnumber of $G_F$ is not provable.

If I assume G then I can totally follow them on why neither $G_F$ nor $\lnot G_F$ is not provable, but my problem is this: why do I have to assume G, what if I just assume ~G? Then the whole problem resolves and everything seems fine because ~G $ \equiv$ $(F \vdash G_F$ $\land$ $Prov(⌈G_F⌉))$ $\lor$ $ (\lnot Prov(⌈G_F⌉) \land F\nvdash G_F)$.

Answer 1

You misunderstood: $G$ is not the biconditional $(F \vdash G_F) \leftrightarrow (\lnot Prov(⌈G_F⌉))$. Rather, $G$ is the metalogical claim that the biconditional $G_F$ $\leftrightarrow$ $\lnot Prov(⌈G_F⌉)$ (which is a logical claim) can be proven in $F$. And that metalogical claim we write as $F \vdash G_F \leftrightarrow \lnot Prov(⌈G_F⌉)$ (think of it as $F \vdash (G_F \leftrightarrow \lnot Prov(⌈G_F⌉))$

Moreover, it is not claim $G$ that is what is typically referred to as the 'Godel sentence', but rather $G_F$. That is, Godel's proof shows that relative to any 'strong enough' (strong enough to prove elementary arithmetical truths basically), consistent, and recursive formal system $F$, there must be some sentence $G_F$ such that $F \vdash G_F$ $\leftrightarrow$ $\lnot Prov(⌈G_F⌉)$ is the case. When you now assume that $G_F$ is false, you get a problem, because then, given the truth of the biconditional (it's true since $F$ derives it), it would have to be true that $G_F$ is provable, and thus true, which contradicts the assumption that is was false. So, it must be true. And, given that same biconditional, not provable.

The truth of $G$ itself is not under discussion. Godel's proof that $G$ has to be the case.

Answer 2

The diagonal lemma isn't used to construct what you call $G$, but rather $G_F$. Really, we should ignore $G$ altogether and just focus on what's going on "inside $F$."

• EDIT: actually, it's even worse than that! The article uses $G$ ambiguously to refer to both the sentence $G_F\leftrightarrow Prov_F(\underline{\ulcorner G_F\urcorner})$ (note that the article also omits the numeralization here!) and the sequent $F\vdash G_F\leftrightarrow Prov_F(\underline{\ulcorner G_F\urcorner})$ (look at the first appearance of $(G)$). I'm normally a fan of SEP, but in my opinion this is a situation where this kind of minor sloppiness is a really bad idea.

---

To start with, let's state the diagonal lemma precisely. For $F$ an "appropriate" system the diagonal lemma says the following:

For every formula $\varphi$ there is some sentence $\theta$ such that $$F\vdash\theta\leftrightarrow\varphi(\underline{\ulcorner\theta\urcorner}).$$

Here "$\ulcorner\psi\urcorner$" is the Godel number of a sentence $\psi$ and "$\underline{n}$" is the numeral corresponding to $n\in\mathbb{N}$. So the diagonal lemma is really doing two things: given a formula $\varphi$, it produces a particular sentence and a particular $F$-proof.

This may seem rather mysterious until you read the proof of the diagonal lemma in detail to see how the desired sentence $\theta$ and $F$-proof of $\theta\leftrightarrow\varphi(\underline{\ulcorner\theta\urcorner})$ are constructed from a given $\varphi$. It's quite concrete, but tedious and often opaque at first glance.

In the incompleteness theorem, then, we apply the diagonal lemma with $\neg Prov$ as our $\varphi$. (Well, at first - we later use Rosser's trick to get a different choice of $\varphi$ that works even better.)

---

A couple quick comments:

• "Produces" is a good word to use above: the diagonal lemma is totally constructive.

• Meanwhile, the diagonal lemma doesn't tell us that $\theta$ literally is $\varphi(\underline{\ulcorner\theta\urcorner})$, but merely that $\theta$ and $\varphi(\underline{\ulcorner\theta\urcorner})$ are $F$-equivalent. That said, see here.