**Description: **Modus tollendo ponens
(inclusive-or version), aka disjunctive
syllogism. This is similar to mtp-xor 1536, one of the five original
"indemonstrables" in Stoic logic. However, in Stoic logic
this rule
used exclusive-or, while the name modus tollendo ponens often refers to
a variant of the rule that uses inclusive-or instead. The rule says,
"if
is not true, and or (or
both) are true, then
must be
true." An alternative phrasing is, "Once you eliminate
the impossible, whatever remains, no matter how improbable, must be the
truth." -- Sherlock Holmes (Sir Arthur Conan Doyle, 1890: The Sign
of
the Four, ch. 6). (Contributed by David A. Wheeler, 3-Jul-2016.)
(Proof shortened by Wolf Lammen,
11-Nov-2017.) |