I came to a good summary of Godel's incompleteness theorem proof (http://www.jamieyorkpress.com/wp-content/uploads/2012/04/G%C3%B6dels-proof-summary.pdf) but I'm confused on one step which leads to the conclusion that "PM is consistent -> PM's consistency is not PM-provable." Would appreciate someone can enlighten me. Because I haven't finished reading the original paper, I based my understanding on this summary. I could be confused because of this summary is wrong.
As the summary says, assuming PM is consistent, then the formula G "G is not PM-provable" is not PM-provable. Then meta-mathematically, it's clear that G is true, therefore PM is incomplete.
This conclusion: "PM is consistent -> PM is incomplete" (*) is then used as a theorem in a series of steps that leads to a contradiction which proves that "PM is consistent -> PM's consistency is not PM-provable". Basically:
"PM is consistent and such consistency is PM-provable" ->
(using (*) here. This is the step I'm confused about)
"PM's incompleteness is PM-provable" ->
"G is PM-provable" -> contradiction.
My confusion is that (* ) is clearly the conclusion of a meta-mathematical proof. Can we use that as part of a PM-proof? Because the above proof uses (*), I wonder we therefore can't say G is PM-provable but just G is meta-mathematically-provable, which doesn't lead to any contradiction with the conclusion that "G is not PM-provable"?
Hope I've explained my confusion clearly. Would appreciate any kind of replies. Thanks!
This is a very good question! Many treatments of Goedel's theorem gloss over exactly where the relevant statements are being proved.
Here's what's going on:
Actually, this is not quite due to Goedel, but rather Rosser's improvement of Goedel's argument; Goedel original showed a somewhat weaker fact.
However, note the constant hypothesis "If PA is consistent." The unqualified claim $$\mbox{PA is incomplete}$$ is not provable in PA alone; rather a stronger theory, capable of proving PA's consistency, is needed. Metamathematically, this corresponds to our accepting that PA is consistent. (Goedel's original argument had even more metamathematical baggage: it required that we accept that PA is true, or at least correct about a certain class of propositions. Rosser's improvement was to reduce the assumption needed to exactly "PA is consistent.")