**Description: **Axiom *Transp*.
Axiom A3 of [Margaris] p. 49.
Unconditional form of condc 723. We state this as an axiom for the benefit
of theorems which have not yet been converted over to having appropriate
decidability conditions added. We could also transform intuitionistic
logic to classical logic by adding unconditional forms of exmiddc 719,
peirce 2069, or notnot2dc 725.
This axiom swaps or "transposes" the order of the consequents
when
negation is removed. An informal example is that the statement "if
there
are no clouds in the sky, it is not raining" implies the statement
"if it
is raining, there are clouds in the sky." This axiom is called
*Transp*
or "the principle of transposition" in *Principia
Mathematica* (Theorem
*2.17 of [WhiteheadRussell] p.
103). We will also use the term
"contraposition" for this principle, although the reader is
advised that
in the field of philosophical logic, "contraposition" has a
different
technical meaning. (Contributed by NM, 5-Aug-1993.)
(New usage is discouraged.) |