**Description: **Modus tollendo ponens
(original exclusive-or version), aka disjunctive
syllogism, similar to mtpor 1316, 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 1316. See rule 3 on [Lopez-Astorga] p. 12
(note that the "or" is the same as mptxor 1315, that is, it is
exclusive-or df-xor 1267), 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 1315), 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.) |