Canonical Calculi: Invertibility, Axiom Expansion and (Non)-determinism

We apply the semantic tool of non-deterministic matrices to characterize two important properties of canonical Gentzen-type calculi: invertibility of rules and axiom expansion. We show that in every canonical calculus G satisfying a natural condition, the following are equivalent: (i) the connectives of G admit axiom expansion, (ii) the rules of G are invertible, and (iii) G has a characteristic finite deterministic matrix.

• Type: Conference
• Year: 2009
• Where: CSR
• Authors: Arnon Avron, Agata Ciabattoni, Anna Zamansky
• Keywords: Axiom Expansion, Canonical Gentzen-type Calculi, CSR 2009, Non-deterministic Matrices, Theoretical Computer Science