Comment by dwohnitmok

Comment by dwohnitmok 18 hours ago

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.

dwohnitmok 11 hours ago

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."

Reply View 1 reply

bubblyworld 6 hours ago

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)

Reply View | 0 replies