Formalizing proof of Godel sentence's non-provability?

Question

In the question

What does it mean for something to be true but not provable in peano arithmetic?

Henning Makholm states, "...he [Godel] gave a (formalizable, with a few additional technical assumptions) proof that a particular sentence was neither "provable in PA" nor "disprovable in PA", and a convincing (but not strictly formalizable) argument that this sentence is true about the actual natural numbers."

Why is it not formalizable? Shouldn't it be formalizable in some system outside of PA, like ZFC, for example?

Answer 1

Well, take formal theory $PAT$ which you get by adding a predicate $T$ to Peano Arithmetic, adding the obvious axioms to make $T$ a compositional truth-predicate, and allowing the truth predicate to appear in instances of the induction schema. The $PAT$ proves $Con(PA)$ and hence $G$ the Gödel sentence for Peano Arithmetic, and hence $T(G)$. So we can certainly formalize one natural line of argument for the truth of $G$, and we don't need anything as fancy as ZFC to do the trick. (But I suppose it is open to question how close this line comes to reflecting Gödel's informal remarks, and anyway, the availability of $PAT$ doesn't affect the point Henning Makholm was after, as Carl Mummert notes.)

Answer 2

I believe that Henning Makholm only meant the argument is not formalizable in the object theory being studied.

You are correct that ZFC will prove that the Gödel sentence for PA is true. This can be interpreted two ways:

• ZFC directly proves the sentence $G_{\text{PA}}$ when this is recast as a formula of ZFC.

• ZFC can talk directly about the standard model of PA. ZFC proves that the standard model of PA satisfies the Gödel sentence. Note that each model of ZFC will contain its own standard model of PA, so what this proof means is that each model of ZFC believes that its own standard model of PA satisfies $G_{\text{PA}}$.

But ZFC cannot prove that the Gödel sentence for ZFC is true, in either of these senses.

• ZFC does not prove $G_{\text{ZFC}}$, by the incompleteness theorem.

• There are some models of ZFC that do not contain any model of ZFC at all. So, unlike the situation with PA, there is no way within ZFC to pick some standard model of ZFC to work with.

Nevertheless, we can use Gödel's original argument to see that, if ZFC is consistent, then $G_{\text{ZFC}}$ is true.

This is a deeper sense in which Gödel's argument is not formalizable: because the argument depends on the object theory being studied (e.g. PA or ZFC), we can't just formalize it "once and for all", but rather we have to re-formalize it for each object theory that we study.