Hacker News new | ask | show | jobs
by thaumasiotes 2943 days ago
No, it would be the same rule, just phrased better. The rule works by introducing a disjunction (to match the one you already have), not by eliminating one.

Given

    a implies p
    b implies p
    a or b
you can conclude ((a or b) implies p) from my statement of the rule, and then conclude "p" from modus ponens. And if you're feeling really obscurist, you can rename modus ponens to "proposition elimination".

But notice that if you have

    a implies p
    b implies p
    c implies p
    a or b or c
then my statement of the rule will still allow you to conclude "p", whereas the statement on wikipedia won't.
1 comments

You misunderstand my comment. I'm not saying that your interpretation is wrong. I'm fine with it. Better or not, either result can be used in the right context. I'm saying that your interpretation does not eliminate disjunction, so it should be called differently. It's a different rule, that's all I want to say.
> Better or not, either result can be used in the right context.

This is most of the point I'm making -- there is no context where the brittle, overspecified version is useful but the more general version isn't. But there are lots of contexts where the overspecified version is useless.

And again, it's not a different rule. Brittle "disjunction elimination" is a special case of the rule I state. Similarly, the Pythagorean Theorem is a special case of the Law of Cosines, not a different rule.

It gets worse, though, because where the Pythagorean Theorem is simpler to state than the Law of Cosines, brittle disjunction elimination is more complex to state than the more general result is.

Think about exportation. We say:

    (a implies (b implies p)) iff ((a and b) implies p)
We don't say:

    ((a implies (b implies p)) and (a and b)) implies p
That second version, which is the equivalent of brittle disjunction elimination for and instead of or, is harder to state, is less informative, and doesn't generalize.