True but unprovable?

Question

I would like to ask a question about Gödel's Incompleteness Theorems which I've had in the back of my head for some time. Since I'm a student working in a completely different area of maths (my usual pastime is cutting and pasting manifolds), my understanding of these results is nontechnical (I first learned about them before I started studying maths at university, by reading Nagel and Newman's excellent book).

I realize there are other questions on this topic, but I'd like to be a bit more specific in my question, and I wasn't able to google up anything that addressed what I'm about to ask.

As I understand it, the First Incompleteness Theorem is proven by producing a sentence, $G$ (which in English reads: "This sentence is not provable in the system."), that is neither provable nor refutable in the system in question. Nevertheless, $G$ is true, which means it satisfies the inductive definition of truth (right?). Here's what I don't understand:

1. Why does the sentence $G$ satisfy the inductive definition of truth? Is this because it is the negation of a false statement? If so, why is $\neg G$ false? Is this because it causes a contradiction, and sentences that lead to a contradiction in the system are false by definition?

2. Why doesn't the fact that $G$ is true (i.e. the list of steps reducing the truth of $G$ to the truth to atomic sentences (axioms?)) constitute a proof of $G$?

3. By Gödel's Completeness Theorem, there are formal systems in which $G$ is false, as argued here. How can this not cause a contradiction ($G$ can't both be provable and not be!). [What makes these systems different from those in which $G$ is true, and why is it often stated that $G$ is true, when in fact there are cases in which it isn't? Edit: answered here]

I hope I have managed to make myself clear. Thanks for any clarification!

Answer 1

About 1., Gödel's First Incompleteness Theorem is a ingenious exercise of "coding" formal properties and relations regarding a theory $F$ with "a certain amount" of arithmetic inside $F$ itself.

This exercise ends with the definition of the so-called provability predicate $Prov_F(x)$ which holds of $a$ iff there is a proof in $F$ of the formula $A$ with "code" $a$.

To complete the proof, [it is used] the negated provability predicate $¬Prov_F(x)$: this gives a sentence $G_F$ such that

$⊢_F G_F \leftrightarrow ¬Prov_F(\ulcorner G_F \urcorner)$ [where $\ulcorner x \urcorner$ is the "code" of formula $x$].

Thus, it can be shown, even inside $F$, that $G_F$ is true if and only if it is not provable in $F$.

Thus, "reading" the above proof, we can "know of" the truth of $G_F$ (provided that $F$ is consistent) simply because $G_F$ is not provable in $F$ and $G_F$ is equivalent to the formula $¬Prov_F(\ulcorner G_F \urcorner)$.

---

About 2. :

Why doesn't the fact that $G$ is true constitute a proof of $G$ ?

Because a proof in $F$ of $G_F$ is a precise formal objcet and G's Incompleteness Th shows that such a proof in $F$ cannot exists.

Thus, the conclusion of G's Incompleteness Th is twofold :

• there is a formula $G_F$ of $F$ which is "intuitively" true but not provable in $F$ [not "absolutely" un-provable]

• the system $F$ is unable to prove all true sentences expressible in it.

---

For 3. :

By Gödel's Completeness Theorem, there are formal systems in which G is false. How can this not cause a contradiction ?

NO; by G's Completeness Th there are models of $F$ in which $G_F$ is false.

G's Completeness Th, prove that a formula provable in a theory $T$ must be true in all models of $T$.

Thus assuming that $\mathbb N$ is a model of our theory $F$ containing "a certain amount" of arithmetic, we have that all theorems of $F$ (i.e. formulae provable from $F$'s axioms) must be true in all models of $F$.

But $G_F$ is not provable from $F$'s axioms; thus, it must be not true in some model of $F$.

The proof of G's Incompleteness Th give us the insight that $G_F$ is true in $\mathbb N$; thus, it must be false in some model of $F$ different from $\mathbb N$, i.e. in some non-standard model of arithmetic.