Abstract
Canonical propositional Gentzen-type systems are systems which in addition to the standard axioms and structural rules have only pure logical rules which have the subformula property, introduce exactly one occurrence of a connective in their conclusion, and no other occurrence of any connective is mentioned anywhere else in their formulation. We provide a constructive coherence criterion for the non-triviality of such systems, and show that a system of this kind admits cut elimination iff it is coherent. We show also that the semantics of such systems is provided by non-deterministic two-valued matrices (2-Nmatrices). 2-Nmatrices form a natural generalization of the classical two-valued matrix, and every coherent canonical system is sound and complete for one of them. Conversely, with any 2-Nmatrix it is possible to associate a coherent canonical Gentzen-type system which has for each connective at most one introduction rule for each side, and is sound and complete for that 2-Nmatrix. We show also that every coherent canonical Gentzen-type system either defines a fragment of the classical two-valued logic, or a logic which has no finite characteristic matrix.
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.
References
Arnon Avron and Iddo Lev, “Non-deterministic matrices,” 2000. Submitted.
Arnon Avron, “Simple consequence relations,” Information and Computation, vol. 92, no. 1, pp. 105–139, 1991.
Nuel. D. Belnap, “Tonk, plonk and plink,” Analysis, vol. 22, pp. 130–134, 1962.
Jean-Yves Béziau, “Classical negation can be expressed by one of its halves,” Logic Journal of the IGPL, vol. 7, pp. 145–151, 1999.
Matthias Baaz, Christian G. FermÜller, and Gernot Salzer, “Automated deduction for many-valued logics,” in Handbook of Automated Reasoning (A. Robinson and A. Voronkov, eds.), Elsevier Science Publishers, 2000.
Matthias Baaz, Christian G. FermÜller, and Richard Zach, “Elimination of cuts in first-oder finite-valued logics,” Information Processing Cybernetics, vol. 29, no. 6, pp. 333–355, 1994.
J. Michael Dunn, “Relevance logic and entailment,” in [GG86], vol. III, ch. 3, pp. 117–224, 1986.
Gerhard Gentzen, “Investigations into logical deduction,” in The Collected Works of Gerhard Gentzen (M. E. Szabo, ed.), pp. 68–131, North Holland, Amsterdam, 1969.
Dov M. Gabbay and Franz Guenthner, Handbook of Philosophical Logic. D. Reidel Publishing company, 1986.
Reiner Hähnle, “Tableaux for multiple-valued logics,”in Handbook of Tableau Methods (Marcello D‘ Agostino, Dov M. Gabbay, Reiner Hähnle, and Joachim Posegga, eds.), pp. 529–580, Kluwer Publishing Company, 1999.
Wilfrid Hodges, “Elementary predicate logic,” in [GG86], vol. I, ch. 1, pp. 1–131, 1986.
A. N. Prior, “The runabout inference ticket,” Analysis, vol. 21, pp. 38-9, 1960.
Dana S. Scott, “Completeness and axiomatization in many-valued logics,” in Proc. of the Tarski symposium, vol. XXV of Proc. of Symposia in Pure Mathematics, (Rhode Island), pp. 411–435, American Mathematical Society, 1974.
Göran Sundholm, “Proof theory and meaning,” in [GG86], vol. III, ch. 8, pp. 471–506, 1986.
Alasdair Urquhart, “Many-valued logic,” in [GG86], vol. III, ch. 2, pp. 71–116, 1986.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Avron, A., Lev, I. (2001). Canonical Propositional Gentzen-Type Systems. In: Goré, R., Leitsch, A., Nipkow, T. (eds) Automated Reasoning. IJCAR 2001. Lecture Notes in Computer Science, vol 2083. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-45744-5_45
Download citation
DOI: https://doi.org/10.1007/3-540-45744-5_45
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42254-9
Online ISBN: 978-3-540-45744-2
eBook Packages: Springer Book Archive