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

Axiom ax-1 5
Description: Axiom Simp. Axiom A1 of [Margaris] p. 49. One of the axioms of propositional calculus. This axiom is called Simp or "the principle of simplification" in Principia Mathematica (Theorem *2.02 of [WhiteheadRussell] p. 100) because "it enables us to pass from the joint assertion of φ and ψ to the assertion of φ simply."

The theorems of propositional calculus are also called tautologies. Although classical propositional logic tautologies can be proved using truth tables, there is no similarly simple system for intuitionistic propositional logic, so proving tautologies from axioms is the preferred approach. (Contributed by NM, 5-Aug-1993.)

Assertion
Ref Expression
ax-1 (φ → (ψφ))

Detailed syntax breakdown of Axiom ax-1
StepHypRef Expression
1 wph . 2 wff φ
2 wps . . 3 wff ψ
32, 1wi 4 . 2 wff (ψφ)
41, 3wi 4 1 wff (φ → (ψφ))
Colors of variables: wff set class
This axiom is referenced by:  a1i  9  id  17  id1  18  a1d  20  a1dd  40  jarr  89  pm2.86i  90  pm2.86d  91  pm5.1im  160  biimt  228  pm5.4  236  pm4.45im  315  pm2.51  562  pm4.8  604  pm2.53  620  imorri  647  pm2.64  692  pm2.82  703  biort  717  condc  724  oibabs  772  pm5.12dc  785  pm5.14dc  786  peircedc  789  pm4.83dc  824  oplem1  844  stdpc4  1580  sbequi  1641  sbidm  1652  eumo  1845  moimv  1878  euim  1880  alral  2236  r19.12  2291  r19.27av  2316  r19.37  2328  gencbval  2467  eqvinc  2532  rr19.3v  2546
  Copyright terms: Public domain W3C validator