Document Open Access Logo

Investigations on Higher-Order Infinitary Logic

Authors Thomas Traversié , Olivier Hermant , Marc Aiguier

PDF

File

Thumbnail PDF
PDF
LIPIcs.FSCD.2026.33.pdf
  • Filesize: 0.8 MB
  • 19 pages

Document Identifiers

Subject Classification

ACM Subject Classification
  • Theory of computation → Higher order logic
  • Theory of computation → Proof theory
Keywords
  • Infinitary logic
  • higher-order logic
  • cut elimination
  • constructivization

Metrics

Abstract

Higher-order logic and infinitary logic are two extensions of first-order logic that allow greater expressivity. Both features have not been investigated together yet. In this paper, we define a higher-order infinitary logic, based on an extension of simple type theory. The resulting logic features higher-order quantifiers, infinite conjunctions and infinite disjunctions. We establish results at both the syntactic and the semantic level. We introduce a sound notion of model, and we show a strong version of completeness that entails the cut-elimination theorem for natural deduction. Moreover, we prove an extension of Barr’s theorem, allowing us to constructivize classical proofs of a particular fragment of higher-order infinitary logic.

Cite As Get BibTex

Thomas Traversié, Olivier Hermant, and Marc Aiguier. Investigations on Higher-Order Infinitary Logic. In 11th International Conference on Formal Structures for Computation and Deduction (FSCD 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 378, pp. 33:1-33:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026) https://doi.org/10.4230/LIPIcs.FSCD.2026.33

Author Details

Thomas Traversié
  • Université Paris-Saclay, CentraleSupélec, MICS, Gif-sur-Yvette, France
  • Université Paris-Saclay, Inria, CNRS, ENS Paris-Saclay, LMF, Gif-sur-Yvette, France
Olivier Hermant
  • Université PSL, Mines Paris, CRI, Paris, France
Marc Aiguier
  • Université Paris-Saclay, CentraleSupélec, MICS, Gif-sur-Yvette, France

Acknowledgements

We dedicate this paper to the memory of Gilles Dowek, with whom we began this work. We would like to thank the anonymous reviewers for their suggestions, which have helped us improve this paper.

