Free Definite Description Theory – Sequent Calculi and Cut Elimination

Andrzej Indrzejczak

doi:10.12775/LLP.2020.020

Authors

Andrzej Indrzejczak University of Łódź, Department of Logic https://orcid.org/0000-0003-4063-1651

DOI:

https://doi.org/10.12775/LLP.2020.020

Keywords

sequent calculus, definite descriptions, free logic, definedness logic, partial terms, cut elimination

Abstract

We provide an application of a sequent calculus framework to the formalization of definite descriptions. It is a continuation of research undertaken in [20, 22]. In the present paper a so-called free description theory is examined in the context of different kinds of free logic, including systems applied in computer science and constructive mathematics for dealing with partial functions. It is shown that the same theory in different logics may be formalised by means of different rules and gives results of varying strength. For all presented calculi a constructive cut elimination is provided.

References

Avron, A., and I. Lev, “Canonical propositional Gentzen-type systems”, pages 529–543 in Proceedings of IJCAR’01, vol. 2083, LNCS, 2001. DOI: http://dx.doi.org/10.1007/3-540-45744-5-45

Baaz, M., and R. Iemhoff, “Gentzen calculi for the existence predicate”, Studia Logica 82, 1 (2006): 7–23. DOI: http://dx.doi.org/10.1007/s11225-006-6603-6

Beeson, M.. Foundations of Constructive Mathematics, Springer 1985. DOI: http://dx.doi.org/10.1007/978-3-642-68952-9

Bencivenga, E., “Free Logics”, pages 373–426 in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, vol. III, Reidel Publishing Company, Dordrecht, 1986. DOI: http://dx.doi.org/10.1007/978-94-009-5203-4-6

Bencivenga, E., K. Lambert, and B.C. van Fraasen, Logic, Bivalence and Denotation, Ridgeview, Atascadero, 1991.

Borkowski, L., and J. Słupecki, “A logical system based on rules and its applications in teaching mathematical logic”, Studia Logica 7 (1958): 71–113. DOI: http://dx.doi.org/10.1007/BF02548936

Bostock, D., Intermediate Logic, Clarendon Press, Oxford 1997.

Carlström, J., “Interpreting descriptions in intensional type theory”, The Journal of Symbolic Logic 70, 2 (2005): 488–514. DOI: http://dx.doi.org/10.2178/jsl/1120224725

Ciabattoni, A., “Automated generation of analytic calculi for logics with linearity”, pages 503–517 in Proceedings of CSL’04, vol. 3210, LNCS, 2004. DOI: http://dx.doi.org/10.1007/978-3-540-30124-0-38

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 (2010): 369–389. DOI: http://dx.doi.org/10.1016/j.fss.2009.09.001

Czermak, J., “A logical calculus with descriptions”, Journal of Philosophical Logic 3 (1974): 211–228. DOI: http://dx.doi.org/10.1007/BF00247223

Feferman, S., “Definedness”, Erkenntnis 43 (1995): 295–320. DOI: http://dx.doi.org/10.1007/BF01135376

Fitting, M., and R.L. Mendelsohn, First-Order Modal Logic, Kluwer, Dordrecht, 1998. DOI: http://dx.doi.org/10.1007/978-94-011-5292-1

Francez, N., and B. Więckowski, “A proof-theoretic semantics for contextual definiteness”, in: E. Moriconi and L. Tesconi (eds.), Second Pisa Colloquium in Logic, Language and Epistemology, ETS, Pisa, 2014.

Garson, J.W., Modal Logic for Philosophers, Cambridge University Press, Cambridge, 2006. DOI: http://dx.doi.org/10.1017/CBO9780511617737

Goldblatt, R., Quantifiers, Propositions and Identity, Cambridge University Press, Cambridge 2011. DOI: http://dx.doi.org/10.1017/CBO9780511862359

Gratzl, N., “Incomplete symbols –definite descriptions revisited”, Journal of Philosophical Logic 44 (2015): 489–506. DOI: http://dx.doi.org/10.1007/s10992-014-9339-1

Gumb, R., “An extended joint consistency theorem for a nonconstructive logic of partial terms with definite descriptions”, Studia Logica 69, 2 (2001): 279–292. DOI: http://dx.doi.org/10.1023/A:1013822008159

Indrzejczak, A., “Eliminability of cut in hypersequent calculi for some modal logics of linear frames”, Information Processing Letters 115, 2 (2015): 75–81. DOI: http://dx.doi.org/10.1016/j.ipl.2014.07.002

Indrzejczak, A., “Cut-free modal theory of definite descriptions”, pages 387–406 in G. Bezhanishvili et al. (eds.), Advances in Modal Logic 12, College Publications, 2018.

Indrzejczak, A., “Rule-generation theorem and its applications”, Bulletin of the Section of Logic 47, 4 (2018): 265–281. DOI: http://dx.doi.org/10.18778/0138-0680.47.4.03

