Document Open Access Logo

Conservativity of Type Theory over Higher-Order Arithmetic

Authors Daniël Otten , Benno van den Berg

PDF
Thumbnail PDF

File

LIPIcs.CSL.2024.44.pdf
  • Filesize: 0.83 MB
  • 23 pages

Document Identifiers

Author Details

Daniël Otten
  • ILLC, University of Amsterdam, The Netherlands
Benno van den Berg
  • ILLC, University of Amsterdam, The Netherlands

Funding

This publication is part of the project "The Power of Equality" (with project number OCENW.M20.380) of the research programme Open Competition Science M 2 which is (partly) financed by the Dutch Research Council (NWO).

Cite As Get BibTex

Daniël Otten and Benno van den Berg. Conservativity of Type Theory over Higher-Order Arithmetic. In 32nd EACSL Annual Conference on Computer Science Logic (CSL 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 288, pp. 44:1-44:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024) https://doi.org/10.4230/LIPIcs.CSL.2024.44

Abstract

We investigate how much type theory can prove about the natural numbers. A classical result in this area shows that dependent type theory without any universes is conservative over Heyting Arithmetic (HA). We build on this result by showing that type theories with one level of impredicative universes are conservative over Higher-order Heyting Arithmetic (HAH). This result clearly depends on the specific type theory in question, however, we show that the interpretation of logic also plays a major role. For proof-irrelevant interpretations, we will see that strong versions of type theory prove exactly the same higher-order arithmetical formulas as HAH. Conversely, for proof-relevant interpretations, they prove different second-order arithmetical formulas than HAH, while still proving exactly the same first-order arithmetical formulas. Along the way, we investigate the various interpretations of logic in type theory, and to what extent dependent type theories can be seen as extensions of higher-order logic. We apply our results by proving a De Jongh’s theorem for type theory.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Higher order logic
  • Theory of computation → Constructive mathematics
Keywords
  • Conservativity
  • Arithmetic
  • Realizability
  • Calculus of Inductive Constructions

Metrics

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

Related Versions

