Comment by bubblyworld
Comment by bubblyworld 2 days ago
Hmm, earlier you wrote:
> This is because the key observation is not that there are nonstandard models, but rather that the standard natural numbers model PA.
This fact (that the standard natural numbers model PA) implies that PA is consistent, so your argument is implicitly assuming that from the outset, right? If PA is consistent then this is not something that PA can prove, so I don't see how you could run your proof in PA itself. And certainly not how you could do it in a weaker theory. Logic is subtle though... so what am I missing?
As far as I know what you're describing (namely that "Provable(X)" implies "X") is called the uniform reflection principle and added to PA is much stronger than PA alone.
I'm not familiar with the uniform reflection principle. What does the actual first-order statement look like? Because the simplest version I can think of how to formalize this in PA, namely that PA proves "Provable(X) -> True(X)" (because you need an encoding if you're working in PA, "Provable(X) -> X" is simply not something you can write in the language of PA), is not possible to write in PA (so would be a category error) because of Tarski's undefinability of truth result.
> so your argument is implicitly assuming that from the outset, right?
No. My argument implicitly has a fork at the beginning.
If PA is consistent, run the usual standard natural number argument I made.
If PA is not consistent, then PA can prove everything.
Hence the statement "If PA proves 'PA proves X' then PA can prove X." goes through either way. It does not depend on the consistency of PA.