VAuroch comments on The Cartoon Guide to Löb's Theorem - Less Wrong
You are viewing a comment permalink. View the original post to see all comments and the full post content.
You are viewing a comment permalink. View the original post to see all comments and the full post content.
Comments (90)
I may not removed the flaw entirely, but I have definitely changed it into a less-obviously bad flaw. And also used Loeb's Theorem to derive Goedel's, or a close analogue.
The summary statement of Loeb is wrong. It is not the case that (◻X->X) -> X, it is only the case that ◻(◻X->X) -> ◻X. That is to say, that if (a proof of X implies X) is provable, then X is provable.
Using Deduction here, we get only ◻(~◻X) -> ◻X, which in English is "If it is provable that X is unprovable, then X is provable", or in other words "If PA is proved complete, it is proved inconsistent."