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
Hugo Herbelin
• Function : Author
• PersonId : 833422
Gyesik Lee
• Function : Correspondent author
• PersonId : 859226

Connectez-vous pour contacter l'auteur

#### 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.

### 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⟩

### Export

BibTeX TEI Dublin Core DC Terms EndNote Datacite

167 View