[thaumasiotes]

Wow, that rule is stated horribly.

You'd get much more value from phrasing it as

    ((p implies r) and (q implies r)) iff ((p or q) implies r).

No need to have a special rule stating that when you also have (p or q), you can resolve all three to just "r" in one step instead of two steps.

[a-nikolaev]

Well, then it would be a different rule. The one I referred to, eliminates disjunction, and so that's where its name is coming from.

[thaumasiotes]

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.

[a-nikolaev]

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.

[thaumasiotes]

> 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.

[abakker]

I really really wish math jargon and symbols could be replaced with code. I feel like I could have done a lot better in math if it had been taught in python.

[a-nikolaev]

Programming languages generally capture only some specific logic (or some specific kind of math) in their semantics.

Certain concepts like the law of excluded middle (either A or not A must hold), and proofs by contradiction that are common in math, simply don't exist in programming. That's because programming is based on constructive logic / constructive math foundation.

Learning the basics of logic can be beneficial for a programmer tho, and the connection with functional programming is especially high.