We formalize two well-known semantics for intuitionistic propositional logic: Heyting algebras and Kripke models. We prove both semantics are sound for an intuitionistic propositional logic with only implication and false. We use Heyting algebras to prove undefinability results. We also prove a Kripke model can be converted into a Heyting algebra. Assuming excluded middle, we can convert a Heyting algebra into a Kripke model. In some ways our task is made easier by the fact that the logic does not have disjunction.
The formalization depends on two Coq files which were used in Introduction to Computational Logic in 2014: the Base library (html) and a formalization PropL of propositional logic (html).
Formalization: html version; Coq code
Report: pdf