Document Open Access Logo

Constructive Cut Elimination in Geometric Logic

Authors Giulio Fellin , Sara Negri , Eugenio Orlandelli

PDF
Thumbnail PDF

File

LIPIcs.TYPES.2021.7.pdf
  • Filesize: 0.8 MB
  • 16 pages

Document Identifiers

Author Details

Giulio Fellin
  • Department of Computer Science, University of Verona, Italy
  • Department of Mathematics, University of Trento, Italy
  • Department of Philosophy, History and Art Studies, University of Helsinki, Finland
Sara Negri
  • Department of Mathematics, University of Genoa, Italy
Eugenio Orlandelli
  • Department of Philosophy and Communication Studies, University of Bologna, Italy

Funding

Partially funded by the Academy of Finland, research project no. 1308664.

Acknowledgements

We are very grateful to Peter Schuster for precious comments and helpful discussions on various points. We also thank the three anonymous referees for their detailed and insightful comments that helped improving the paper.

Cite As Get BibTex

Giulio Fellin, Sara Negri, and Eugenio Orlandelli. Constructive Cut Elimination in Geometric Logic. In 27th International Conference on Types for Proofs and Programs (TYPES 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 239, pp. 7:1-7:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.TYPES.2021.7

Abstract

A constructivisation of the cut-elimination proof for sequent calculi for classical and intuitionistic infinitary logic with geometric rules - given in earlier work by the second author - is presented. This is achieved through a procedure in which the non-constructive transfinite induction on the commutative sum of ordinals is replaced by two instances of Brouwer’s Bar Induction. Additionally, a proof of Barr’s Theorem for geometric theories that uses only constructively acceptable proof-theoretical tools is obtained.

Subject Classification

ACM Subject Classification
  • Theory of computation → Proof theory
Keywords
  • Geometric theories
  • sequent calculi
  • axioms-as-rules
  • infinitary logic
  • constructive cut elimination

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Peter Aczel and Michael Rathjen. Notes on constructive set theory. Technical report, Institut Mittag-Leffler (The Royal Swedish Academy of Sciences), 2001. URL: https://ncatlab.org/nlab/files/AczelRathjenCST.pdf.
  2. Ryota Akiyoshi. An ordinal-free proof of the complete cut-elimination theorem for Π₁¹-CA + BI with the ω-rule. IfCoLog J. of Logics and their Applications, 4:867-884, January 2017. Google Scholar
  3. Michael Barr. Toposes without points. J. Pure Appl. Algebra, 5(3):265-280, 1974. URL: https://doi.org/10.1016/0022-4049(74)90037-1.
  4. Agata Ciabattoni, George Metcalfe, and Franco Montagna. Algebraic and proof-theoretic characterizations of truth stressers for mtl and its extensions. Fuzzy Sets and Systems, 161(3):369-389, 2010. Fuzzy Logics and Related Structures. URL: https://doi.org/10.1016/j.fss.2009.09.001.
  5. Haskell B. Curry. Foundations of Mathematical Logic. Dover Books on Mathematics Series. Dover Publications, 1977. Google Scholar
  6. Solomon Feferman. Lectures on Proof Theory. In Proceedings of the Summer School in Logic (Leeds, 1967), pages 1-107. Springer, Berlin, 1968. Google Scholar
  7. Peter Freyd. Aspects of topoi. Bull. Austral. Math. Soc., 7(1):1-76, 1972. URL: https://doi.org/10.1017/S0004972700044828.
  8. Andrzej Indrzejczak. Eliminability of cut in hypersequent calculi for some modal logics of linear frames. Information Processing Letters, 115(2):75-81, 2015. URL: https://doi.org/10.1016/j.ipl.2014.07.002.
  9. Peter T. Johnstone. Sketches of an Elephant: A Topos Theory Compendium. Vol. 1 & 2. Oxford University Press, New York, 2002. Google Scholar
  10. Hidenori Kurokawa. Hypersequent calculi for modal logics extending S4. In Yukiko Nakano, Ken Satoh, and Daisuke Bekki, editors, New Frontiers in Artificial Intelligence, pages 51-68, Cham, 2014. Springer International Publishing. URL: https://doi.org/10.1007/978-3-319-10061-6_4.
  11. E. G. K. Lopez-Escobar. An interpolation theorem for denumerably long formulas. Fund. Math., 57:253-272, 1965. URL: https://doi.org/10.4064/fm-57-3-253-272.
  12. Saunders Mac Lane and Ieke Moerdijk. Sheaves in Geometry and Logic. A First Introduction to Topos Theory. Springer-Verlag, 1994. URL: https://doi.org/10.1007/978-1-4612-0927-0.
  13. George Metcalfe, Nicola Olivetti, and Dov Gabbay. Proof Theory for Fuzzy Logics. Springer, 2008. URL: https://doi.org/10.1007/978-1-4020-9409-5.
  14. Sara Negri. Contraction-free sequent calculi for geometric theories with an application to Barr’s theorem. Arch. Math. Logic, 42(4):389-401, 2003. URL: https://doi.org/10.1007/s001530100124.
  15. Sara Negri. Glivenko sequent classes in the light of structural proof theory. Arch. Math. Logic, 55(3-4):461-473, 2016. URL: https://doi.org/10.1007/s00153-016-0474-y.
  16. Sara Negri. Geometric rules in infinitary logic. In Ofer Arieli and Anna Zamansky, editors, Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, pages 265-293. Springer, 2021. URL: https://doi.org/10.1007/978-3-030-71258-7_12.
  17. Sara Negri and Jan von Plato. Proof Analysis. A Contribution to Hilbert’s Last Problem. Cambridge University Press, Cambridge, 2011. Google Scholar
  18. V.P. Orevkov. Glivenko’s sequence classes. In V.P. Orevkov, editor, Logical and logico-mathematical calculi. Part 1, pages 131-154. Inst. Steklov, Leningrad, 1968. Google Scholar
  19. Michael Rathjen. A note on Bar Induction in constructive set theory. Mathematical Logic Quarterly, 52(3):253-258, 2006. URL: https://doi.org/10.1002/malq.200510030.
  20. Michael Rathjen. Remarks on Barr’s theorem. Proofs in geometric theories. In Dieter Probst and Peter Schuster, editors, Concepts of Proof in Mathematics, Philosophy, and Computer Science, pages 347-374. de Gruyter, 2016. URL: https://doi.org/10.1515/9781501502620-019.
  21. Annika Siders. From Stenius' consistency proof to Schütte’s cut elimination for ω-arithmetic. Rev. Symb. Log., 9(1):1-22, 2016. URL: https://doi.org/10.1017/S1755020315000337.
  22. Göran Sundholm. Proof theory, a survey of the omega-rule. Videnskapsselskapets skrifter, 1. Mat.-naturv. klasse, 4, April 1983. Google Scholar
  23. Gaisi Takeuti. Proof Theory. North-Holland, 1987 (second edition). Google Scholar
  24. Anne S. Troelstra and Helmut Schwichtenberg. Basic Proof Theory. Cambridge University Press, Cambridge, 2nd edition, 2000. URL: https://doi.org/10.1017/CBO9781139168717.
  25. Gavin C. Wraith. Generic Galois theory of local rings. In Michael P. Fourman et al., editor, Applications of Sheaves, pages 739-767. Springer-Verlag, 1979. URL: https://doi.org/10.1007/BFb0061844.
  26. Gavin C. Wraith. Intuitionistic algebra: some recent developments in topos theory. In Proceedings of the International Congress of Mathematicians (Helsinki, 1978), pages 331-337. Acad. Sci. Fennica, 1980. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact