Comment by bubblyworld
1 month 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.
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."
Right, this is a claim I agree with, of course. I interpreted your earlier comments as the former, which I'm sure you agree is not provable in PA. There's a certain unavoidable ambiguity when talking about these things informally!
The truth predicate for PA is undefinable in PA, I agree, but you can represent the reflection principle as an axiom schema: for each formula A(x) the axiom "forall x. Provable([A(x)]) -> A(x)".
(which has the intended meaning at the meta-level, "if A(x) is provable in PA then it is true")
This is consistent with PA but much stronger. In particular it proves Goodstein's theorem, and hence consistency of PA too via cut elimination.
(or flavours of that, there are many reflection principles, but the basic idea is not to represent it as a single formula - quantify at the meta level, if you will)
2 replies →