Comment by dwohnitmok
1 month 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.
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!