Indrzejczak, A., “Fregean description theory in proof-theoretical setting”, Logic and Logical Philosophy 28, 1 (2019): 137–155. DOI: http://dx.doi.org/10.12775/LLP.2018.008

Indrzejczak, A., “Cut elimination in hypersequent calculus for some logics of linear time”, Review of Symbolic Logic 12, 4 (2019): 806–822. DOI: http://dx.doi.org/10.1017/S1755020319000352

Indrzejczak, A., “Existence, definedness and definite descriptions in hybrid modal logic”, pages 349–368 in N. Olivetti et al. (eds.), Advances in Modal Logic 13, College Publications, 2020.

Indrzejczak, A., “Free logics are cut-free’, to appear in Studia Logica. DOI: http://dx.doi.org/10.1007/s11225-020-09929-8

Kalish, D., and R. Montague, “Remarks on descriptions and natural deduction”, Archiv. für Mathematische Logik und Grundlagen Forschung 3 (1957): 50–64, 65–73.

Kalish, D., R. Montague and G. Mar, Logic. Techniques of Formal Reasoning (2nd edition), New York, Oxford: Oxford University Press, 1980.

Kurokawa, H., “Hypersequent calculi for modal logics extending S4”, pages 51–68 in New Frontiers in Artificial Intelligence (2013), Springer, 2014. DOI: http://dx.doi.org/10.1007/978-3-319-10061-6-4

Kürbis, N., “A binary quantifier for definite descriptions in intuitionist negative free logic: Natural deduction and normalization’, Bulletin of the Section of Logic 48, 2 (2019): 81–97. DOI: http://dx.doi.org/10.18778/0138-0680.48.2.01

Kürbis, N., “Two treatments of definite descriptions in intuitionistnegative free logic”, Bulletin of the Section of Logic 48, 4 (2019): 299–317. DOI: http://dx.doi.org/10.18778/0138-0680.48.4.04

Lambert, K., “A theory of definite descriptions”, pages 17–27 in K. Lambert (ed.), Philosophical Applications of Free Logic, Kluwer, 1962.

Lambert, K., “Free logic and definite descriptions”, pages 37–48 in K. Lambert (ed.), New Essays in Free Logic, Springer, 2001. DOI: http://dx.doi.org/10.1007/978-94-015-9761-6-2

Lehmann, S., “More free logic”, pages 197–259 in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic, second edition, vol. V, Springer, 2002. DOI: http://dx.doi.org/10.1007/978-94-017-0458-8-4

Maffezioli, P., and E. Orlandelli, “Full cut elimination and interpolation for intuitionistic logic with existence predicate”, Bulletin of the Section of Logic 48, 2 (2019): 137–158. DOI: http://dx.doi.org/10.18778/0138-0680.48.2.04

Metcalfe, G., N. Olivetti and D. Gabbay, Proof Theory for Fuzzy Logics, Springer, 2008. DOI: http://dx.doi.org/10.1007/978-1-4020-9409-5

Negri, S., and J. von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001. DOI: http://dx.doi.org/10.1017/CBO9780511527340

Pavlović, E., and N. Gratzl, “A more unified approach to free logics”, to appear in Journal of Philosophical Logic, online (2020): 1–32. DOI: http://dx.doi.org/10.1007/s10992-020-09564-7

Pelletier, F.J., and B. Linsky, “What is Frege’s theory of descriptions?”, pages 195–250 in B. Linsky and G. Imaguire (eds.), On Denoting: 1905–2005, Munich: Philosophia Verlag, 2005.

Scott, D., “Identity and existence in intuitionistic logic”, pages 660–696 in M. Fourman, C. Mulvey and D. Scott (eds.), Applications of Sheaves, Springer, 1979. DOI: http://dx.doi.org/10.1007/BFb0061839

Smiley, T., Lecture Notes in Mathematical Logic, Cambridge University Press, 1970.

Stenlund, S., The Logic of Description and Existence, Filosofiska Studier no 18, Uppsala, 1973.

Stenlund, S., “Descriptions in intuitionistic logic”, pages 197–212 in S. Kanger (ed.), Proceedings of the Third Scandinavian Logic Symposium, 1975. DOI: http://dx.doi.org/10.1016/S0049-237X(08)70732-8

Tennant, N., Natural Logic, Edinbourgh University Press, 1978.

Tennant, N., “A general theory of abstraction operators”, The Philosophical Quaterly 54, 214 (2004): 105–133. DOI: http://dx.doi.org/10.1111/j.0031-8094.2004.00344.x

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, 2000. DOI: http://dx.doi.org/10.1017/CBO9781139168717

Wansing, H., Displaying Modal Logics, Kluwer Academic Publishers, Dordrecht, 1999. DOI: http://dx.doi.org/10.1007/978-94-017-1280-4