Cut-Elimination and Quantification in Canonical Systems

Studia Logica 82 (1):157-176 (2006)
  Copy   BIBTEX


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.



    Upload a copy of this work     Papers currently archived: 91,252

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

Similar books and articles

Paraconsistency, paracompleteness, Gentzen systems, and trivalent semantics.Arnon Avron - 2014 - Journal of Applied Non-Classical Logics 24 (1-2):12-34.
Canonical signed calculi with multi-ary quantifiers.Anna Zamansky & Arnon Avron - 2012 - Annals of Pure and Applied Logic 163 (7):951-960.
Weak forms of elimination of imaginaries.Enrique Casanovas & Rafel Farré - 2004 - Mathematical Logic Quarterly 50 (2):126-140.
Subformula semantics for strong negation systems.Seiki Akama - 1990 - Journal of Philosophical Logic 19 (2):217 - 226.
The middle ground-ancestral logic.Liron Cohen & Arnon Avron - 2019 - Synthese 196 (7):2671-2693.
Sequent systems for compact bilinear logic.Wojciech Buszkowski - 2003 - Mathematical Logic Quarterly 49 (5):467.


Added to PP

249 (#77,871)

6 months
6 (#470,955)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Arnon Avron
Tel Aviv University

References found in this work

Mathematical logic.Joseph R. Shoenfield - 1967 - Reading, Mass.,: Addison-Wesley.
Structural Proof Theory.Sara Negri, Jan von Plato & Aarne Ranta - 2001 - New York: Cambridge University Press. Edited by Jan Von Plato.
Investigations into Logical Deduction.Gerhard Gentzen - 1964 - American Philosophical Quarterly 1 (4):288 - 306.
Investigations into Logical Deduction.Gerhard Gentzen, M. E. Szabo & Paul Bernays - 1970 - Journal of Symbolic Logic 35 (1):144-145.

View all 12 references / Add more references