ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  ax-1 Structured version   Unicode 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
2 wps . . 3
32, 1wi 4 . 2
41, 3wi 4 1
Colors of variables: wff set class
This axiom is referenced by:  a1i  9  id  19  id1  20  a1d  22  a1dd  42  jarr  91  pm2.86i  92  pm2.86d  93  pm5.1im  162  biimt  230  pm5.4  238  pm4.45im  317  pm2.51  568  pm4.8  610  pm2.53  628  imorri  655  pm2.64  701  pm2.82  712  biort  726  condc  737  imorr  785  oibabs  788  pm5.12dc  804  pm5.14dc  805  peircedc  808  pm4.83dc  844  dedlem0a  861  oplem1  868  stdpc4  1636  sbequi  1698  sbidm  1709  eumo  1910  moimv  1944  euim  1946  alral  2341  r19.12  2396  r19.27av  2422  r19.37  2436  gencbval  2575  eqvinc  2640  eqvincg  2641  rr19.3v  2655  ralidm  3296  ralm  3300  class2seteq  3886  sotritric  4031  bj-findis  7393
  Copyright terms: Public domain W3C validator