Email Gateway (Sep 19 2022 at 18:11): Email Gateway (Sep 19 2022 at 18:11):From: Gerwin Klein <kleing@unsw.edu.au>
Soundness and Completeness of Implicational Logic
by Asta Halkjær From and Jørgen Villadsen
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.
https://www.isa-afp.org/entries/Implicational_Logic.html
Enjoy!
Gerwin
Last updated: Apr 29 2024 at 04:18 UTC