The closest axiom PPT.2 has to the one you’re claiming is “If K>0, and PPT.2 proves that ‘if K>0 and 1+2=8’, then (if K-1>0, then 1+2=8).” If you substitute 42 for K—which does NOT give you another axiom or AFAICT theorem of PPT.2, but if you do it anyway—then you get the formula, “If 42>0, and PPT.2 proves that ‘if K>0 and 1+2=8’, then (if 42-1>0, then 1+2=8).” I’m not sure how you came up with the statement you claim to be an axiom of PPT.2, and I’m not sure what point you are trying to make.
No, it doesn’t give you an axiom or theorem, it gives you a statement. In particular, it gives you a statement which does not prove itself through Lobs theorem.
Huh?
The closest axiom PPT.2 has to the one you’re claiming is “If K>0, and PPT.2 proves that ‘if K>0 and 1+2=8’, then (if K-1>0, then 1+2=8).” If you substitute 42 for K—which does NOT give you another axiom or AFAICT theorem of PPT.2, but if you do it anyway—then you get the formula, “If 42>0, and PPT.2 proves that ‘if K>0 and 1+2=8’, then (if 42-1>0, then 1+2=8).” I’m not sure how you came up with the statement you claim to be an axiom of PPT.2, and I’m not sure what point you are trying to make.
No, it doesn’t give you an axiom or theorem, it gives you a statement. In particular, it gives you a statement which does not prove itself through Lobs theorem.