Canonical signed calculi, non-deterministic matrices and cut-elimination

Abstract

Canonical propositional Gentzen-type calculi are a natural class of systems which in addition to the standard axioms and structural rules have only logical rules where exactly one occurrence of a connective is introduced and no other connective is mentioned. Cut-elimination in such systems is fully characterized by a syntactic constructive criterion of coherence. In this paper we extend the theory of canonical systems to the considerably more general class of signed calculi. We show that the extended criterion of coherence fully characterizes only analytic cutelimination in such calculi, while for characterizing strong and standard cut-elimination a stronger criterion of density is required. Modular semantics based on non-deterministic matrices are provided for every coherent canonical signed calculus. © Springer-Verlag Berlin Heidelberg 2009.