Single Conclusion Canonical Gentzen-Calculus: Semantics and Cut-Elimination

Ori Lahav

Abstract:

We define a general notion of a coherent canonical single-conclusion
sequent calculus, of which the usual systems for propositional
intuitionistic logic and minimal logic are special cases. We further
provide a general non-deterministic Kripke style semantics for calculi
of this sort.  Using this semantic, we prove general completeness and
strong cut elimination theorems for such calculi, as well as some
important corollaries. By this we extend to constructive logics
results that have previously been known for propositional logics that
can be characterized using multiple-conclusion sequent calculi (of
which classical logic is just one example).

Work of Arnon Avron and Ori Lahav