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