![]() |
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 ![]() ![]() ![]() 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 643 pm4.8 697 oibabs 704 imorr 711 pm2.53 712 imorri 739 jao1i 786 pm2.64 791 pm2.82 802 biort 815 condcOLD 840 pm5.12dc 896 pm5.14dc 897 peircedc 900 pm4.83dc 936 dedlem0a 953 oplem1 960 stdpc4 1749 sbequi 1812 sbidm 1824 eumo 2032 moimv 2066 euim 2068 alral 2481 r19.12 2541 r19.27av 2570 r19.37 2586 gencbval 2737 eqvinc 2812 eqvincg 2813 rr19.3v 2827 ralidm 3468 ralm 3472 class2seteq 4095 exmid0el 4135 sotritric 4254 elnnnn0b 9045 zltnle 9124 iccneg 9802 qltnle 10054 frec2uzlt2d 10208 hashfzp1 10602 algcvgblem 11766 bj-trst 13122 bj-findis 13348 |
Copyright terms: Public domain | W3C validator |