Comment by bubblyworld 2 days ago
The standard model is a model of PA only if PA is consistent, which it cannot prove unless it is inconsistent (Godel's theorem). So your proposed proof doesn't work in PA itself, which is the point of that comment, I believe.
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.
Crucially, I am not claiming that "if PA proves X, then X holds" for arbitrary X, which again I'm not even sure how to state in PA. My statement is simply "If PA proves 'PA proves X' then PA can prove X."
I believe my proof actually works in systems even weaker than PA (but the metatheory of how exactly to do the encoding in a first-order theory is a bit of a headache for me at the moment).
In particular I'm not relying on the consistency of PA. If PA is inconsistent, "If PA proves 'PA proves X' then PA can prove X" also holds (trivially), because then PA can prove anything.