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 627 pm4.8 681 oibabs 688 imorr 695 pm2.53 696 imorri 723 jao1i 770 pm2.64 775 pm2.82 786 biort 799 condcOLD 824 pm5.12dc 880 pm5.14dc 881 peircedc 884 pm4.83dc 920 dedlem0a 937 oplem1 944 stdpc4 1733 sbequi 1795 sbidm 1807 eumo 2009 moimv 2043 euim 2045 alral 2455 r19.12 2515 r19.27av 2544 r19.37 2560 gencbval 2708 eqvinc 2782 eqvincg 2783 rr19.3v 2797 ralidm 3433 ralm 3437 class2seteq 4057 exmid0el 4097 sotritric 4216 elnnnn0b 8979 zltnle 9058 iccneg 9727 qltnle 9978 frec2uzlt2d 10132 hashfzp1 10525 algcvgblem 11642 bj-trst 12847 bj-findis 13073 |
Copyright terms: Public domain | W3C validator |