Oh. It looks like I was confused about what Gödel’s first incompleteness theorem really says.
What the theorem does not say:
Let PA* be a formal system containing the Peano axioms and maybe some other stuff. Let G be a sentence provably equivalent to “G cannot be proved in PA*”. Then if PA* is consistent, it can’t prove G and it can’t prove Not G either.
Why doesn’t the theorem say that? Because we can define a system PA^ consisting of PA and an extra axiom asserting the inconsistency of PA. PA^ is consistent in the sense that you can’t derive a contradiction from it (though note that it’s not sound, so don’t trust any result that PA^ “proves”).
But PA^ can prove its version of Not G. PA^ proves that PA^ can prove anything; hence PA^ proves that PA^ can prove G; hence PA^ proves Not G.
So why did I feel (possibly unfairly) that this post promoted my original confusion? It says this:
Peano arithmetic cannot prove G without being inconsistent; but this is precisely what G is saying
G doesn’t say that “PA cannot prove G without being inconsistent”. G says that “PA cannot prove G”. From the point of view of PA, those are not equivalent statements. So the sort of reasoning used in the article will work for PA but not for PA^ - we need to know something about the soundness of the system we are working in, not merely its consistency.
Oh. It looks like I was confused about what Gödel’s first incompleteness theorem really says.
What the theorem does not say:
Why doesn’t the theorem say that? Because we can define a system PA^ consisting of PA and an extra axiom asserting the inconsistency of PA. PA^ is consistent in the sense that you can’t derive a contradiction from it (though note that it’s not sound, so don’t trust any result that PA^ “proves”).
But PA^ can prove its version of Not G. PA^ proves that PA^ can prove anything; hence PA^ proves that PA^ can prove G; hence PA^ proves Not G.
So why did I feel (possibly unfairly) that this post promoted my original confusion? It says this:
G doesn’t say that “PA cannot prove G without being inconsistent”. G says that “PA cannot prove G”. From the point of view of PA, those are not equivalent statements. So the sort of reasoning used in the article will work for PA but not for PA^ - we need to know something about the soundness of the system we are working in, not merely its consistency.