ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-3 Structured version   GIF version

Axiom ax-3 2512
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 2542, 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.)

Assertion
Ref Expression
ax-3 ((¬ φ → ¬ ψ) → (ψφ))

Detailed syntax breakdown of Axiom ax-3
StepHypRef Expression
1 wph . . . 4 wff φ
21wn 3 . . 3 wff ¬ φ
3 wps . . . 4 wff ψ
43wn 3 . . 3 wff ¬ ψ
52, 4wi 4 . 2 wff φ → ¬ ψ)
63, 1wi 4 . 2 wff (ψφ)
75, 6wi 4 1 wff ((¬ φ → ¬ ψ) → (ψφ))
Colors of variables: wff set class
This axiom is referenced by:  con4d  2513
  Copyright terms: Public domain W3C validator