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