Studia Logica 82 (1):157 - 176 (2006)
|Abstract||Canonical Propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules with the sub-formula 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. In this paper we considerably 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 prove that the following properties are equivalent for a canonical system G: (1) G admits Cut-Elimination, (2) G is coherent, and (3) G has a characteristic 2-valued non-deterministic matrix.|
|Keywords||No keywords specified (fix it)|
|Through your library||Configure|
Similar books and articles
Arnon Avron (2005). A Non-Deterministic View on Non-Classical Negations. Studia Logica 80 (2-3):159 - 194.
Grigori Mints (1997). Indexed Systems of Sequents and Cut-Elimination. Journal of Philosophical Logic 26 (6):671-696.
Seiki Akama (1990). Subformula Semantics for Strong Negation Systems. Journal of Philosophical Logic 19 (2):217 - 226.
J. W. Degen (1999). Complete Infinitary Type Logics. Studia Logica 63 (1):85-119.
Arnon Avron & Anna Zamansky, A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-Deterministic Semantics.
Sorry, there are not enough data points to plot this chart.
Added to index2009-01-28
Recent downloads (6 months)0
How can I increase my downloads?