Abstract
The paper presents a uniform proof-theoretic treatment of several kinds of free logic, including the logics of existence and definedness applied in constructive mathematics and computer science, and called here quasi-free logics. All free and quasi-free logics considered are formalised in the framework of sequent calculus, the latter for the first time. It is shown that in all cases remarkable simplifications of the starting systems are possible due to the special rule dealing with identity and existence predicate. Cut elimination is proved in a constructive way for sequent calculi adequate for all logics under consideration.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
References
Baaz, M., and R. Iemhoff, Gentzen Calculi for the existence predicate Studia Logica 82(1):7–23, 2006.
Beeson, M., Foundations of Constructive Mathematics, Springer, Berlin, 1985
Bencivenga, E., Free Logics, in D. Gabbay, and F. Guenthner, (eds.), Handbook of Philosophical Logic, Vol. III, Reidel Publishing Company, Dordrecht, 1986, pp. 373–426.
Bencivenga, E., K. Lambert, and B. C. van Fraassen, Logic, Bivalence and Denotation, Ridgeview, Atascadero, 1991.
Ciabattoni, A., G. Metcalfe, and F. Montagna, Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions, Fuzzy Sets and Systems 161(3):369–389, 2010.
Feferman, S., Definedness, Erkenntnis 43:295–320, 1995.
Fitting, M., and R. L. Mendelsohn, First-Order Modal Logic, Kluwer, Dordrecht 1998.
Garson, J.W., Modal Logic for Philosophers, Cambridge University Press, Cambridge 2006.
Gratzl, N., A sequent calculus for a negative free logic, Studia Logica 96:331–348, 2010.
Gumb, R., An extended joint consistency theorem for a nonconstructive logic of partial terms with definite descriptions, Studia Logica 69(2):279–292, 2001.
Indrzejczak, A., Eliminability of cut in hypersequent calculi for some modal logics of linear frames, Information Processing Letters 115/2:75–81, 2015.
Indrzejczak, A., Cut-Free Modal Theory of Definite Descriptions, in G. Bezhanishvili, G. D’Agostino, G. Metcalfe, and T. Studer, (eds.), Advances in Modal Logic 12, College Publications, 2018, pp. 387–406.
Indrzejczak, A., Rule-generation theorem and its applications, Bulletin of the Section of Logic 47(4):265–281, 2018.
Indrzejczak, A., Cut elimination in hypersequent calculus for some logics of linear time, Review of Symbolic Logic 12(4):806–822, 2019.
Indrzejczak, A., Existence, Definedness and Definite Descriptions in Hybrid Modal Logic, in N. Olivetti, R. Verbrugge, and S. Negri, (eds.), Advances in Modal Logic 13, College Publications, 2020, pp. 349–368.
Jaśkowski, S., On the rules of suppositions in formal logic, Studia Logica 1:5–32, 1934.
Kurokawa, H., Hypersequent calculi for modal logics extending S4, in Y. Nakano, K. Satoh, and D. Bekki, (eds.), New Frontiers in Artificial Intelligence, Springer, 2014, pp. 51–68.
Lehmann, S., More Free Logic, in D. Gabbay, and F. Guenthner, (eds.), Handbook of Philosophical Logic, Vol V, 2nd edition, Springer, 2002, pp. 197–259.
Maffezioli, P., and E. Orlandelli, Full cut elimination and interpolation for intuitionistic logic with existence predicate, Bulletin of the Section of Logic 48(2):137–158, 2019.
Metcalfe, G., N. Olivetti, and D. Gabbay, Proof Theory for Fuzzy Logics, Springer, Berlin, 2008.
Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001.
Negri, S., and J. von Plato, Proof Analysis, Cambridge University Press, Cambridge, 2011.
Pavlović, E., and N. Gratzl, A more unified approach to free logics, to appear in Journal of Philosophical Logic. https://doi.org/10.1007/s10992-020-09564-7.
Priest, G., An Introduction to Non-classical Logic, Cambridge University Press, Cambridge, 2001.
Scott, D., Identity and Existence in Intuitionistic Logic, in M. Fourman, C. Mulvey, and D. Scott, (eds.), Applications of Sheaves, Springer, 1979, pp. 660–696.
Takeuti, G., Proof Theory, North-Holland, Amsterdam, 1987.
Tennant, N., Natural Logic, Edinburgh University Press, 1978.
Trew, A., Nonstandard theories of quantification and identity, Journal of Symbolic Logic 35:267–294, 1970.
Troelstra, A. S., and D. van Dalen, Constructivism in Mathematics, vol. I, North-Holland, 1988.
Troelstra, A. S., and H. Schwichtenberg Basic Proof Theory, Oxford University Press, Oxford, 1996.
Acknowledgements
I am greatly indebted to both reviewers for many useful comments and for drawing my attention to the fresh work of Pavlović and Gratzl [23]. It helped to improve the text and clarify some issues not sufficiently emphasized in the former version. The research is supported by the National Science Centre, Poland (grant number: DEC-2017/25/B/HS1/01268).
Author information
Authors and Affiliations
Corresponding author
Additional information
Publisher's Note
Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.
Presented by Jacek Malinowski
Rights and permissions
Open Access This article is licensed under a Creative Commons Attribution 4.0 International License, which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons licence, and indicate if changes were made. The images or other third party material in this article are included in the article’s Creative Commons licence, unless indicated otherwise in a credit line to the material. If material is not included in the article’s Creative Commons licence and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder. To view a copy of this licence, visit http://creativecommons.org/licenses/by/4.0/.
About this article
Cite this article
Indrzejczak, A. Free Logics are Cut-Free. Stud Logica 109, 859–886 (2021). https://doi.org/10.1007/s11225-020-09929-8
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s11225-020-09929-8