Abstract
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 cut-elimination 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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Avron, A.: Gentzen-Type Systems, Resolution and Tableaux. Journal of Automated Reasoning 10, 265–281 (1993)
Avron, A.,, Lev, I.: Non-deterministic Multi-valued Structures. Journal of Logic and Computation 15, 241–261 (2005)
Avron, A., Zamansky, A.: Generalized Non-deterministic matrices and (n,k)-ary quantifiers. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 26–41. Springer, Heidelberg (2007)
Avron, A., Zamansky, A.: Canonical calculi with (n,k)-ary quantifiers. Journal of Logical Methods in Computer Science (forthcming, 2008)
Baaz, M., Fermüller, C.G., Salzer, G., Zach, R.: Labeled Calculi and Finite-valued Logics. Studia Logica 61, 7–33 (1998)
Carnielli, W.A.: Systematization of Finite Many-valued Logics through the method of Tableaux. Journal of Symbolic Logic 52(2), 473–493 (1987)
Carnielli, W.A., Conglio, M.E.: Splitting Logics. In: Artemov,, Barringer,, Garcez,, Lamb (eds.) We Will Show Them!, Essays in Honour of Dov Gabbay, vol. 1, pp. 389–414. Woods College Publications (2005)
Ciabattoni, A., Terui, K.: Modular cut-elimination: Finding proofs or counter-examples. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 135–149. Springer, Heidelberg (2006)
Church, A.: A formulation of the simple theory of types. Journal of Symbolic Logic 5, 56–68 (1940)
Gentzen, G.: Investigations into Logical Deduction. In: Szabo, M.E. (ed.) The collected works of Gerhard Gentzen, pp. 68–131. North Holland, Amsterdam (1969)
Hähnle, R.: Commodious Axiomatization of Quantifiers in Many-valued Logic. Studia Logica 61, 101–121 (1998)
Henkin, L.: Some remarks on infinitely long formulas. In: Infinistic Methods, pp. 167–183. Pergamon Press, Oxford (1961)
Kalish, D., Montague, R.: Logic, Techniques. of Formal Reasoning. Brace and World, Inc., New York, Harcourt (1964)
Miller, D., Pimentel, E.: Using Linear logic to reason about sequent systems. In: Egly, U., Fermüller, C. (eds.) TABLEAUX 2002. LNCS (LNAI), vol. 2381, pp. 2–23. Springer, Heidelberg (2002)
Shroeder-Heister, P.: Natural deduction calculi with rules of higher levels. Journal of Symbolic Logic 50, 275–276 (1985)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, pp. 126–130. Cambridge University Press, Cambridge (2000)
Zamansky, A., Avron, A.: ‘Cut Elimination and Quantification in Canonical Systems’. Studia Logica 82(1), 157–176 (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avron, A., Zamansky, A. (2008). A Triple Correspondence in Canonical Calculi: Strong Cut-Elimination, Coherence, and Non-deterministic Semantics. In: Hirsch, E.A., Razborov, A.A., Semenov, A., Slissenko, A. (eds) Computer Science – Theory and Applications. CSR 2008. Lecture Notes in Computer Science, vol 5010. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-79709-8_9
Download citation
DOI: https://doi.org/10.1007/978-3-540-79709-8_9
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-79708-1
Online ISBN: 978-3-540-79709-8
eBook Packages: Computer ScienceComputer Science (R0)