= 27d567bc2d48d9f40e9ccc20ea370b15)
CronoDAS 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)
Then C is a theorem of PA (and we're assuming that PA is sound).
EDIT: I was mistaken, see below. (If the statement doesn't contain K, then it's equivalent to a statement in PA.)
PPT.2 != BAD, so you don't have exactly the same axioms as BAD.
Yup, modulo one nit, but let me expand a bit on this answer.
Nit: C ranges over all statements; for example, it is an axiom of PPT.2 that "if K>0, and PPT.2 proves '0=1', then 0=1", even though 0=1 is not a theorem of PA. However, unless my proof is borked, it should be the case that if C doesn't contain K, then (PPT.2 proves C) iff (PA proves C), and also (PPT.2 proves C) iff (PPT.2 proves "PPT.2 proves 'C'"). Therefore, in a sense you can't apply the axiom involving C unless C is provable in PA, which is what I think you had in mind.
One possible point of confusion here is that it might seem as if replacing K by 15 would yield the proof system
NOTGOOD := PA + for every statement C, "If 15>0, and 'C' is provable in NOTGOOD, then C,"
because it may seem as if replacing every occurrence of K in the formula "PPT.2 proves 'C'" should yield the statement "NOTGOOD proves 'C'".
But this is not true: the formula "PPT.2 proves 'C'" contains no occurrence of K, not even if C contains K. This is because the formula doesn't literally contain C, it contains the unary representation of the Gödel number of C, and similarly, the predicate "PPT.2 proves ..." only talks about Gödel numbers, not about K.
Oh, I see. So we can conclude, when we replace K by 15, that "If 1=0 is provable in PPT.2, then 1=0." However, since we're not actually working in PPT.2 anymore -- we've replaced K by 15, which gave us a different proof system -- then we don't get an inconsistency.
Exactly!
Yeah, I goofed.
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
:-)