Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-1 | Unicode 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 | |
2 | wps | . . 3 | |
3 | 2, 1 | wi 4 | . 2 |
4 | 1, 3 | wi 4 | 1 |
Colors of variables: wff set class |
This axiom is referenced by: a1i 9 id 19 idALT 20 a1d 22 a1dd 48 jarr 97 pm2.86i 98 pm2.86d 99 pm5.1im 172 biimt 240 pm5.4 248 pm4.45im 332 conax1 648 pm4.8 702 oibabs 709 imorr 716 pm2.53 717 imorri 744 jao1i 791 pm2.64 796 pm2.82 807 condcOLD 849 pm5.12dc 905 pm5.14dc 906 peircedc 909 pm4.83dc 946 dedlem0a 963 oplem1 970 stdpc4 1768 sbequi 1832 sbidm 1844 eumo 2051 moimv 2085 euim 2087 alral 2515 r19.12 2576 r19.27av 2605 r19.37 2622 gencbval 2778 eqvinc 2853 eqvincg 2854 rr19.3v 2869 ralidm 3514 ralm 3518 class2seteq 4147 exmid0el 4188 sotritric 4307 elnnnn0b 9166 zltnle 9245 iccneg 9933 qltnle 10189 frec2uzlt2d 10347 hashfzp1 10746 algcvgblem 11990 bj-trst 13733 bj-findis 13974 |
Copyright terms: Public domain | W3C validator |