Syntax vs Semantics: Comparing Consistency Proofs for Minimal Propositional Logics

<p>&nbsp; Consistency is a key property of any logical system. However, proofs of<br> &nbsp; consistency usually rely on heavy proof theory notions like admissibility<br> &nbsp; of cut. A more semantics-based approach to consistency proofs explores the<br> &nbsp; correspondence between a logic and its relationship with the<br> &nbsp; evaluation in a lambda-calculus, known as Curry-Howard isomorphism.<br> &nbsp; In this work, we present a comparison between two<br> &nbsp; formalizations of consistency for minimal propositional logic: one using a<br> &nbsp; semantic-based approach and another following the (traditional) syntactic,<br> &nbsp; proof-theoretical approach in both Coq proof assistant and Agda programming<br> &nbsp; language. We conclude by discussing the lessons learned during<br> &nbsp; the cerfication of these results in both languages.</p>