![]() |
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 jarri 98 pm2.86i 99 pm2.86d 100 pm5.1im 173 biimt 241 pm5.4 249 pm4.45im 334 conax1 653 pm4.8 707 oibabs 714 imorr 721 pm2.53 722 imorri 749 jao1i 796 pm2.64 801 pm2.82 812 condcOLD 854 pm5.12dc 910 pm5.14dc 911 peircedc 914 pm4.83dc 951 dedlem0a 968 oplem1 975 stdpc4 1775 sbequi 1839 sbidm 1851 eumo 2058 moimv 2092 euim 2094 alral 2522 r19.12 2583 r19.27av 2612 r19.37 2629 gencbval 2785 eqvinc 2860 eqvincg 2861 rr19.3v 2876 ralidm 3523 ralm 3527 class2seteq 4163 exmid0el 4204 sotritric 4324 elnnnn0b 9219 zltnle 9298 iccneg 9988 qltnle 10245 frec2uzlt2d 10403 hashfzp1 10803 algcvgblem 12048 bj-trst 14461 bj-findis 14701 |
Copyright terms: Public domain | W3C validator |