Forcing-Based Cut-Elimination for Gentzen-Style Intuitionistic Sequent Calculus

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.

• Type: Conference
• Year: 2009
• Where: WOLLIC
• Authors: Hugo Herbelin, Gyesik Lee
• Keywords: Applied Computing, Coq Proof Assistant, Intuitionistic Completeness Proof, Intuitionistic Sequent Calculus, WOLLIC 2009