Less Wrong is a community blog devoted to refining the art of human rationality. Please visit our About page for more information.

Comment author: Ender 24 June 2012 07:16:27PM 1 point [-]

I think that this is what the theorem means;

If (X->Y) -> Y, then ~X -> Y (If it's true that "If it's true that 'if X is true, then Y is true,' then Y must be true," then Y must be true, even if X is not true).

This makes sense because the first line, "(X->Y) -> Y," can be true whether or not X is actually true. The fact that ~X -> Y if this is true is an overly specific example of that "The first line being true (regardless of the truth of X)" -> Y. It's actually worded kind of weirdly, unless "imply" means something different in Logicianese than it does in colloquial English; ~X isn't really "implying" Y, it's just irrelevant.

This doesn't mean that "(X -> Y) -> Y" is always true. I actually can't think of any intuitive situations where this could be true. It's not true that the fact that "if Jesus really had come back to life, Christians would be Less Wrong about stuff" implies that Christians would be Less Wrong about stuff even if Jesus really hadn't come back to life.


To anyone who wants to tell me I'm wrong about this; If I'm wrong about this, and you know because you've learned about this in a class, whereas I just worked this out for myself, I'd appreciate it if you told me and mentioned that you've learned about this somewhere and know more than I do. If logic is another one of those fields where people who know a lot about it HATE it when people who don't know much about it try to work stuff out for themselves (like Physics and AI), I'd definitely like to know so that I don't throw out wrong answers in the future. Thanks.

Comment author: VHanson 21 January 2014 02:37:26AM 0 points [-]

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.