How to show (in a hand waving manner) that the Godel sentence is true

Question

I have been reading Graham Priest's The Logic of Paradox, and there is a section where he tried to show that our informal proof argument (in Priest's terminology, naive proof procedure) is more powerful in terms of proving power than our formal proof systems, by showing that the Godel sentence can be shown to be true if we go through the formal theory's meta-language. (Attached below)

I think I understand how he is proceeding from (1) all the way to (4). What I don't understand is what is his assumption/beginning of the argument, and how he is getting his conclusion?

If we take (1) to be true, then indeed from there we seem to be able to show that the Godel sentence is true. But where is (1) coming from?

(1) seems to be saying that IF there is a proof of the Godel sentence, then it (as denoted by its Godel code) is true; which I suppose is a fair point. (But is that already enough to warrant this conditional?) Then (2) to (4) seem to be equivalences of the conclusion, these are also relatively straight forward.

But surely until we actually have a code for the proof of the Godel sentence (which would then satisfies the antecedent and thus allows us to isolate the conclusion, ie. ¬∃x Prov(xg)), what we have remains a conditional. So I am not entirely sure how he has seemingly applied Modus Ponens to get ¬∃x Prov(xg) at the end?

---

Answer 1

Gödel’s Incompleteness Theorem is a result about formal systems.

Its proof requires certain assumptions about the properties of specific formal system F: basically, about its "expressive capabilities".

In a sense that can be specified rigorously, system F must have the capabilities to manufacture the provability predicate for F, i.e. a suitable formula PrF(x) such that :

F ⊢ A iff PrF("A") is a true sentence about the natural numbers,

where "A" is the Gödel-number for formula A.

The second key feature of system F is the so-called Diagonalization Lemma that can be applied to formula ¬PrF(x), to get :

F ⊢ G ↔ ¬ PrF("G") [here PrF("G") is the same as ∃x Prov(x,"G") of Priest].

The third key assumption is consistency of F; but G's proof can be simplified assuming the slightly stronger condition of soundness.

Now for the main result: assume that F proves G, i.e. assume F ⊢ G.

Due to the property of the provability predicate, the assumption about the provability of G amounts to the fact that sentence PrF("G") is true.

Using the diagonal equivalence, we have that G is false.

Then by the assumption that F is sound (it proves only true sentences about the natural numbers), it follows that F ⊬ G, which contradicts our assumption that F proves G.

So by propositional logic:

(i) F ⊬ G.

Thus, by the property of the provability predicate, we have that ¬ PrF("G") is true.

So by the diagonal equivalence:

(ii) G is true.

Then ¬ G is false and thus, by soundness of F:

(iii) F ⊬ ¬G.

In conclusion:

if F is sound, then F ⊬ G, G is true, and F ⊬ ¬G.

---

Having said that, what is Priest's handwaving argument ?

The starting point is the "purely syntactical" proof that G is not provable in F, i.e. F ⊬ G [this is result (i) above].

By the property of provability predicate:

F ⊢ A iff PrF("A") is a true sentence about the natural numbers,

we have that ¬ PrF("A") is a true sentence, i.e. ¬ ∃x Prov(x,"G") is a true sentence [this is result (ii) above].

Answer 2

(1) is a special case of the general principle that if you accept a statement, then you accept that the statement is true. If you believe snow is white, then you believe "Snow is white" is true. It remains handwavy until you give a precise explanation of what you mean by "X is true." And that turns out to be a tricky business.