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?