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?

enter image description here enter image description here

  • For a good overview, see B.Buldt, The Scope of Gödel’s First Incompleteness Theorem (2014). Dec 24 '19 at 16:53
  • @MauroALLEGRANZA Thank you, I have been reading Peter Smith's An Introduction to Gödel's Theorems so I roughly know how Godel proves the Incompleteness; but I am afraid I don't see how Godel's proof comes into play here. Isn't what Priest is doing here independent of Godel's proof? It just seems like he is applying Modus Ponens to (1) somehow to get the conclusion Dec 24 '19 at 17:15
  • What you quoted is very misleading or meaningless. There is no such thing as "P's meta-language", unless it simply means "P+Con(P)". The author fails to state this clearly, and so is either ignorant or trying to cover it up. All this has nothing to do with "semantics". Any reasonable foundational system for mathematics can formulate and reason about its own semantics. What it cannot do is to prove itself consistent. Neither can so-called 'naive semantic reasoning' get anywhere; as I said the extra assumption is "Con(P)", not any 'semantic' thing.
    – user21820
    Dec 25 '19 at 17:13
  • Since you said you have gone through Peter Smith's book, I assumed you fully understood all the technical details, in which case it should be trivial for you to verify what I said. If you are unsure about the exact details of Godel coding, you can take a look at a self-contained computability-based proof that is more general and may help you to grasp what exactly are the critical conditions for the incompleteness phenomenon to arise.
    – user21820
    Dec 25 '19 at 17:27
  • @user21820 'Any reasonable foundational system for mathematics can formulate and reason about its own semantics.' I could very well be wrong, but doesn't a theory need a truth/satisfaction predicate to be able to formulate its own semantics? As far as I understand, PA does not have that. Dec 30 '19 at 20:36

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].

  • Oh I see now; I thought Priest was doing something different from Godel but in reality he was just sketching out Godel's proof. Thank you so much that is very clear! Dec 25 '19 at 11:31

(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.

  • Ah ok, so (1) is an instance of Tarski's T-schema? But how do we get ¬∃x Prov(xg)? Priest seems to have done a Modus Ponens on the T-schema to get it, but I don't see how he can Dec 24 '19 at 16:42
  • The sentence g is gotten by diagonalization, so that it says "there does not exist a proof of g." Dec 24 '19 at 16:51

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.