Sciweavers

Share
CSR
2008
Springer

A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-deterministic Semantics

9 years 1 months ago
A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-deterministic Semantics
An (n, k)-ary quantifier is a generalized logical connective, binding k variables and connecting n formulas. Canonical systems with (n, k)-ary quantifiers form a natural class of Gentzen-type systems which in addition to the standard axioms and structural rules have only logical rules in which exactly one occurrence of a quantifier is introduced. The semantics for these systems is provided using two-valued non-deterministic matrices, a generalization of the classical matrix. In this paper we use a constructive syntactic criterion of coherence to characterize strong cutelimination in such systems. We show that the following properties of a canonical system G with arbitrary (n, k)-ary quantifiers are equivalent: (i) G is coherent, (ii) G admits strong cut-elimination, and (iii) G has a strongly characteristic two-valued generalized non-deterministic matrix.
Arnon Avron, Anna Zamansky
Added 10 Dec 2010
Updated 10 Dec 2010
Type Journal
Year 2008
Where CSR
Authors Arnon Avron, Anna Zamansky
Comments (0)
books