Comment by ComplexSystems
Comment by ComplexSystems 2 days ago
That is very different though. You are now saying that for all n, PA proves that it has a proof the Goodstein sequence terminates for that n. But that is very different from the earlier claim:
"And, therefore, there must be a distinction to be made between "PA proves" and "PA proves that it proves"."
It seems that for each standard n, PA proves that the Goodstein sequence terminates for that n. If also proves that it proves that the Goodstein sequence terminates for all n, and so on. But this is very different from saying "PA proves that it proves the sentence 'for all n, the corresponding Goodstein sequence terminates,'" which is what I thought you were saying.
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.)