Intuitionistic Logic Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > ILE Home > Th. List > ax-1 | GIF 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 wff 𝜑 | |
2 | wps | . . 3 wff 𝜓 | |
3 | 2, 1 | wi 4 | . 2 wff (𝜓 → 𝜑) |
4 | 1, 3 | wi 4 | 1 wff (𝜑 → (𝜓 → 𝜑)) |
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 642 pm4.8 696 oibabs 703 imorr 710 pm2.53 711 imorri 738 jao1i 785 pm2.64 790 pm2.82 801 biort 814 condcOLD 839 pm5.12dc 895 pm5.14dc 896 peircedc 899 pm4.83dc 935 dedlem0a 952 oplem1 959 stdpc4 1748 sbequi 1811 sbidm 1823 eumo 2031 moimv 2065 euim 2067 alral 2478 r19.12 2538 r19.27av 2567 r19.37 2583 gencbval 2734 eqvinc 2808 eqvincg 2809 rr19.3v 2823 ralidm 3463 ralm 3467 class2seteq 4087 exmid0el 4127 sotritric 4246 elnnnn0b 9021 zltnle 9100 iccneg 9772 qltnle 10023 frec2uzlt2d 10177 hashfzp1 10570 algcvgblem 11730 bj-trst 12951 bj-findis 13177 |
Copyright terms: Public domain | W3C validator |