### Abstract

This work is a formalization of soundness and completeness of the Bernays-Tarski axiom system for classical implicational logic. The completeness proof is constructive following the approach by László Kalmár, Elliott Mendelson and others. The result can be extended to full classical propositional logic by uncommenting a few lines for falsehood.

### License

BSD License

### Topics

- Logic/General logic/Classical propositional logic
- Logic/Proof theory

### Session Implicational_Logic

- Implicational_Logic
- Implicational_Logic_Appendix

## Cite

×

Implicational_Logic-AFP

    @article{Implicational_Logic-AFP,
      author  = {Asta Halkjær From and Jørgen Villadsen},
      title   = {Soundness and Completeness of Implicational Logic},
      journal = {Archive of Formal Proofs},
      month   = {September},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/Implicational_Logic.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Sep 19, 2022 : Isabelle2021-1