But we could just as easily type “If PPT2 proves 1+2=8, then 1+2=8.” Even though 1+2=8 isn’t a theorem of PA, we can type it in as a “test sentence.”
That’s correct, as I noted in my own response. (I believe ChronoDAS meant to say something slightly different, as I explain there, but the stated claim was wrong.)
But once that’s an axiom, it can be used with the PA axioms to prove 1+2=8, which is bad.
Well, um—I just posted a proof which implies the opposite, and—I don’t expect you to go through the details of my proof if it’s obvious to you that my result is wrong, but could you at least post your argument rather than just asserting this?
I’m not sure whether you think that “If PPT.2 proves ‘1+2=8’, then 1+2=8” is an axiom of PPT.2. It is not; the axiom of PPT.2 is:
If K>0, and PPT.2 proves '1+2=8', then 1+2=8.
Now, I do claim that every statement in PPT.2 is true if K is replaced by any concrete number, like 42. Thus, I claim that you can, for example, add to PA the following axiom:
If 42>0, and PPT.2 proves '1+2=8', then 1+2=8.
And since PA would conclude this from the above axiom anyway, you might as well also add
If PPT.2 proves '1+2=8', then 1+2=8.
However, this doesn’t lead to inconsistency any more than adding the following axiom to PA:
If PA proves '1+2=8', then 1+2=8.
For example, PA_omega can prove this. The point in both cases is that while it’s consistent to add these axioms, the proof systems PA and PPT.2 to which the axioms refer do not contain the axiom itself (unlike in the case of BAD).
No, we have “If PPT2 proves that ‘if 42>0 and 1+2=8’, then ‘if 41>0 then 1+2=8’ ” as an axiom of PPT2.
Where ‘if 42>0 and 1+2=8’ is C and ‘if 41>0 then 1+2=8’ is D. Those two statements have different Gödel numbers, and therefore are different statements.
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.
That’s correct, as I noted in my own response. (I believe ChronoDAS meant to say something slightly different, as I explain there, but the stated claim was wrong.)
Well, um—I just posted a proof which implies the opposite, and—I don’t expect you to go through the details of my proof if it’s obvious to you that my result is wrong, but could you at least post your argument rather than just asserting this?
I’m not sure whether you think that “If PPT.2 proves ‘1+2=8’, then 1+2=8” is an axiom of PPT.2. It is not; the axiom of PPT.2 is:
Now, I do claim that every statement in PPT.2 is true if K is replaced by any concrete number, like 42. Thus, I claim that you can, for example, add to PA the following axiom:
And since PA would conclude this from the above axiom anyway, you might as well also add
However, this doesn’t lead to inconsistency any more than adding the following axiom to PA:
For example, PA_omega can prove this. The point in both cases is that while it’s consistent to add these axioms, the proof systems PA and PPT.2 to which the axioms refer do not contain the axiom itself (unlike in the case of BAD).
No, we have “If PPT2 proves that ‘if 42>0 and 1+2=8’, then ‘if 41>0 then 1+2=8’ ” as an axiom of PPT2.
Where ‘if 42>0 and 1+2=8’ is C and ‘if 41>0 then 1+2=8’ is D. Those two statements have different Gödel numbers, and therefore are different statements.
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.
I’m slooowly starting to figure your post out. But yeah, feel free to ignore me :P
:-)