Nmatrices, Canonical Systems and Quantification

Anna Zamansky

Canonical propositional Gentzen-type systems are systems which in
addition to the standard axioms and structural rules have only pure
logical rules with the subformula property, in which exactly one
occurrence of a connective is introduced in the conclusion, and no
other occurrence of any connective is mentioned anywhere else. We
generalize the notion of a ``canonical system'' to first-order
languages and beyond. We extend the propositional coherence criterion
for the non-triviality of such systems to rules with unary quantifiers
and show that it remains constructive. Then we provide semantics for
such canonical systems using 2-valued non-deterministic matrices
extended to languages with quantifiers, and show that like in the
propositional case, there exists a deep connection between the
possibility to eliminate cuts in a canonical system G, and the
existence of a 2-valued non-deterministic characteristic matrix for G.