Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-1 | GIF version |
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.) |
Ref | Expression |
---|---|
ax-1 | ⊢ (𝜑 → (𝜓 → 𝜑)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | wph | . 2 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 2, 1 | wi 4 | . 2 wff (𝜓 → 𝜑) |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → (𝜓 → 𝜑)) |
Colors of variables: wff set class |
This axiom is referenced by: a1i 9 id 19 idALT 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 581 pm4.8 623 pm2.53 641 imorri 668 pm2.64 714 pm2.82 725 biort 738 condc 749 imorr 797 oibabs 800 pm5.12dc 816 pm5.14dc 817 peircedc 820 pm4.83dc 858 dedlem0a 875 oplem1 882 stdpc4 1658 sbequi 1720 sbidm 1731 eumo 1932 moimv 1966 euim 1968 alral 2367 r19.12 2422 r19.27av 2448 r19.37 2462 gencbval 2602 eqvinc 2667 eqvincg 2668 rr19.3v 2682 ralidm 3321 ralm 3325 class2seteq 3916 sotritric 4061 elnnnn0b 8226 zltnle 8291 iccneg 8857 qltnle 9101 frec2uzlt2d 9190 algcvgblem 9888 bj-findis 10104 |
Copyright terms: Public domain | W3C validator |