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  563  pm4.8  605  pm2.53  622  imorri  649  pm2.64  694  pm2.82  705  biort  719  condc  731  imorr  781  oibabs  784  pm5.12dc  800  pm5.14dc  801  peircedc  804  pm4.83dc  842  oplem1  863  stdpc4  1611  sbequi  1672  sbidm  1683  eumo  1876  moimv  1909  euim  1911  alral  2267  r19.12  2322  r19.27av  2347  r19.37  2359  gencbval  2498  eqvinc  2563  rr19.3v  2577  ralidm  3215  ralm  3219
  Copyright terms: Public domain W3C validator