Comment by bubblyworld

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)