General Canonical Gentzen-Type Systems

We construct a general framework for fully-structural, standard
propositional Gentzen-type systems.  The framework is based on a very
general notion of a canonical sequential rule, and allows a unified
treatment of diversity of logics. The logics that fall under it
include classical, intuitionistic, dual intuitionistic, and
bi-intuitionistic logics, the modal logics $S4$ and $S5$, as well as
possible combinations of all these logics. We present a general method
for providing an effective non-deterministic Kripke-style semantics
for any system that can be represented within this framework, and
prove a corresponding general soundness and completeness theorem.
This semantics is then used for identifying the systems in our
framework that admit strong cut-elimination, as well as those which
admit only strong analytic cut-elimination.

(Joint work with Arnon Avron.)