= 27d567bc2d48d9f40e9ccc20ea370b15)
Decius comments on How to cheat Löb's Theorem: my second try - Less Wrong Discussion
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)
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.