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