Comment by dwohnitmok
1 month 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."
1 month 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."
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)
> 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.
Yes I agree.
All of this spun from the original comment on Math Stack Exchange, which got distilled down to this (https://news.ycombinator.com/item?id=44277936).
> > If PA proves "PA proves X" then PA can prove X.
> Not true.
As for the following
> The truth predicate for PA is undefinable in PA, I agree, but you can represent the reflection principle as an axiom schema
got it, thank you!
The main thing I'm wondering is whether this is provable in PA: "forall x, IsSentence(x) -> Provable(g(Provable(x))) -> Provable(x)", which I think it is, but haven't had the opportunity to write enough of the formal details to be 100% confident.
I suspect you are right too about that last one. It's difficult to do this stuff formally though, I've made one attempt and failed so far!