How would I show that PA proves the godel sentence for PA implies Con(PA)

Question

Started off with definitions: godel sentence for PA is the sentence in PA that cannot be proved nor disproved Con(PA) formalizes PA is consistent

We know godels first incompleteness theorem is essentially showing if the theory is consistent the there's a godel sentence. So we need to show that PA proves the opposite.

I'd start off supposing there's a godel sentence for PA but I am not really sure where to go from there.

Answer 1

There seems to be a bit of confusion here:

"the sentence in PA that cannot be proved nor disproved"

is not a definition - there are many sentences which PA can neither prove nor disprove. The Godel sentence for PA is a very particular example, but there are lots of others.

• Indeed one of the consequences of (the general version of) Godel's theorem is that there is no algorithm for determining when a sentence is undecidable in PA. Put another way, there will always be surprising examples of independent sentences; the "strengthened finite Ramsey theorem" is a natural example, and the MRDP theorem tells us that some (very unnatural, granted) Diophantine equations have no solutions but are not PA-provably-unsolvable.

Roughly speaking, $G_{PA}$ says "This sentence is not PA-provable." Somewhat more precisely, the key fact about $G_{PA}$ is $$(*)\quad PA\vdash [G_{PA}\leftrightarrow\neg Prov_{PA}(\ulcorner G_{PA}\urcorner)]$$ (where "$\ulcorner\cdot\urcorner$" is the usual Godel coding function and "$Prov$" is the arithmetized provability predicate). That is, PA proves "$G_{PA}$ is true iff PA doesn't prove $G_{PA}$."

---

Now on to the problem. The key observation is that, while there are many facts about PA-provability which PA can't prove (e.g. PA doesn't prove $Prov_{PA}(\ulcorner\varphi\urcorner)\implies\varphi$ except when PA proves $\varphi$ already), it can prove "obvious" facts: in particular, whenever PA proves a statement, it proves that it proves that statement, and moreover it proves that. (Hehe).

So we argue in PA as follows. PA proves that inconsistent theories prove everything; that is, we have $$(**)\quad PA\vdash(\neg Con(PA)\iff \forall x(Prov_{PA}(x))).$$ Now - reasoning in PA - if $G_{PA}$ is true then $\forall x(Prov_{PA}(x)))$ is false (take $x=\ulcorner G_{PA}\urcorner$ and apply $(*)$ above), so by contrapositive we have $$PA\vdash G_{PA}\rightarrow Con(PA).$$