Metamath Proof Explorer

Table of Contents - 1.3. Other axiomatizations related to classical propositional calculus

1. Minimal implicational calculus
   1. minimp
   2. minimp-syllsimp
   3. minimp-ax1
   4. minimp-ax2c
   5. minimp-ax2
   6. minimp-pm2.43
2. Implicational Calculus
   1. impsingle
   2. impsingle-step4
   3. impsingle-step8
   4. impsingle-ax1
   5. impsingle-step15
   6. impsingle-step18
   7. impsingle-step19
   8. impsingle-step20
   9. impsingle-step21
   10. impsingle-step22
   11. impsingle-step25
   12. impsingle-imim1
   13. impsingle-peirce
   14. tarski-bernays-ax2
3. Derive the Lukasiewicz axioms from Meredith's sole axiom
   1. meredith
   2. merlem1
   3. merlem2
   4. merlem3
   5. merlem4
   6. merlem5
   7. merlem6
   8. merlem7
   9. merlem8
   10. merlem9
   11. merlem10
   12. merlem11
   13. merlem12
   14. merlem13
   15. luk-1
   16. luk-2
   17. luk-3
4. Derive the standard axioms from the Lukasiewicz axioms
   1. luklem1
   2. luklem2
   3. luklem3
   4. luklem4
   5. luklem5
   6. luklem6
   7. luklem7
   8. luklem8
   9. ax1
   10. ax2
   11. ax3
5. Derive Nicod's axiom from the standard axioms
   1. nic-dfim
   2. nic-dfneg
   3. nic-mp
   4. nic-mpALT
   5. nic-ax
   6. nic-axALT
6. Derive the Lukasiewicz axioms from Nicod's axiom
   1. nic-imp
   2. nic-idlem1
   3. nic-idlem2
   4. nic-id
   5. nic-swap
   6. nic-isw1
   7. nic-isw2
   8. nic-iimp1
   9. nic-iimp2
   10. nic-idel
   11. nic-ich
   12. nic-idbl
   13. nic-bijust
   14. nic-bi1
   15. nic-bi2
   16. nic-stdmp
   17. nic-luk1
   18. nic-luk2
   19. nic-luk3
7. Derive Nicod's Axiom from Lukasiewicz's First Sheffer Stroke Axiom
   1. lukshef-ax1
   2. lukshefth1
   3. lukshefth2
   4. renicax
8. Derive the Lukasiewicz Axioms from the Tarski-Bernays-Wajsberg Axioms
   1. tbw-bijust
   2. tbw-negdf
   3. tbw-ax1
   4. tbw-ax2
   5. tbw-ax3
   6. tbw-ax4
   7. tbwsyl
   8. tbwlem1
   9. tbwlem2
   10. tbwlem3
   11. tbwlem4
   12. tbwlem5
   13. re1luk1
   14. re1luk2
   15. re1luk3
9. Derive the Tarski-Bernays-Wajsberg axioms from Meredith's First CO Axiom
   1. merco1
   2. merco1lem1
   3. retbwax4
   4. retbwax2
   5. merco1lem2
   6. merco1lem3
   7. merco1lem4
   8. merco1lem5
   9. merco1lem6
   10. merco1lem7
   11. retbwax3
   12. merco1lem8
   13. merco1lem9
   14. merco1lem10
   15. merco1lem11
   16. merco1lem12
   17. merco1lem13
   18. merco1lem14
   19. merco1lem15
   20. merco1lem16
   21. merco1lem17
   22. merco1lem18
   23. retbwax1
10. Derive the Tarski-Bernays-Wajsberg axioms from Meredith's Second CO Axiom
    1. merco2
    2. mercolem1
    3. mercolem2
    4. mercolem3
    5. mercolem4
    6. mercolem5
    7. mercolem6
    8. mercolem7
    9. mercolem8
    10. re1tbw1
    11. re1tbw2
    12. re1tbw3
    13. re1tbw4
11. Derive the Lukasiewicz axioms from the Russell-Bernays Axioms
    1. rb-bijust
    2. rb-imdf
    3. anmp
    4. rb-ax1
    5. rb-ax2
    6. rb-ax3
    7. rb-ax4
    8. rbsyl
    9. rblem1
    10. rblem2
    11. rblem3
    12. rblem4
    13. rblem5
    14. rblem6
    15. rblem7
    16. re1axmp
    17. re2luk1
    18. re2luk2
    19. re2luk3
12. Stoic logic non-modal portion (Chrysippus of Soli)
    1. mptnan
    2. mptxor
    3. mtpor
    4. mtpxor
    5. stoic1a
    6. stoic1b
    7. stoic2a
    8. stoic2b
    9. stoic3
    10. stoic4a
    11. stoic4b