Canonical Signed Calculi, Non-deterministic Matrices and Cut-Elimination

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.

• Type: Conference
• Year: 2009
• Where: LFCS
• Authors: Arnon Avron, Anna Zamansky
• Keywords: Artificial Intelligence, Canonical, LFCS 2009, Propositional Gentzen-type Calculi, Syntactic Constructive Criterion