![]() |
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 42 jarr 91 pm2.86i 92 pm2.86d 93 pm5.1im 162 biimt 230 pm5.4 238 pm4.45im 317 pm2.51 580 pm4.8 622 pm2.53 640 imorri 667 pm2.64 713 pm2.82 724 biort 737 condc 748 imorr 796 oibabs 799 pm5.12dc 815 pm5.14dc 816 peircedc 819 pm4.83dc 857 dedlem0a 874 oplem1 881 stdpc4 1655 sbequi 1717 sbidm 1728 eumo 1929 moimv 1963 euim 1965 alral 2361 r19.12 2416 r19.27av 2442 r19.37 2456 gencbval 2596 eqvinc 2661 eqvincg 2662 rr19.3v 2676 ralidm 3315 ralm 3319 class2seteq 3907 sotritric 4052 elnnnn0b 8002 zltnle 8067 iccneg 8627 frec2uzlt2d 8871 bj-findis 9439 |
Copyright terms: Public domain | W3C validator |