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

* 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.
Keywords :
Document type :
Conference papers
Domain :

Cited literature [14 references]

https://hal.inria.fr/inria-00381554
Contributor : Hugo Herbelin <>
Submitted on : Tuesday, May 5, 2009 - 6:48:07 PM
Last modification on : Monday, June 24, 2019 - 10:22:03 AM
Long-term archiving on : Monday, October 15, 2012 - 9:56:37 AM

### File

wollic-HerLee09-kripke-cut-eli...
Files produced by the author(s)

### Identifiers

• HAL Id : inria-00381554, version 1

### Citation

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