References

  1. Peter B Andrews. Resolution in type theory. The Journal of Symbolic Logic, 36(3):414-432, September 1971. URL: https://doi.org/10.2307/2269949.
  2. Michael Barr. Toposes without points. Journal of Pure and Applied Algebra, 5(3):265-280, 1974. URL: https://doi.org/10.1016/0022-4049(74)90037-1.
  3. Jon Barwise. Infinitary logic and admissible sets. Journal of Symbolic Logic, 34(2):226-252, 1969. URL: https://doi.org/10.2307/2271099.
  4. Alonzo Church. A Formulation of the Simple Theory of Types. The Journal of Symbolic Logic, 5(2):56-68, 1940. URL: https://doi.org/10.2307/2266170.
  5. Mary DeMarco and James Lipton. Completeness and cut-elimination in the intuitionistic theory of types. Journal of Logic and Computation, 15(6):821-854, December 2005. URL: https://doi.org/10.1093/logcom/exi055.
  6. Gilles Dowek and Olivier Hermant. A simple proof that super-consistency implies cut elimination. In Franz Baader, editor, Proceedings of the 18th International Conference on Term Rewriting and Applications (RTA), volume 4533 of Lecture Notes in Computer Science, pages 93-106, Berlin, Heidelberg, 2007. Springer. URL: https://doi.org/10.1007/978-3-540-73449-9_9.
  7. Gilles Dowek and Olivier Hermant. A Simple Proof that Super-Consistency Implies Cut Elimination. Notre Dame Journal of Formal Logic, 53(4):439-456, 2012. URL: https://doi.org/10.1215/00294527-1722692.
  8. Gilles Dowek and Benjamin Werner. Proof normalization modulo. The Journal of Symbolic Logic, 68(4):1289-1316, December 2003. URL: https://doi.org/10.2178/jsl/1067620188.
  9. William M. Farmer. The seven virtues of simple type theory. Journal of Applied Logic, 6(3):267-286, 2008. URL: https://doi.org/10.1016/j.jal.2007.11.001.
  10. Solomon Feferman. Lectures on proof theory. In M. H. Löb, editor, Proceedings of the Summer School in Logic Leeds, 1967, pages 1-107, Berlin, Heidelberg, 1968. Springer Berlin Heidelberg. Google Scholar
  11. Harvey Friedman. Classically and intuitionistically provably recursive functions. In Gert H. Müller and Dana S. Scott, editors, Higher Set Theory, pages 21-27, Berlin, Heidelberg, 1978. Springer Berlin Heidelberg. Google Scholar
  12. Gerhard Gentzen. Die Widerspruchsfreiheit der Reinen Zahlentheorie. Mathematische Annalen, 112:493-565, 1936. Google Scholar
  13. Gaëtan Gilbert and Olivier Hermant. Normalisation by completeness with heyting algebras. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning - 20th International Conference, LPAR-20 2015, Suva, Fiji, November 24-28, 2015, Proceedings, volume 9450 of Lecture Notes in Computer Science, pages 469-482. Springer, 2015. URL: https://doi.org/10.1007/978-3-662-48899-7_33.
  14. Jean-Yves Girard. Interprétation fonctionnelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris 7, June 1972. Google Scholar
  15. Kurt Gödel. Zur intuitionistischen Arithmetik und Zahlentheorie. Ergebnisse eines Mathematischen Kolloquiums, 4:34-38, 1933. Google Scholar
  16. Olivier Hermant and James Lipton. A constructive semantic approach to cut elimination in type theories with axioms. In Michael Kaminski and Simone Martini, editors, CSL, volume 5213 of Lecture Notes in Computer Science, pages 169-183. Springer, 2008. URL: https://doi.org/10.1007/978-3-540-87531-4_14.
  17. Olivier Hermant and James Lipton. Cut elimination in the intuitionistic theory of types with axioms and rewriting cuts, constructively. In Christoph Benzmüller, Chad E. Brown, Jörg Siekmann, and Richard Statman, editors, Reasoning in Simple Type Theory - Festschrift in Honor of Peter B. Andrews on His 70th Birthday, volume 17 of Studies in Logic and the Foundations of Mathematics, pages 101-134. College Publications London, 2008. Google Scholar
  18. Peter Johnstone. Sketches of an Elephant: A Topos Theory Compendium. Volume 1 and Volume 2. Oxford University Press, 2002. Google Scholar
  19. Carol R. Karp. Languages with Expressions of Infinite Length. Studies in Logic and the Foundations of Mathematics. North-Holland, Amsterdam, 1964. Google Scholar
  20. H. Jerome Keisler. Model Theory for Infinitary Logic. North-Holland, Amsterdam, 1971. Google Scholar
  21. Andrey Nikolaevich Kolmogorov. O principe tertium non datur. Matematicheskiĭ Sbornik, 32:646-667, 1925. Google Scholar
  22. Sigekatu Kuroda. Intuitionistische Untersuchungen der formalistischen Logik. Nagoya Mathematical Journal, 2:35-47, 1951. URL: https://doi.org/10.1017/S0027763000010023.
  23. E. G. K. López-Escobar. An interpolation theorem for denumerably long formulas. Fundamenta Mathematicae, 57(3):253-272, 1965. Google Scholar
  24. Shôji Maehara. Lattice-valued representation of the cut-elimination theorem. Tsukuba Journal of Mathematics, 15(2):509-521, 1991. URL: http://www.jstor.org/stable/43685780.
  25. Saunders McLane and Ieke Moerdijk. Sheaves in geometry and logic: A first introduction to topos theory. Springer Verlag, 1992. Google Scholar
  26. 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 International Publishing, Cham, 2021. URL: https://doi.org/10.1007/978-3-030-71258-7_12.
  27. Mitsuhiro Okada. A uniform semantic proof for cut-elimination and completeness of various first and higher order logics. Theoretical Computer Science, 281:471-498, 2002. URL: https://doi.org/10.1016/S0304-3975(02)00024-5.
  28. Erik Palmgren. An Intuitionistic Axiomatisation of Real Closed Fields. Mathematical Logic Quarterly, 48(2):297-299, 2002. URL: https://doi.org/10.1002/1521-3870(200202)48:2%3C297::AID-MALQ297%3E3.0.CO;2-G.
  29. Dag Prawitz. Hauptsatz for higher order logic. The Journal of Symbolic Logic, 33(3):452-457, September 1968. URL: https://doi.org/10.2307/2270331.
  30. 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, Berlin, Boston, 2016. URL: https://doi.org/10.1515/9781501502620-019.
  31. Kurt Schütte. Syntactical and semantical properties of simple type theory. The Journal of Symbolic Logic, 25(4):305-326, December 1960. URL: https://doi.org/10.2307/2963525.
  32. Raymond M. Smullyan. First-Order Logic. Springer-Verlag, Berlin Heidelberg New York, 1968. Google Scholar
  33. William W. Tait. Intensional Interpretations of Functionals of Finite Type I. The Journal of Symbolic Logic, 32(2):198-212, 1967. URL: https://doi.org/10.2307/2271658.
  34. William W. Tait. Normal derivability in classical logic. In Jon Barwise, editor, The Syntax and Semantics of Infinitary Languages, pages 204-236, Berlin, Heidelberg, 1968. Springer Berlin Heidelberg. Google Scholar
  35. Moto-o Takahashi. A proof of cut-elimination theorem in simple type-theory. Journal of the Mathematical Society of Japan, 19(4):399-410, 1967. Google Scholar
  36. Gaisi Takeuti. Chapter 4 Infinitary Logic. In Proof Theory, volume 81 of Studies in Logic and the Foundations of Mathematics, pages 188-284. Elsevier, 1975. URL: https://doi.org/10.1016/S0049-237X(08)70609-8.
  37. Ralph Gregory Taylor. Zermelo 1932a. In Heinz-Dieter Ebbinghaus, Craig G. Fraser, and Akihiro Kanamori, editors, Ernst Zermelo - Collected Works/Gesammelte Werke: Volume I - Set Theory, Miscellanea / Band I - Mengenlehre, Varia, pages 532-549. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010. URL: https://doi.org/10.1007/978-3-540-79384-7_29.
  38. Thomas Traversié. Monad Translations for Higher-Order Logic. In Maribel Fernández, editor, 10th International Conference on Formal Structures for Computation and Deduction (FSCD 2025), volume 337 of Leibniz International Proceedings in Informatics (LIPIcs), pages 34:1-34:14, Dagstuhl, Germany, 2025. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.FSCD.2025.34.
  39. Benno van den Berg. A Kuroda-style j-translation. Archive for Mathematical Logic, 58(5-6):627-634, August 2019. URL: https://doi.org/10.1007/s00153-018-0656-x.
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

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