We give a simple intuitionistic completeness proof of Kripke semantics with constant domain for intuitionistic logic with implication and universal quantification. We use a cut-free intuitionistic sequent calculus as formal system and by combining soundness with completeness, we obtain an executable cut-elimination procedure. The proof, which has been formalised in the Coq proof assistant, easily extends to the case of the absurdity connective using Kripke models with exploding nodes.
Swipe to navigate through the chapters of this book
Please log in to get access to this content
To get access to this content you need the following product:
- Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus
- Springer Berlin Heidelberg
- Sequence number
Neuer Inhalt/© ITandMEDIA