![]() |
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 328 pm2.51 619 pm4.8 661 pm2.53 679 imorri 706 jao1i 748 pm2.64 753 pm2.82 764 biort 777 condc 790 imorr 838 oibabs 841 pm5.12dc 857 pm5.14dc 858 peircedc 861 pm4.83dc 900 dedlem0a 917 oplem1 924 stdpc4 1712 sbequi 1774 sbidm 1786 eumo 1987 moimv 2021 euim 2023 alral 2432 r19.12 2491 r19.27av 2518 r19.37 2533 gencbval 2681 eqvinc 2754 eqvincg 2755 rr19.3v 2769 ralidm 3402 ralm 3406 class2seteq 4019 exmid0el 4056 sotritric 4175 elnnnn0b 8815 zltnle 8894 iccneg 9555 qltnle 9806 frec2uzlt2d 9960 hashfzp1 10363 algcvgblem 11474 bj-findis 12598 |
Copyright terms: Public domain | W3C validator |