Lo! A cartoon proof of Löb's Theorem!
Löb's Theorem shows that a mathematical system cannot assert its own soundness without becoming inconsistent. Marcello and I wanted to be able to see the truth of Löb's Theorem at a glance, so we doodled it out in the form of a cartoon. (An inability to trust assertions made by a proof system isomorphic to yourself, may be an issue for self-modifying AIs.)
It was while learning mathematical logic that I first learned to rigorously distinguish between X, the truth of X, the quotation of X, a proof of X, and a proof that X's quotation was provable.
The cartoon guide follows as an embedded Scribd document after the jump, or you can download as a PDF file. Afterward I offer a medium-hard puzzle to test your skill at drawing logical distinctions.
Cartoon Guide to Löb's ... by on Scribd
Cartoon Guide to Löb's Theorem - Upload a Document to Scribd
And now for your medium-hard puzzle:
The Deduction Theorem (look it up) states that whenever assuming a hypothesis H enables us to prove a formula F in classical logic, then (H->F) is a theorem in classical logic.
Let ◻Z stand for the proposition "Z is provable". Löb's Theorem shows that, whenever we have ((◻C)->C), we can prove C.
Applying the Deduction Theorem to Löb's Theorem gives us, for all C:
((◻C)->C)->C
However, those familiar with the logic of material implication will realize that:
(X->Y)->Y
implies
(not X)->Y
Applied to the above, this yields (not ◻C)->C.
That is, all statements which lack proofs are true.
I cannot prove that 2 = 1.
Therefore 2 = 1.
Can you exactly pinpoint the flaw?
I did study stuff like this a LONG time ago, so I respect your trying to work this out from 'common sense'. The way I see it, the key to the puzzle is the truth-value of Y, not 'whether or not X is actually true'. By working out the truth-tables for the various implications, the statement "((◻C)->C)->C" has a False truth-value when both (◻C) and C are False, i.e. if C is both unprovable and false the statement is false. Even though the 'material implication' "(X->Y)->Y implies (not X)->Y" is a tautology (because when the 1st part is false the 2nd part is true & vice-versa) that does not guarantee the truth of the 2nd part alone. In fact, it is intuitively unsurprising that if C is false, the premise that 'C is provable' is also false (of course such intuition is logically unreliable, but it feels nice to me when it happens to be confirmed in a truth table). What may seem counterintuitive is that this is the only case for which the premise is True, but the encompassing implication is False. That's because a 'logical implication' is equivalent to stating that 'either the premise (1st part) is False or the conclusion (2nd part) is True (or both)'. So, for the entire statement "((◻C)->C)->C" to be True when C is False, means "((◻C)->C)" must be False. "((◻C)->C)" is only False when "(◻C)" is True and "C" is False. Here's where the anti-intuitive feature of material implication causes brain-freeze - that with a false premise any implication is assigned a True truth-value. But that does NOT mean that such an implication somehow forces the conclusion to be true! It only affirms that for any implication to be true, it must be the case that "IF the premise is true then the conclusion is true." If the premise is False, the conclusion may be True or False. If the premise is True and the conclusion is False, then the implication itself is False!
The translation of " (not ◻C)->C" as "all statements which lack proofs are true" is a ringer. I'd say the implication "If it is not the case that C is provable, then C is True" is equivalent to saying "Either C is provable or C is True or both." Both of these recognize that the case for which "C is provable" and "C is False" makes the implication itself False. The mistranslation erroneously eliminates consideration of the case in which C is both unprovable an False, which is (not coincidentally, I suspect) the one case for which the grand formulation "((◻C)->C)->C" is False.
Jeepers. I haven't thought about this problem for a long time. Thanks.
The answer that occurs to me for the original puzzle is that Yudkowsky never proved (◻(2 = 1) -> (2 = 1)). I don't know it that is actually the answer, but I really need to go do other work and stop thinking about this problem.