Skip to Main content Skip to Navigation
Conference papers

Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus

Hugo Herbelin 1, 2 Gyesik Lee 3, *
* Corresponding author
2 PI.R2 - Design, study and implementation of languages for proofs and programs
PPS - Preuves, Programmes et Systèmes, Inria Paris-Rocquencourt, UPD7 - Université Paris Diderot - Paris 7, CNRS - Centre National de la Recherche Scientifique : UMR7126
Abstract : We give a simple intuitionistic completeness proof of Kripke semantics for intuitionistic logic with implication and universal quantification with respect to cut-free intuitionistic sequent calculus. The Kripke semantics is ``simplified'' in the way that the domain remains constant. The proof has been formalised in the Coq proof assistant and by combining soundness with completeness, we obtain an executable cut-elimination procedure. The proof easily extends to the case of the absurdity connective using Kripke models with exploding nodes à la Veldman.
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Hugo Herbelin Connect in order to contact the contributor
Submitted on : Tuesday, May 5, 2009 - 6:48:07 PM
Last modification on : Saturday, March 28, 2020 - 2:09:08 AM
Long-term archiving on: : Monday, October 15, 2012 - 9:56:37 AM


Files produced by the author(s)


  • HAL Id : inria-00381554, version 1



Hugo Herbelin, Gyesik Lee. Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus. Workshop on Logic, Language, Information and Computation, Jun 2009, Tokyo, Japan. pp.209-217. ⟨inria-00381554⟩



Record views


Files downloads