>>14337577>No, the issue is that it doesn't serve as a foundation that Hilbert wantedWhy not?
>If you use PRA to prove the consistency of PA, great! FYI PRA alone does not prove consistency of PA. PRA is weaker than PA.
>But all you've done is shift the goalpost to having to prove PRA is consistent, and what are you going to use to do that?You don't need to prove PRA consistent for the proof to be valuable and convincing. The proof can be encoded within PRA, but it also can be encoded within other systems. The proof has value in and of itself, without reference to systems within which it is encoded. What matters is that it's finitist proof of the consistency of PA, without involving any kind of completed infinities or other vague, undefined notions. As such, it provides a very strong evidence for the consistency of PA.
If you have any particular step of the proof of Con(PA) that you object to or find questionable, feel free to bring it up.