References

  1. Steve Awodey, Jonas Frey, and Sam Speight. Impredicative encodings of (higher) inductive types. In Proceedings of the 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, LICS '18, pages 76-85, New York, NY, USA, 2018. Association for Computing Machinery. URL: https://doi.org/10.1145/3209108.3209130.
  2. Steve Awodey, Nicola Gambino, and Kristina Sojakova. Inductive types in homotopy type theory. In 2012 27th Annual IEEE Symposium on Logic in Computer Science, pages 95-104, 2012. URL: https://doi.org/10.1109/LICS.2012.21.
  3. Michael Beeson. Foundations of Constructive Mathematics. A Series of Modern Surveys in Mathematics. Springer, Berlin, 1985. Google Scholar
  4. Stefano Berardi. Encoding of data types in pure construction calculus: a semantic justification. In G. Huet and G. Plotkin, editors, Logical Environments, pages 30-60, 1993. Google Scholar
  5. Yves Bertot and Pierre Castéran. Interactive theorem proving and program development, Coq’Art: the calculus of inductive constructions. Springer Science & Business Media, 2013. Google Scholar
  6. Ingemarie Bethke. Notes on partial combinatory algebras. PhD thesis, University of Amsterdam, 1988. Google Scholar
  7. Andrés Caicedo. How is exponentiation defined in Peano arithmetic? Mathematics Stack Exchange, 2013. (version: 2017-04-13). URL: https://math.stackexchange.com/q/313049.
  8. Georg Cantor. Ein Beitrag zur Mannigfaltigkeitslehre. Journal für die reine und angewandte Mathematik, 84:242-258, 1877. URL: http://eudml.org/doc/148353.
  9. Ray-Ming Chen and Michael Rathjen. Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory. Archive for Mathematical Logic, 51(7):789-818, 2012. Google Scholar
  10. J.H. Conway. Regular Algebra and Finite Machines. Chapman and Hall mathematics series. Dover Publications, Incorporated, 2012. URL: https://books.google.nl/books?id=1KAXc5TpEV8C.
  11. Thierry Coquand and Gérard Huet. The calculus of constructions. Information and Computation, 76(2):95-120, 1988. URL: https://doi.org/10.1016/0890-5401(88)90005-3.
  12. Dick de Jongh. The maximality of the intuitionistic predicate calculus with respect to Heyting’s arithmetic. The Journal of Symbolic Logic, 1970. Google Scholar
  13. Dick de Jongh and Craig Smorynski. Kripke models and the intuitionistic theory of species. Annals of Mathematical Logic, 9(1):157, 1976. URL: https://doi.org/10.1016/0003-4843(76)90008-5.
  14. Dick de Jongh, Rineke Verbrugge, and Albert Visser. Intermediate logics and the de jongh property. Archive for Mathematical Logic, 50(1-2):197-213, 2011. Google Scholar
  15. Radu Diaconescu. Axiom of choice and complementation. Proceedings of the American Mathematical Society, 51(1):176-178, 1975. URL: http://www.jstor.org/stable/2039868.
  16. Peter Dybjer. Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Theoretical Computer Science, 176(1):329-335, 1997. URL: https://doi.org/10.1016/S0304-3975(96)00145-4.
  17. Harvey Friedman and Andrej Ščedrov. On the quantificational logic of intuitionistic set theory. Mathematical proceedings of the Cambridge Philosophical Society, 99(1):5-10, 1986. Google Scholar
  18. Herman Geuvers. The calculus of constructions and higher order logic, pages 139-191. Cahiers du centre de logique. Katholieke Universiteit Leuven, Belgium, 1994. Google Scholar
  19. Herman Geuvers. Induction is not derivable in second order dependent type theory. In Samson Abramsky, editor, Typed Lambda Calculi and Applications, pages 166-181, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  20. Jean-Yves Girard. Proofs and types, volume 7. Cambridge university press Cambridge, 1989. Google Scholar
  21. Petr Hájek and Pavel Pudlák. Metamathematics of first-order arithmetic, volume 3. Cambridge University Press, 2017. Google Scholar
  22. Martin Hofmann. Syntax and Semantics of Dependent Types, pages 79-130. Publications of the Newton Institute. Cambridge University Press, 1997. URL: https://doi.org/10.1017/CBO9780511526619.004.
  23. Martin Hyland. A small complete category. Annals of pure and applied logic, 40(2):135-165, 1988. Google Scholar
  24. Bart Jacobs. Comprehension categories and the semantics of type dependency. Theoretical Computer Science, 107(2):169-207, 1993. URL: https://doi.org/10.1016/0304-3975(93)90169-T.
  25. Richard Kaye. Models of Peano arithmetic. Clarendon Press, 1991. Google Scholar
  26. S. C. Kleene. Representation of Events in Nerve Nets and Finite Automata, pages 3-42. Princeton University Press, Princeton, 1956. URL: https://doi.org/10.1515/9781400882618-002.
  27. D. Kozen. A completeness theorem for kleene algebras and the algebra of regular events. Information and Computation, 110(2):366-390, 1994. URL: https://doi.org/10.1006/inco.1994.1037.
  28. Giuseppe Longo and Eugenio Moggi. Constructive natural deduction and its ‘ω-set’ interpretation. Mathematical Structures in Computer Science, 1(2):215-254, 1991. URL: https://doi.org/10.1017/S0960129500001298.
  29. Robert S. Lubarsky. Independence results around constructive ZF. Annals of Pure and Applied Logic, 132(2):209-225, 2005. URL: https://doi.org/10.1016/j.apal.2004.08.002.
  30. Per Martin-Löf. Intuitionistic type theory. Studies in proof theory. Lecture notes; 1 861180607. Bibliopolis, Napoli, 1984. Google Scholar
  31. Daniël Otten. De Jongh’s theorem for type theory. Master’s thesis, University of Amsterdam, 2022. URL: https://eprints.illc.uva.nl/id/document/12640.
  32. Robert Passmann. De Jongh’s theorem for intuitionistic Zermelo-Fraenkel set theory. In Maribel Fernández and Anca Muscholl, editors, 28th EACSL Annual Conference on Computer Science Logic (CSL 2020), volume 152 of Leibniz International Proceedings in Informatics (LIPIcs), pages 33:1-33:16, Dagstuhl, Germany, 2020. Schloss Dagstuhl-Leibniz-Zentrum fuer Informatik. URL: https://doi.org/10.4230/LIPIcs.CSL.2020.33.
  33. Robert Passmann. The first-order logic of CZF is intuitionistic first-order logic. The Journal of Symbolic Logic, pages 1-23, 2022. URL: https://doi.org/10.1017/jsl.2022.51.
  34. Christine Paulin-Mohring. Introduction to the calculus of inductive constructions, 2015. Google Scholar
  35. Bernhard Reus. Realizability models for type theories. Electronic Notes in Theoretical Computer Science, 23(1):128-158, 1999. Tutorial Workshop on Realizability Semantics and Applications (associated to FLoC'99, the 1999 Federated Logic Conference). URL: https://doi.org/10.1016/S1571-0661(04)00108-2.
  36. Mike Shulman. Impredicative encodings, part 3, November 2018. URL: https://homotopytypetheory.org/2018/11/26/impredicative-encodings-part-3/.
  37. Jan M. Smith. The independence of Peano’s fourth axiom from Martin-Löf’s type theory without universes. The Journal of Symbolic Logic, 53(3):840-845, 1988. URL: http://www.jstor.org/stable/2274575.
  38. Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis. New York,: Springer, 1973. Google Scholar
  39. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in Mathematics, volume I. North-Holland Publishing Co., 1988. Google Scholar
  40. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in Mathematics, volume II. North-Holland Publishing Co., 1988. Google Scholar
  41. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. https://homotopytypetheory.org/book, Institute for Advanced Study, 2013.
  42. Benno van den Berg and Lotte van Slooten. Arithmetical conservation results. Indagationes Mathematicae, 29:260-275, 2018. Google Scholar
  43. Jaap van Oosten. A general form of relative recursion. Notre Dame Journal of Formal Logic, 47(3):311-318, 2006. 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