{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T14:37:25Z","timestamp":1753886245224,"version":"3.37.3"},"reference-count":30,"publisher":"Springer Science and Business Media LLC","issue":"4","license":[{"start":{"date-parts":[[2021,1,13]],"date-time":"2021-01-13T00:00:00Z","timestamp":1610496000000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"},{"start":{"date-parts":[[2021,1,13]],"date-time":"2021-01-13T00:00:00Z","timestamp":1610496000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0"}],"funder":[{"DOI":"10.13039\/501100004281","name":"Narodowe Centrum Nauki","doi-asserted-by":"publisher","award":["DEC-2017\/25\/B\/HS1\/01268"],"award-info":[{"award-number":["DEC-2017\/25\/B\/HS1\/01268"]}],"id":[{"id":"10.13039\/501100004281","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Stud Logica"],"published-print":{"date-parts":[[2021,8]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.1007\/s11225-020-09929-8","type":"journal-article","created":{"date-parts":[[2021,1,14]],"date-time":"2021-01-14T05:45:13Z","timestamp":1610603113000},"page":"859-886","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":9,"title":["Free Logics are Cut-Free"],"prefix":"10.1007","volume":"109","author":[{"ORCID":"https:\/\/orcid.org\/0000-0003-4063-1651","authenticated-orcid":false,"given":"Andrzej","family":"Indrzejczak","sequence":"first","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2021,1,13]]},"reference":[{"issue":"1","key":"9929_CR1","doi-asserted-by":"publisher","first-page":"7","DOI":"10.1007\/s11225-006-6603-6","volume":"82","author":"M Baaz","year":"2006","unstructured":"Baaz, M., and R. Iemhoff, Gentzen Calculi for the existence predicate Studia Logica 82(1):7\u201323, 2006.","journal-title":"Studia Logica"},{"key":"9929_CR2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-68952-9","volume-title":"Foundations of Constructive Mathematics","author":"M Beeson","year":"1985","unstructured":"Beeson, M., Foundations of Constructive Mathematics, Springer, Berlin, 1985"},{"key":"9929_CR3","doi-asserted-by":"publisher","first-page":"373","DOI":"10.1007\/978-94-009-5203-4_6","volume-title":"Handbook of Philosophical Logic","author":"E Bencivenga","year":"1986","unstructured":"Bencivenga,\u00a0E., Free Logics, in D. Gabbay, and F. Guenthner, (eds.), Handbook of Philosophical Logic, Vol. III, Reidel Publishing Company, Dordrecht, 1986, pp. 373\u2013426."},{"key":"9929_CR4","unstructured":"Bencivenga,\u00a0E., K. Lambert, and B. C. van Fraassen, Logic, Bivalence and Denotation, Ridgeview, Atascadero, 1991."},{"key":"9929_CR5","doi-asserted-by":"crossref","unstructured":"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\u2013389, 2010.","DOI":"10.1016\/j.fss.2009.09.001"},{"key":"9929_CR6","doi-asserted-by":"publisher","first-page":"295","DOI":"10.1007\/BF01135376","volume":"43","author":"S Feferman","year":"1995","unstructured":"Feferman, S., Definedness, Erkenntnis 43:295\u2013320, 1995.","journal-title":"Erkenntnis"},{"key":"9929_CR7","doi-asserted-by":"crossref","unstructured":"Fitting,\u00a0M., and R. L. Mendelsohn, First-Order Modal Logic, Kluwer, Dordrecht 1998.","DOI":"10.1007\/978-94-011-5292-1"},{"key":"9929_CR8","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511617737","volume-title":"Modal Logic for Philosophers","author":"JW Garson","year":"2006","unstructured":"Garson,\u00a0J.W., Modal Logic for Philosophers, Cambridge University Press, Cambridge 2006."},{"key":"9929_CR9","doi-asserted-by":"publisher","first-page":"331","DOI":"10.1007\/s11225-010-9293-z","volume":"96","author":"N Gratzl","year":"2010","unstructured":"Gratzl, N., A sequent calculus for a negative free logic, Studia Logica 96:331\u2013348, 2010.","journal-title":"Studia Logica"},{"issue":"2","key":"9929_CR10","doi-asserted-by":"publisher","first-page":"279","DOI":"10.1023\/A:1013822008159","volume":"69","author":"R Gumb","year":"2001","unstructured":"Gumb, R., An extended joint consistency theorem for a nonconstructive logic of partial terms with definite descriptions, Studia Logica 69(2):279\u2013292, 2001.","journal-title":"Studia Logica"},{"issue":"2","key":"9929_CR11","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.ipl.2014.07.002","volume":"115","author":"A Indrzejczak","year":"2015","unstructured":"Indrzejczak,\u00a0A., Eliminability of cut in hypersequent calculi for some modal logics of linear frames, Information Processing Letters 115\/2:75\u201381, 2015.","journal-title":"Information Processing Letters"},{"key":"9929_CR12","unstructured":"Indrzejczak, A., Cut-Free Modal Theory of Definite Descriptions, in G. Bezhanishvili, G. D\u2019Agostino, G. Metcalfe, and T. Studer, (eds.), Advances in Modal Logic 12, College Publications, 2018, pp. 387\u2013406."},{"issue":"4","key":"9929_CR13","doi-asserted-by":"publisher","first-page":"265","DOI":"10.18778\/0138-0680.47.4.03","volume":"47","author":"A Indrzejczak","year":"2018","unstructured":"Indrzejczak, A., Rule-generation theorem and its applications, Bulletin of the Section of Logic 47(4):265\u2013281, 2018.","journal-title":"Bulletin of the Section of Logic"},{"issue":"4","key":"9929_CR14","doi-asserted-by":"publisher","first-page":"806","DOI":"10.1017\/S1755020319000352","volume":"12","author":"A Indrzejczak","year":"2019","unstructured":"Indrzejczak, A., Cut elimination in hypersequent calculus for some logics of linear time, Review of Symbolic Logic 12(4):806\u2013822, 2019.","journal-title":"Review of Symbolic Logic"},{"key":"9929_CR15","unstructured":"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\u2013368."},{"key":"9929_CR16","first-page":"5","volume":"1","author":"S Ja\u015bkowski","year":"1934","unstructured":"Ja\u015bkowski,\u00a0S., On the rules of suppositions in formal logic, Studia Logica 1:5\u201332, 1934.","journal-title":"Studia Logica"},{"key":"9929_CR17","doi-asserted-by":"crossref","unstructured":"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\u201368.","DOI":"10.1007\/978-3-319-10061-6_4"},{"key":"9929_CR18","doi-asserted-by":"crossref","unstructured":"Lehmann, S., More Free Logic, in D. Gabbay, and F. Guenthner, (eds.), Handbook of Philosophical Logic, Vol V, 2nd edition, Springer, 2002, pp. 197\u2013259.","DOI":"10.1007\/978-94-017-0458-8_4"},{"issue":"2","key":"9929_CR19","doi-asserted-by":"publisher","first-page":"137","DOI":"10.18778\/0138-0680.48.2.04","volume":"48","author":"P Maffezioli","year":"2019","unstructured":"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\u2013158, 2019.","journal-title":"Bulletin of the Section of Logic"},{"key":"9929_CR20","volume-title":"Proof Theory for Fuzzy Logics","author":"G Metcalfe","year":"2008","unstructured":"Metcalfe, G., N. Olivetti, and D. Gabbay, Proof Theory for Fuzzy Logics, Springer, Berlin, 2008."},{"key":"9929_CR21","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511527340","volume-title":"Structural Proof Theory","author":"S Negri","year":"2001","unstructured":"Negri,\u00a0S., and J.\u00a0von Plato, Structural Proof Theory, Cambridge University Press, Cambridge, 2001."},{"key":"9929_CR22","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139003513","volume-title":"Proof Analysis","author":"S Negri","year":"2011","unstructured":"Negri,\u00a0S., and J.\u00a0von Plato, Proof Analysis, Cambridge University Press, Cambridge, 2011."},{"key":"9929_CR23","doi-asserted-by":"publisher","unstructured":"Pavlovi\u0107, 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.","DOI":"10.1007\/s10992-020-09564-7"},{"key":"9929_CR24","volume-title":"An Introduction to Non-classical Logic","author":"G Priest","year":"2001","unstructured":"Priest,\u00a0G., An Introduction to Non-classical Logic, Cambridge University Press, Cambridge, 2001."},{"key":"9929_CR25","doi-asserted-by":"crossref","unstructured":"Scott, D., Identity and Existence in Intuitionistic Logic, in M. Fourman, C. Mulvey, and D. Scott, (eds.), Applications of Sheaves, Springer, 1979, pp. 660\u2013696.","DOI":"10.1007\/BFb0061839"},{"key":"9929_CR26","volume-title":"Proof Theory","author":"G Takeuti","year":"1987","unstructured":"Takeuti, G., Proof Theory, North-Holland, Amsterdam, 1987."},{"key":"9929_CR27","unstructured":"Tennant, N., Natural Logic, Edinburgh University Press, 1978."},{"key":"9929_CR28","doi-asserted-by":"publisher","first-page":"267","DOI":"10.2307\/2270518","volume":"35","author":"A Trew","year":"1970","unstructured":"Trew, A., Nonstandard theories of quantification and identity, Journal of Symbolic Logic 35:267\u2013294, 1970.","journal-title":"Journal of Symbolic Logic"},{"key":"9929_CR29","unstructured":"Troelstra, A. S., and D. van Dalen, Constructivism in Mathematics, vol. I, North-Holland, 1988."},{"key":"9929_CR30","unstructured":"Troelstra, A. S., and H. Schwichtenberg Basic Proof Theory, Oxford University Press, Oxford, 1996."}],"container-title":["Studia Logica"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-020-09929-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s11225-020-09929-8\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s11225-020-09929-8.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2021,7,18]],"date-time":"2021-07-18T13:05:38Z","timestamp":1626613538000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s11225-020-09929-8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2021,1,13]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2021,8]]}},"alternative-id":["9929"],"URL":"https:\/\/doi.org\/10.1007\/s11225-020-09929-8","relation":{},"ISSN":["0039-3215","1572-8730"],"issn-type":[{"type":"print","value":"0039-3215"},{"type":"electronic","value":"1572-8730"}],"subject":[],"published":{"date-parts":[[2021,1,13]]},"assertion":[{"value":"21 July 2020","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"15 October 2020","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"13 January 2021","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}