Abstract
A constructivisation of the cut-elimination proof for sequent calculi for classical, intuitionistic and minimal infinitary logics with geometric rules—given in earlier work by the second author—is presented. This is achieved through a procedure where the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. The proof of admissibility of the structural rules is made ordinal-free by introducing a new well-founded relation based on a notion of embeddability of derivations. Additionally, conservativity for classical over intuitionistic/minimal logic for the seven (finitary) Glivenko sequent classes is here shown to hold also for the corresponding infinitary classes.
Similar content being viewed by others
Availability of data and materials
Data sharing not applicable to this article as no datasets were generated or analysed during the current study.
Notes
Barr’s theorem is often alleged to achieve more in that it also allows to eliminate uses of the axiom of choice. That such formulations of Barr’s theorem should be taken with caution is demonstrated in [25] where internal versus external addition of the the axiom of choice is considered and it is shown that the latter preserves conservativity whereas the former does not.
Barr’s Theorem corresponds to Orevkov’s first class.
By “constructive” here we mean not relying on classical logical principles such as excluded middle or linearity of ordinals but we do not mean acceptable in all schools of constructive mathematics.
Even if all proofs in [7] make no use of non-constructive assumptions about ordinals, we prefer to avoid completely the assumption of total ordering.
Derivations can thus be represented as (infinite) trees, where the nodes are the sequents in the derivation, and a nodes that corresponds to a premiss of a rule is an immediate successor of the node that corresponds to the conclusion of such rule. Therefore, a node that corresponds to the conclusion of a rule with \(\beta \) premisses has \(\beta \) immediate successors.
This example is due to Parlamento and Previale [24].
One may be mislead here by assuming that the correspondence between branches implies that the two derivations have the same structure. However, this is not the case as the correspondence is not required to be injective nor surjective.
Since the number of nodes of the tree is at most countable, one may also define an encoding such that the correspondence is unique. This however would require more effort and we would lose the property that every infinite sequence has an initial segment that indexes a branch of the tree.
Orevkov [23] proved optimality for the finitary case by classifying the other possible classes of sequents and exhibiting for each of them a sequent that is classically but not intuitionistically derivable.
References
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
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–884 (2017)
Barr, M.: Toposes without points. J. Pure Appl. Algebra 5(3), 265–280 (1974)
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–389 (2010). https://doi.org/10.1016/j.fss.2009.09.001
Curry, H.B.: Foundations of Mathematical Logic. Dover Books on Mathematics Series, Dover Publications, New York (1977)
Feferman, S.: Lectures on proof theory. In: Proceedings of the Summer School in Logic (Leeds, 1967), pp. 1–107. Springer, Berlin (1968). https://doi.org/10.1007/bfb0079094
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–7:16. LIPIcs (2022). https://doi.org/10.4230/LIPIcs.TYPES.2021.7
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–227. College Publications, London (2020)
Freyd, P.: Aspects of topoi. Bull. Austral. Math. Soc. 7(1), 1–76 (1972). https://doi.org/10.1017/S0004972700044828
Indrzejczak, A.: Eliminability of cut in hypersequent calculi for some modal logics of linear frames. Inf. Process. Lett. 115(2), 75–81 (2015). https://doi.org/10.1016/j.ipl.2014.07.002
Ishihara, H.: A note on the Gödel-Gentzen translation. Math. Logic Q. 46, 135–137 (2000). https://doi.org/10.1002/(SICI)1521-3870(200001)46:1<135::AID-MALQ135>3.0.CO;2-R
Johnstone, P.T.: Sketches of an Elephant: A Topos Theory Compendium, vol. 1 and 2. Oxford University Press, New York (2002)
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–68. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-10061-6_4
Lopez-Escobar, E.G.K.: An interpolation theorem for denumerably long formulas. Fund. Math. 57, 253–272 (1965). https://doi.org/10.4064/fm-57-3-253-272
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
Metcalfe, G., Olivetti, N., Gabbay, D.: Proof Theory for Fuzzy Logics. Springer, Berlin (2008). https://doi.org/10.1007/978-1-4020-9409-5
Nadathur, G.: Correspondences between classical, intuitionistic and uniform provability. Theor. Comput. Sci. 232, 273���298 (2000). https://doi.org/10.1016/S0304-3975(99)00177-2
Negri, S.: Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Arch. Math. Logic 42(4), 389–401 (2003). https://doi.org/10.1007/s001530100124
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–293. Springer, Cham (2021). https://doi.org/10.1007/978-3-030-71258-7_12
Negri, S.: Glivenko sequent classes in the light of structural proof theory. Arch. Math. Logic 55(3–4), 461–473 (2016). https://doi.org/10.1007/s00153-016-0474-y
Negri, S., von Plato, J.: Cut elimination in the presence of axioms. Bull. Symb. Logic 4(4), 418–435 (1998). https://doi.org/10.2307/420956
Negri, S., von Plato, J.: Proof Analysis. A Contribution to Hilbert’s Last Problem, p. 265. Cambridge University Press, Cambridge (2011). https://doi.org/10.1017/CBO9781139003513
Orevkov, V.P.: Glivenko’s sequence classes. In: Orevkov, V.P. (ed.) Logical and Logico-mathematical Calculi. Part 1, pp. 131–154. American Mathematical Society, Providence (1968)
Parlamento, F., Previale, F.: A note on the sequent calculus \(\mathbf{G3[mic]^=} \). Rev. Symb. Logic 15(2), 537–551 (2022). https://doi.org/10.1017/S1755020320000155
Rathjen, M.: Remarks on Barr’s theorem: Proofs in geometric theories. In: Probst, D., Schuster, P. (eds.) Concepts of Proof in Mathematics, Philosophy, and Computer Science, pp. 347–374. de Gruyter, Berlin (2016). https://doi.org/10.1515/9781501502620-019
Schwichtenberg, H., Senjak, C.: Minimal from classical proofs. Ann. Pure Appl. Logic 164(6), 740–748 (2013)
Siders, A.: From Stenius’ consistency proof to Schütte’s cut elimination for \(\omega \)-arithmetic. Rev. Symb. Logic 9(1), 1–22 (2016). https://doi.org/10.1017/S1755020315000337
Skolem, T.: Logisch-kombinatorische Untersuchungen. Videnskapsselskapets skrifter, 1. Mat.-naturv. klasse 4 (1920)
Takeuti, G.: Proof Theory. North-Holland, Amsterdam (1987)
Troelstra, A.S., Schwichtenberg, H.: Basic Proof Theory, 2nd edn. Cambridge University Press, Cambridge (2000). https://doi.org/10.1017/CBO9781139168717
Wraith, G.: Generic Galois theory of local rings. In: Fourman, A., et al. (eds.) Applications of Sheaves, pp. 739–767. Springer, Berlin, Heidelberg (1979). https://doi.org/10.1007/BFb0061844
Acknowledgements
Special thanks are due to Peter Schuster for precious comments and helpful discussions on various points. The authors are grateful to Mario Piazza and Tarmo Uustalu for their interest and valuable suggestions. We are also grateful to an anonymous referee for detailed and insightful comments, and to the audience of the conferences LAP 2020, LAP 2021, and TYPES 2021, where the paper was presented. The first two authors are members of the “Gruppo Nazionale per le Strutture Algebriche, Geometriche e le loro Applicazioni” (GNSAGA of the Istituto Nazionale di Alta Matematica (IndAM).
Funding
Partial financial support was received from the Academy of Finland, research project no. 1308664.
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.
This paper is a revised and extended version of the conference paper [7]. The latter presented only the constructive cut elimination for classical and intuitionistic geometric logics based on Brouwer’s Bar Induction. The main novelties of this paper are (i) that also minimal geometric logic is considered, (ii) that the notion of “proof-embeddability” is here introduced and transfinite inductions on ordinals are replaced by Noetherian induction with proof-embeddability, and (iii) that proofs of conservativity for the infinitary Glivenko classes are given.
Rights and permissions
Springer Nature or its licensor (e.g. a society or other partner) holds exclusive rights to this article under a publishing agreement with the author(s) or other rightsholder(s); author self-archiving of the accepted manuscript version of this article is solely governed by the terms of such publishing agreement and applicable law.
About this article
Cite this article
Fellin, G., Negri, S. & Orlandelli, E. Glivenko sequent classes and constructive cut elimination in geometric logics. Arch. Math. Logic 62, 657–688 (2023). https://doi.org/10.1007/s00153-022-00857-z
Received:
Accepted:
Published:
Issue Date:
DOI: https://doi.org/10.1007/s00153-022-00857-z
Keywords
- Geometric theories
- Glivenko sequent classes
- Infinitary logic
- Conservativity
- Constructive cut elimination