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.
|Keywords||No keywords specified (fix it)|
|Categories||categorize this paper)|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
Cut-Free Ordinary Sequent Calculi for Logics Having Generalized Finite-Valued Semantics.Arnon Avron, Jonathan Ben-Naim & Beata Konikowska - 2007 - Logica Universalis 1 (1):41-70.
Multi-Valued Calculi for Logics Based on Non-Determinism.Arnon Avron & Beata Konikowska - 2005 - Logic Journal of the IGPL 13 (4):365-387.
Subformula Semantics for Strong Negation Systems.Seiki Akama - 1990 - Journal of Philosophical Logic 19 (2):217 - 226.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Total downloads1 ( #876,000 of 2,164,554 )
Recent downloads (6 months)0
How can I increase my downloads?