Forcing-based cut-elimination for Gentzen-style intuitionistic sequent calculus - Archive ouverte HAL Access content directly
Conference Papers Year : 2009

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

(1, 2) , (3)
1
2
3

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.
Fichier principal
Vignette du fichier
wollic-HerLee09-kripke-cut-elim.pdf (118.71 Ko) Télécharger le fichier
Origin : Files produced by the author(s)
Loading...

Dates and versions

inria-00381554 , version 1 (05-05-2009)

Identifiers

  • HAL Id : inria-00381554 , version 1

Cite

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⟩
167 View
288 Download

Share

Gmail Facebook Twitter LinkedIn More