Abstract
We define the notions of a canonical inference rule and a canonical constructive system in the framework of strict single-conclusion Gentzen-type systems (or, equivalently, natural deduction systems), and develop a corresponding general non-deterministic Kripke-style semantics. We show that every strict constructive canonical system induces a class of non-deterministic Kripke-style frames, for which it is strongly sound and complete. This non-deterministic semantics is used for proving a strong form of the cut-elimination theorem for such systems, and for providing a decision procedure for them. These results identify a large family of basic constructive connectives, including the standard intuitionistic connectives, together with many other independent connectives.
This research was supported by The Israel Science Foundation (grant no. 809-06).
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Avron, A.: Simple Consequence Relations. Information and Computation 92, 105–139 (1991)
Avron, A.: Gentzen-Type Systems, Resolution and Tableaux. Journal of Automated Reasoning 10, 265–281 (1993)
Avron, A.: Nondeterministic View on Nonclassical Negations. Studia Logica 80, 159–194 (2005)
Avron, A.: Non-deterministic Semantics for Families of Paraconsistent Logics. In: Beziau, J.-Y., Carnielli, W., Gabbay, D.M. (eds.) Handbook of Paraconsistency. Studies in Logic, vol. 9, pp. 285–320. College Publications (2007)
Avron, A., Lahav, O.: Canonical constructive systems. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS, vol. 5607, pp. 62–76. Springer, Heidelberg (2009)
Avron, A., Lev, I.: Canonical Propositional Gentzen-Type Systems. In: Goré, R.P., Leitsch, A., Nipkow, T. (eds.) IJCAR 2001. LNCS (LNAI), vol. 2083, pp. 529–544. Springer, Heidelberg (2001)
Avron, A., Lev, I.: Non-deterministic Multiple-valued Structures. Journal of Logic and Computation 15, 24–261 (2005)
Belnap, N.D.: Tonk, Plonk and Plink. Analysis 22, 130–134 (1962)
Bowen, K.A.: An extension of the intuitionistic propositional calculus. Indagationes Mathematicae 33, 287–294 (1971)
Ciabattoni, A., Terui, K.: Towards a Semantic Characterization of Cut-Elimination. Studia Logica 82, 95–119 (2006)
Fernandez, D.: Non-deterministic Semantics for Dynamic Topological Logic. Annals of Pure and Applied Logic 157, 110–121 (2009)
Gentzen, G.: Investigations into Logical Deduction. In: Szabo, M.E. (ed.) The Collected Works of Gerhard Gentzen, pp. 68–131. North Holland, Amsterdam (1969)
Gurevich, Y., Neeman, I.: The Logic of Infons, Microsoft Research Tech. Report MSR-TR-2009-10 (January 2009)
Kripke, S.: Semantical Analysis of Intuitionistic Logic I. In: Crossly, J., Dummett, M. (eds.) Formal Systems and Recursive Functions, pp. 92–129. North-Holland, Amsterdam (1965)
Prior, A.N.: The Runabout Inference Ticket. Analysis 21, 38–39 (1960)
Sundholm, G.: Proof theory and Meaning. In: Gabbay, D.M., Guenthner, F. (eds.) Handbook of Philosophical Logic, vol. 9, pp. 165–198 (2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Avron, A., Lahav, O. (2010). Strict Canonical Constructive Systems. In: Blass, A., Dershowitz, N., Reisig, W. (eds) Fields of Logic and Computation. Lecture Notes in Computer Science, vol 6300. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15025-8_4
Download citation
DOI: https://doi.org/10.1007/978-3-642-15025-8_4
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-15024-1
Online ISBN: 978-3-642-15025-8
eBook Packages: Computer ScienceComputer Science (R0)