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.
Liste complète des métadonnées

Cited literature [14 references]  Display  Hide  Download

https://hal.inria.fr/inria-00381554
Contributor : Hugo Herbelin <>
Submitted on : Tuesday, May 5, 2009 - 6:48:07 PM
Last modification on : Friday, January 4, 2019 - 5:33:25 PM
Document(s) archivé(s) le : 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

Collections

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⟩

Share

Metrics

Record views

301

Files downloads

159