Soundness and Completeness of Implicational Logic

Asta Halkjær From 🌐 and Jørgen Villadsen 🌐

September 13, 2022

This is a development version of this entry. It might change over time and is not stable. Please refer to release versions for citations.


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.


BSD License


Session Implicational_Logic