**Description: **Modus tollendo ponens
(original exclusive-or version), aka disjunctive
syllogism, similar to mtpor 1578, one of the five "indemonstrables"
in
Stoic logic. The rule says, "if is not true, and either
or
(exclusively) are true, then must be true." Today the
name "modus tollendo ponens" often refers to a variant, the
inclusive-or
version as defined in mtpor 1578. See rule 3 on [Lopez-Astorga] p. 12
(note that the "or" is the same as mptxor 1577, that is, it is
exclusive-or df-xor 1352), rule 3 of [Sanford] p. 39 (where it is not as
clearly stated which kind of "or" is used but it appears to be
in the
same sense as mptxor 1577), and rule A5 in [Hitchcock] p. 5 (exclusive-or
is expressly used). (Contributed by David A. Wheeler, 4-Jul-2016.)
(Proof shortened by Wolf Lammen, 11-Nov-2017.) (Proof shortened by BJ,
19-Apr-2019.) |