{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,29]],"date-time":"2025-09-29T11:46:40Z","timestamp":1759146400719,"version":"3.37.3"},"reference-count":31,"publisher":"Springer Science and Business Media LLC","issue":"5-6","license":[{"start":{"date-parts":[[2022,12,8]],"date-time":"2022-12-08T00:00:00Z","timestamp":1670457600000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2022,12,8]],"date-time":"2022-12-08T00:00:00Z","timestamp":1670457600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"funder":[{"DOI":"10.13039\/501100002341","name":"Academy of Finland","doi-asserted-by":"crossref","award":["1308664"],"award-info":[{"award-number":["1308664"]}],"id":[{"id":"10.13039\/501100002341","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":["Arch. Math. Logic"],"published-print":{"date-parts":[[2023,7]]},"DOI":"10.1007\/s00153-022-00857-z","type":"journal-article","created":{"date-parts":[[2022,12,8]],"date-time":"2022-12-08T17:03:01Z","timestamp":1670518981000},"page":"657-688","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Glivenko sequent classes and constructive cut elimination in geometric logics"],"prefix":"10.1007","volume":"62","author":[{"given":"Giulio","family":"Fellin","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Sara","family":"Negri","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4021-8667","authenticated-orcid":false,"given":"Eugenio","family":"Orlandelli","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2022,12,8]]},"reference":[{"key":"857_CR1","unstructured":"Aczel, P., Rathjen, M.: Notes on constructive set theory. Technical report, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences) (2001). http:\/\/www.ml.kva.se\/preprints\/archive2000-2001.php"},{"key":"857_CR2","unstructured":"Akiyoshi, R.: An ordinal-free proof of the complete cut-elimination theorem for $$\\varvec {\\Pi _1^1}$$-CA + BI with the $$\\omega $$-rule. IfCoLog J. Logics Appl. 4, 867\u2013884 (2017)"},{"issue":"3","key":"857_CR3","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1016\/0022-4049(74)90037-1","volume":"5","author":"M Barr","year":"1974","unstructured":"Barr, M.: Toposes without points. J. Pure Appl. Algebra 5(3), 265\u2013280 (1974)","journal-title":"J. Pure Appl. Algebra"},{"issue":"3","key":"857_CR4","doi-asserted-by":"publisher","first-page":"369","DOI":"10.1016\/j.fss.2009.09.001","volume":"161","author":"A Ciabattoni","year":"2010","unstructured":"Ciabattoni, A., Metcalfe, G., Montagna, F.: Algebraic and proof-theoretic characterizations of truth stressers for MTL and its extensions. Fuzzy logics and related structures. Fuzzy Sets Syst. 161(3), 369\u2013389 (2010). https:\/\/doi.org\/10.1016\/j.fss.2009.09.001","journal-title":"Fuzzy Sets Syst."},{"key":"857_CR5","series-title":"Dover Books on Mathematics Series","volume-title":"Foundations of Mathematical Logic","author":"HB Curry","year":"1977","unstructured":"Curry, H.B.: Foundations of Mathematical Logic. Dover Books on Mathematics Series, Dover Publications, New York (1977)"},{"key":"857_CR6","doi-asserted-by":"publisher","unstructured":"Feferman, S.: Lectures on proof theory. In: Proceedings of the Summer School in Logic (Leeds, 1967), pp. 1\u2013107. Springer, Berlin (1968). https:\/\/doi.org\/10.1007\/bfb0079094","DOI":"10.1007\/bfb0079094"},{"key":"857_CR7","unstructured":"Fellin, G., Negri, S., Orlandelli, E.: Constructive cut elimination in geometric logic. In: Basold, H., Cockx, J., Ghilezan, S. (eds.) 27th International Conference on Types for Proofs and Programs (TYPES 2021), pp. 7:1\u20137:16. LIPIcs (2022). https:\/\/doi.org\/10.4230\/LIPIcs.TYPES.2021.7"},{"key":"857_CR8","first-page":"209","volume-title":"Advances in Modal Logic","author":"G Fellin","year":"2020","unstructured":"Fellin, G., Negri, S., Schuster, P.: Modal logic for induction. In: Olivetti, N., Verbrugge, R., Negri, S., Sandu, G. (eds.) Advances in Modal Logic, vol. 13, pp. 209\u2013227. College Publications, London (2020)"},{"issue":"1","key":"857_CR9","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S0004972700044828","volume":"7","author":"P Freyd","year":"1972","unstructured":"Freyd, P.: Aspects of topoi. Bull. Austral. Math. Soc. 7(1), 1\u201376 (1972). https:\/\/doi.org\/10.1017\/S0004972700044828","journal-title":"Bull. Austral. Math. Soc."},{"issue":"2","key":"857_CR10","doi-asserted-by":"publisher","first-page":"75","DOI":"10.1016\/j.ipl.2014.07.002","volume":"115","author":"A Indrzejczak","year":"2015","unstructured":"Indrzejczak, A.: Eliminability of cut in hypersequent calculi for some modal logics of linear frames. Inf. Process. Lett. 115(2), 75\u201381 (2015). https:\/\/doi.org\/10.1016\/j.ipl.2014.07.002","journal-title":"Inf. Process. Lett."},{"key":"857_CR11","doi-asserted-by":"publisher","unstructured":"Ishihara, H.: A note on the G\u00f6del-Gentzen translation. Math. Logic Q. 46, 135\u2013137 (2000). https:\/\/doi.org\/10.1002\/(SICI)1521-3870(200001)46:1<135::AID-MALQ135>3.0.CO;2-R","DOI":"10.1002\/(SICI)1521-3870(200001)46:1<135::AID-MALQ135>3.0.CO;2-R"},{"key":"857_CR12","volume-title":"Sketches of an Elephant: A Topos Theory Compendium","author":"PT Johnstone","year":"2002","unstructured":"Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium, vol. 1 and 2. Oxford University Press, New York (2002)"},{"key":"857_CR13","doi-asserted-by":"publisher","first-page":"51","DOI":"10.1007\/978-3-319-10061-6_4","volume-title":"New Frontiers in Artificial Intelligence","author":"H Kurokawa","year":"2014","unstructured":"Kurokawa, H.: Hypersequent calculi for modal logics extending $$\\textbf{S4} $$. In: Nakano, Y., Satoh, K., Bekki, D. (eds.) New Frontiers in Artificial Intelligence, pp. 51\u201368. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-10061-6_4"},{"key":"857_CR14","doi-asserted-by":"publisher","first-page":"253","DOI":"10.4064\/fm-57-3-253-272","volume":"57","author":"EGK Lopez-Escobar","year":"1965","unstructured":"Lopez-Escobar, E.G.K.: An interpolation theorem for denumerably long formulas. Fund. Math. 57, 253\u2013272 (1965). https:\/\/doi.org\/10.4064\/fm-57-3-253-272","journal-title":"Fund. Math."},{"key":"857_CR15","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0","volume-title":"Sheaves in Geometry and Logic. A First Introduction to Topics Theory","author":"S Mac Lane","year":"1994","unstructured":"Mac Lane, S., Moerdijk, I.: Sheaves in Geometry and Logic. A First Introduction to Topics Theory. Springer, New York (1994). https:\/\/doi.org\/10.1007\/978-1-4612-0927-0"},{"key":"857_CR16","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4020-9409-5","volume-title":"Proof Theory for Fuzzy Logics","author":"G Metcalfe","year":"2008","unstructured":"Metcalfe, G., Olivetti, N., Gabbay, D.: Proof Theory for Fuzzy Logics. Springer, Berlin (2008). https:\/\/doi.org\/10.1007\/978-1-4020-9409-5"},{"key":"857_CR17","doi-asserted-by":"publisher","first-page":"273","DOI":"10.1016\/S0304-3975(99)00177-2","volume":"232","author":"G Nadathur","year":"2000","unstructured":"Nadathur, G.: Correspondences between classical, intuitionistic and uniform provability. Theor. Comput. Sci. 232, 273\u2013298 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(99)00177-2","journal-title":"Theor. Comput. Sci."},{"issue":"4","key":"857_CR18","doi-asserted-by":"publisher","first-page":"389","DOI":"10.1007\/s001530100124","volume":"42","author":"S Negri","year":"2003","unstructured":"Negri, S.: Contraction-free sequent calculi for geometric theories with an application to Barr\u2019s theorem. Arch. Math. Logic 42(4), 389\u2013401 (2003). https:\/\/doi.org\/10.1007\/s001530100124","journal-title":"Arch. Math. Logic"},{"key":"857_CR19","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1007\/978-3-030-71258-7_12","volume-title":"Arnon Avron on Semantics and Proof Theory of Non-classical Logics","author":"S Negri","year":"2021","unstructured":"Negri, S.: Geometric rules in infinitary logic. In: Arieli, O., Zamansky, A. (eds.) Arnon Avron on Semantics and Proof Theory of Non-classical Logics, pp. 265\u2013293. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-71258-7_12"},{"issue":"3\u20134","key":"857_CR20","doi-asserted-by":"publisher","first-page":"461","DOI":"10.1007\/s00153-016-0474-y","volume":"55","author":"S Negri","year":"2016","unstructured":"Negri, S.: Glivenko sequent classes in the light of structural proof theory. Arch. Math. Logic 55(3\u20134), 461\u2013473 (2016). https:\/\/doi.org\/10.1007\/s00153-016-0474-y","journal-title":"Arch. Math. Logic"},{"issue":"4","key":"857_CR21","doi-asserted-by":"publisher","first-page":"418","DOI":"10.2307\/420956","volume":"4","author":"S Negri","year":"1998","unstructured":"Negri, S., von Plato, J.: Cut elimination in the presence of axioms. Bull. Symb. Logic 4(4), 418\u2013435 (1998). https:\/\/doi.org\/10.2307\/420956","journal-title":"Bull. Symb. Logic"},{"key":"857_CR22","doi-asserted-by":"publisher","first-page":"265","DOI":"10.1017\/CBO9781139003513","volume-title":"Proof Analysis. A Contribution to Hilbert\u2019s Last Problem","author":"S Negri","year":"2011","unstructured":"Negri, S., von Plato, J.: Proof Analysis. A Contribution to Hilbert\u2019s Last Problem, p. 265. Cambridge University Press, Cambridge (2011). https:\/\/doi.org\/10.1017\/CBO9781139003513"},{"key":"857_CR23","first-page":"131","volume-title":"Logical and Logico-mathematical Calculi. Part 1","author":"VP Orevkov","year":"1968","unstructured":"Orevkov, V.P.: Glivenko\u2019s sequence classes. In: Orevkov, V.P. (ed.) Logical and Logico-mathematical Calculi. Part 1, pp. 131\u2013154. American Mathematical Society, Providence (1968)"},{"issue":"2","key":"857_CR24","doi-asserted-by":"publisher","first-page":"537","DOI":"10.1017\/S1755020320000155","volume":"15","author":"F Parlamento","year":"2022","unstructured":"Parlamento, F., Previale, F.: A note on the sequent calculus $$\\mathbf{G3[mic]^=} $$. Rev. Symb. Logic 15(2), 537\u2013551 (2022). https:\/\/doi.org\/10.1017\/S1755020320000155","journal-title":"Rev. Symb. Logic"},{"key":"857_CR25","doi-asserted-by":"publisher","first-page":"347","DOI":"10.1515\/9781501502620-019","volume-title":"Concepts of Proof in Mathematics, Philosophy, and Computer Science","author":"M Rathjen","year":"2016","unstructured":"Rathjen, M.: Remarks on Barr\u2019s theorem: Proofs in geometric theories. In: Probst, D., Schuster, P. (eds.) Concepts of Proof in Mathematics, Philosophy, and Computer Science, pp. 347\u2013374. de Gruyter, Berlin (2016). https:\/\/doi.org\/10.1515\/9781501502620-019"},{"issue":"6","key":"857_CR26","doi-asserted-by":"publisher","first-page":"740","DOI":"10.1016\/j.apal.2012.05.009","volume":"164","author":"H Schwichtenberg","year":"2013","unstructured":"Schwichtenberg, H., Senjak, C.: Minimal from classical proofs. Ann. Pure Appl. Logic 164(6), 740\u2013748 (2013)","journal-title":"Ann. Pure Appl. Logic"},{"issue":"1","key":"857_CR27","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1017\/S1755020315000337","volume":"9","author":"A Siders","year":"2016","unstructured":"Siders, A.: From Stenius\u2019 consistency proof to Sch\u00fctte\u2019s cut elimination for $$\\omega $$-arithmetic. Rev. Symb. Logic 9(1), 1\u201322 (2016). https:\/\/doi.org\/10.1017\/S1755020315000337","journal-title":"Rev. Symb. Logic"},{"key":"857_CR28","unstructured":"Skolem, T.: Logisch-kombinatorische Untersuchungen. Videnskapsselskapets skrifter, 1.\u00a0Mat.-naturv.\u00a0klasse 4 (1920)"},{"key":"857_CR29","volume-title":"Proof Theory","author":"G Takeuti","year":"1987","unstructured":"Takeuti, G.: Proof Theory. North-Holland, Amsterdam (1987)"},{"key":"857_CR30","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139168717","volume-title":"Basic Proof Theory","author":"AS Troelstra","year":"2000","unstructured":"Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000). https:\/\/doi.org\/10.1017\/CBO9781139168717","edition":"2"},{"key":"857_CR31","doi-asserted-by":"publisher","first-page":"739","DOI":"10.1007\/BFb0061844","volume-title":"Applications of Sheaves","author":"G Wraith","year":"1979","unstructured":"Wraith, G.: Generic Galois theory of local rings. In: Fourman, A., et al. (eds.) Applications of Sheaves, pp. 739\u2013767. Springer, Berlin, Heidelberg (1979). https:\/\/doi.org\/10.1007\/BFb0061844"}],"container-title":["Archive for Mathematical Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-022-00857-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/article\/10.1007\/s00153-022-00857-z\/fulltext.html","content-type":"text\/html","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/s00153-022-00857-z.pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,5,30]],"date-time":"2023-05-30T02:01:56Z","timestamp":1685412116000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/s00153-022-00857-z"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,12,8]]},"references-count":31,"journal-issue":{"issue":"5-6","published-print":{"date-parts":[[2023,7]]}},"alternative-id":["857"],"URL":"https:\/\/doi.org\/10.1007\/s00153-022-00857-z","relation":{},"ISSN":["0933-5846","1432-0665"],"issn-type":[{"type":"print","value":"0933-5846"},{"type":"electronic","value":"1432-0665"}],"subject":[],"published":{"date-parts":[[2022,12,8]]},"assertion":[{"value":"14 January 2022","order":1,"name":"received","label":"Received","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"11 November 2022","order":2,"name":"accepted","label":"Accepted","group":{"name":"ArticleHistory","label":"Article History"}},{"value":"8 December 2022","order":3,"name":"first_online","label":"First Online","group":{"name":"ArticleHistory","label":"Article History"}}]}}