= 27d567bc2d48d9f40e9ccc20ea370b15)
Manfred comments on How to cheat Löb's Theorem: my second try - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
= 783df68a0f980790206b9ea87794c5b6)
Loading…= b715d02e85f7b3b4ae65ca3d3e450868)
Subscribe to RSS Feed
Powered by Reddit
= f037147d6e6c911a85753b9abdedda8d)
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (25)
Not necessarily. For example, replace C with "X+Y=Z" (I'm just copying form the cartoon guide here). The axiom then becomes "If PPT2 proves X+Y=Z, then X+Y=Z."
Now replace X with 1, Y with 2, and Z with 3. "If PPT2 proves 1+2=3, then 1+2=3."
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." But once that's an axiom, it can be used with the PA axioms to prove 1+2=8, which is bad.
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
:-)