Abstract
The aim of this work is to perform a proof-theoretical investigation of some propositional logics underlying either finite-valued Gödel logic or finite-valued Łukasiewicz logic. We define cut-free hypersequent calculi for logics obtained by adding either the n-contraction law or the n-weak law of excluded middle to afine intuitionistic linear logic with the linearity axiom (A → B) ⋁ (B → A). We also develop cut-free calculi for the classical counterparts of these logics. Moreover we define a hypersequent calculus for Ł3⋂ Ł4 in which the cut-elimination theorem holds. This calculus allows to define an alternative axiomatization of Ł4 making no use of the Lukasiewicz axiom.
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
A. Avron. A constructive analysis of RM. J. of Symbolic Logic, vol. 52. pp. 939–951. 1987.
A. Avron. Natural 3-valued Logics. Characterization and Proof Theory. J. of Symbolic Logic, vol. 56. pp. 276–294. 1991.
A. Avron. Hypersequents, Logical Consequence and Intermediate Logics for Concurrency. Annals of Mathematics and Artificial Intelligence, vol. 4. pp. 225–248. 1991.
A. Avron. The Method of Hypersequents in the Proof Theory of Propositional Nonclassical Logics. In: Logic: from Foundations to Applications. W. Hodges, M. Hyland, C. Steinhorn and J. Truss Eds., European Logic Colloquium. Oxford Science Publications. Clarendon Press. Oxford. pp. 1–32. 1996.
A. Avron. Two Types of Multiple-Conclusion Systems. Logic Journal of the IGPL, vol. 6(5). pp. 695–717. 1998.
M. Baaz, A. Ciabattoni, C.G. Fermüller, H. Veith. Proof Theory of Fuzzy Logics: Urquhart’s C and Related Logics. Prooceedings of MFCS’98. Lectures Notes in Computer Science. vol.1450. pp.203–212. 1998.
A. Ciabattoni, D.M. Gabbay, N. Olivetti. Cut-free Proof Systems for Logics of Weak Excluded Middle. Soft Computing. vol. 2(4). To appear. 1998.
R. Cignoli, D. Mundici, I.M.L. D’Ottaviano. Algebraic foundations of many-valued reasoning. In preparation.
J.Y. Girard. Linear Logic. Theoretical Comp. Science, vol. 50. pp. 1–102. 1987.
R. Grigolia. Algebraic analysis of Łukasiewicz-Tarski n-valued logical systems. In Selected Papers on Łukasiewicz Sentential Calculi. R. Wòjciki and G. Malinowski Ed., Polish Acad. of Sciences, Ossolineum, Wrocław. pp. 81–91. 1977.
P. Hájek. Metamathematics of fuzzy logic. Kluwer. 1998.
U. Höhle. Commutative, residuated l-monoids. In: Nonclassical logics and their applications to fuzzy subsets. U. Höhle and P. Klement Eds., Kluwer. Dordrecht. pp. 53–106. 1995.
R. Hori, H. Ono, H. Schellinx. Extending Intuitionistic Linear Logic with Knotted Structural Rules. Notre Dame Journal of Formal Logic. vol. 35(2). pp. 219–242. 1994.
H. Ono. Logics without contraction rule and residuated lattices. Draft. 1997.
H. Ono, Y. Komori. Logics without the contraction rule. J. of Symbolic Logic, vol. 50. pp.169–201. 1985.
A. Prijatelj. Bounded Contraction and Gentzen style Formulation of Łukasiewicz Logics. Studia Logica, vol. 57. pp. 437–456. 1996.
A. Prijatelj. Connectification for n-contraction. Studia Logica, vol. 54(2). pp. 149–171. 1995.
A.S. Troelstra. Lectures on Linear Logic. CSLI Lectures Notes n.29. 1991.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Ciabattoni, A. (1999). Bounded Contraction in Systems with Linearity. In: Murray, N.V. (eds) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 1999. Lecture Notes in Computer Science(), vol 1617. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48754-9_13
Download citation
DOI: https://doi.org/10.1007/3-540-48754-9_13
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66086-6
Online ISBN: 978-3-540-48754-8
eBook Packages: Springer Book Archive