Interesting attempt, I’m not completely clear upon the distinction between using a number n and the symbol K in the substitutions, but if we assume that bit works, I think your second paragraph proves PA_K to be inconsistent.
Since if your sentence C does not contain the constant K, then you have proved: given K>0, if PA_K proves C, then C. But all sentences which are in PA are of this form, hence by Löb’s theorem they are all true.
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.
Interesting attempt, I’m not completely clear upon the distinction between using a number n and the symbol K in the substitutions, but if we assume that bit works, I think your second paragraph proves PA_K to be inconsistent.
Since if your sentence C does not contain the constant K, then you have proved: given K>0, if PA_K proves C, then C. But all sentences which are in PA are of this form, hence by Löb’s theorem they are all true.
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.