Document Open Access Logo

The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation

Authors Martín Hötzel Escardó, Chuangjie Xu

PDF
Thumbnail PDF

File

LIPIcs.TLCA.2015.153.pdf
  • Filesize: 345 kB
  • 12 pages

Document Identifiers

Author Details

Martín Hötzel Escardó
Chuangjie Xu

Cite As Get BibTex

Martín Hötzel Escardó and Chuangjie Xu. The Inconsistency of a Brouwerian Continuity Principle with the Curry–Howard Interpretation. In 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015). Leibniz International Proceedings in Informatics (LIPIcs), Volume 38, pp. 153-164, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2015) https://doi.org/10.4230/LIPIcs.TLCA.2015.153

Abstract

If all functions (N -> N) -> N are continuous then 0 = 1. We establish this in intensional (and hence also in extensional) intuitionistic dependent-type theories, with existence in the formulation of continuity expressed as a Sigma type via the Curry-Howard interpretation. But with an intuitionistic notion of anonymous existence, defined as the propositional truncation of Sigma, it is consistent that all such functions are continuous. A model is Johnstone’s topological topos. On the other hand, any of these two intuitionistic conceptions of existence give the same, consistent, notion of uniform continuity for functions (N -> 2) -> N, again valid in the topological topos. It is open whether the consistency of (uniform) continuity extends to homotopy type theory. The theorems of type theory informally proved here are also formally proved in Agda, but the development presented here is self-contained and doesn't show Agda code.

Subject Classification

Keywords
  • Dependent type
  • intensional Martin-Löf type theory
  • Curry-Howard interpretation
  • constructive mathematics
  • Brouwerian continuity axioms
  • anonymous exi

Metrics

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

References

  1. Steve Awodey and Andrej Bauer. Propositions as [types]. Journal of Logic and Computation, 14(4):447-471, 2004. Google Scholar
  2. Michael J. Beeson. Foundations of Constructive Mathematics. Springer-Verlag, 1985. Google Scholar
  3. Ana Bove and Peter Dybjer. Dependent types at work. Lecture Notes for the LerNet Summer School, Piriápolis, Uruguay, 2008. Google Scholar
  4. Ana Bove, Peter Dybjer, and Ulf Norell. A brief overview of Agda - a functional language with dependent types. In Theorem proving in higher order logics, volume 5674 of Lecture Notes in Computer Science, pages 73-78. Springer, 2009. Google Scholar
  5. Martín Hötzel Escardó and Chuangjie Xu. A constructive manifestation of the Kleene-Kreisel continuous functionals. To appear in APAL, 2013. Google Scholar
  6. Martín Hötzel Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation (Agda development). School of Computer Science, University of Birmingham, UK. Available at http://www.cs.bham.ac.uk/~mhe/continuity-false/, 2015.
  7. Michael Hedberg. A coherence theorem for Martin-Löf’s type theory. J. Functional Programming, pages 413-436, 1998. Google Scholar
  8. J Martin E Hyland. The effective topos. Studies in Logic and the Foundations of Mathematics, 110:165-216, 1982. Google Scholar
  9. Peter T. Johnstone. On a topological topos. Proceedings of the London Mathematical Society, 38(3):237-271, 1979. Google Scholar
  10. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Generalizations of hedberg’s theorem. In Typed Lambda Calculi and Applications, volume 7941 of Lecture Notes in Computer Science, pages 173-188. Springer Berlin Heidelberg, 2013. Google Scholar
  11. Nicolai Kraus, Martín Escardó, Thierry Coquand, and Thorsten Altenkirch. Notions of anonymous existence in Martin-Löf Type Theory. Submitted for publication, 2014. Google Scholar
  12. G. Kreisel. On weak completeness of intuitionistic predicate logic. J. Symbolic Logic, 27:139-158, 1962. Google Scholar
  13. Maria Emilia Maietti. The internal type theory of a Heyting pretopos. In Eduardo Giménez and Christine Paulin-Mohring, editors, Types for Proofs and Programs, volume 1512 of Lecture Notes in Computer Science, pages 216-235. Springer Berlin Heidelberg, 1998. Google Scholar
  14. N. P. Mendler. Quotient types via coequalizers in Martin-Löf type theory. In G. Huet and G. Plotkin, editors, Informal Proceedings of the First Workshop on Logical Frameworks, Antibes, May 1990, pages 349–360, 1990, May 1990. Google Scholar
  15. M. Menni and A. Simpson. Topological and limit-space subcategories of countably-based equilogical spaces. Math. Struct. Comput. Sci., 12(6):739-770, 2002. Google Scholar
  16. U. Norell. Dependently typed programming in Agda. In Proceedings of the 4th international workshop on Types in language design and implementation, TLDI '09, pages 1-2, 2009. Google Scholar
  17. The Univalent Foundations Program. Homotopy Type Theory: Univalent Foundations of Mathematics. Institute for Advanced Study, 2013. Google Scholar
  18. A. S. Troelstra. A note on non-extensional operations in connection with continuity and recursiveness. Indag. Math., 39(5):455-462, 1977. Google Scholar
  19. Anne Sjerp Troelstra and Dirk van Dalen. Constructivism in Mathematics : An Introduction. North-Holland, 1988. Google Scholar
  20. Chuangjie Xu and Martín Hötzel Escardó. A constructive model of uniform continuity. In Typed Lambda Calculi and Applications, volume 7941 of Lecture Notes in Computer Science, pages 236-249. Springer Berlin Heidelberg, 2013. 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