Comment by btilly

No, it is not different from the earlier claim. If you think that it is, then you were misreading me.

My earlier claim is that for each n, "PA proves that it proves that G(n) terminates". But in logic there is an important distinction to be made between "PA proves" and "PA proves that it proves". From the second, you cannot conclude the first. You must actually present the proof, and then verify it.

And the reason is this. It is true that, for all standard n, "PA proves that it proves" implies that "PA proves". But for nonstandard n it does not. Since PA cannot itself distinguish standard n from nonstandard n, PA cannot follow that implication to a proof.

(All of this is based on long conversations with my logic professor back in grad school. To the extent that I get it right, https://faculty-directory.dartmouth.edu/marcia-j-groszek deserves the credit. To the extent that I get it wrong, I deserve the blame.)