But PA_K cannot prove that K>0. I think all your argument shows is that PA_K + “K>0” is a strictly stronger language that can prove the consistency of PA_K.
I’m rather confident that PA_K is conservative over PA(1) for the reason given in the second note at the end of the post, which implies that PA_K is consistent. However, the second paragraph of the proof sketch is definitely broken, so it’s possible that it implies incorrect things. Nevertheless, I don’t think your argument works.
I recently posted a comment giving an overview of my attempt to fix my proof; it contains a proof sketch for the soundness, and therefore consistency, of the system PPT considered in that comment, which I’m hoping is relatively easy to follow. If you can poke holes into that one or if you have other comments on it, that could be very helpful.
But PA_K cannot prove that K>0. I think all your argument shows is that PA_K + “K>0” is a strictly stronger language that can prove the consistency of PA_K.
I’m rather confident that PA_K is conservative over PA(1) for the reason given in the second note at the end of the post, which implies that PA_K is consistent. However, the second paragraph of the proof sketch is definitely broken, so it’s possible that it implies incorrect things. Nevertheless, I don’t think your argument works.
I recently posted a comment giving an overview of my attempt to fix my proof; it contains a proof sketch for the soundness, and therefore consistency, of the system PPT considered in that comment, which I’m hoping is relatively easy to follow. If you can poke holes into that one or if you have other comments on it, that could be very helpful.