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  565  pm4.8  607  pm2.53  625  imorri  652  pm2.64  698  pm2.82  709  biort  722  condc  733  imorr  781  oibabs  784  pm5.12dc  800  pm5.14dc  801  peircedc  804  pm4.83dc  840  dedlem0a  857  oplem1  864  stdpc4  1631  sbequi  1693  sbidm  1704  eumo  1905  moimv  1939  euim  1941  alral  2336  r19.12  2391  r19.27av  2417  r19.37  2431  gencbval  2570  eqvinc  2635  eqvincg  2636  rr19.3v  2650  ralidm  3289  ralm  3293  class2seteq  3879  sotritric  4024  elnnnn0b  7800  zltnle  7862  bj-findis  8359
  Copyright terms: Public domain W3C validator