Intuitionistic Propositional Logic in Lean
Dafina Trufa\c{s}
TL;DR
This paper formalizes Intuitionistic Propositional Logic in Lean, verifying completeness proofs and exploring Kripke and algebraic semantics, while establishing numerous theorems and deduction rules.
Contribution
It provides a formalization of intuitionistic logic in Lean, including completeness proofs and semantic comparisons, which is a novel contribution.
Findings
Verified two completeness proofs for intuitionistic logic
Explored relations between Kripke and algebraic semantics
Proved numerous theorems and deduction rules
Abstract
In this paper we present a formalization of Intuitionistic Propositional Logic in the Lean proof assistant. Our approach focuses on verifying two completeness proofs for the studied logical system, as well as exploring the relation between the two analyzed semantical paradigms - Kripke and algebraic. In addition, we prove a large number of theorems and derived deduction rules.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.