Document Open Access Logo

Constructing Unprejudiced Extensional Type Theories with Choices via Modalities

Authors Liron Cohen , Vincent Rahli

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2022.10.pdf
  • Filesize: 1.16 MB
  • 23 pages

Document Identifiers

Author Details

Liron Cohen
  • Ben-Gurion University of the Negev, Beer-Sheva, Israel
Vincent Rahli
  • University of Birmingham, UK

Funding

This research was partially supported by Grant No. 2020145 from the United States-Israel Binational Science Foundation (BSF).

Cite AsGet BibTex

Liron Cohen and Vincent Rahli. Constructing Unprejudiced Extensional Type Theories with Choices via Modalities. In 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 228, pp. 10:1-10:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)
https://doi.org/10.4230/LIPIcs.FSCD.2022.10

Abstract

Time-progressing expressions, i.e., expressions that compute to different values over time such as Brouwerian choice sequences or reference cells, are a common feature in many frameworks. For type theories to support such elements, they usually employ sheaf models. In this paper, we provide a general framework in the form of an extensional type theory incorporating various time-progressing elements along with a general possible-worlds forcing interpretation parameterized by modalities. The modalities can, in turn, be instantiated with topological spaces of bars, leading to a general sheaf model. This parameterized construction allows us to capture a distinction between theories that are "agnostic", i.e., compatible with classical reasoning in the sense that classical axioms can be validated, and those that are "intuitionistic", i.e., incompatible with classical reasoning in the sense that classical axioms can be proven false. This distinction is made via properties of the modalities selected to model the theory and consequently via the space of bars instantiating the modalities. We further identify a class of time-progressing elements that allows deriving "intuitionistic" theories that include not only choice sequences but also simpler operators, namely reference cells.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
  • Theory of computation → Constructive mathematics
Keywords
  • Intuitionism
  • Extensional Type Theory
  • Constructive Type Theory
  • Realizability
  • Choice sequences
  • References
  • Classical Logic
  • Theorem proving
  • Agda

Metrics

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

References

  1. Agda wiki. URL: http://wiki.portal.chalmers.se/agda/pmwiki.php.
  2. Stuart F. Allen. A non-type-theoretic definition of Martin-Löf’s types. In LICS, pages 215-221. IEEE Computer Society, 1987. Google Scholar
  3. Michael J. Beeson. Foundations of Constructive Mathematics. Springer, 1985. Google Scholar
  4. Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Computability beyond church-turing via choice sequences. In Anuj Dawar and Erich Grädel, editors, LICS 2018, pages 245-254. ACM, 2018. URL: https://doi.org/10.1145/3209108.3209200.
  5. Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Open bar - a brouwerian intuitionistic logic with a pinch of excluded middle. In Christel Baier and Jean Goubault-Larrecq, editors, CSL, volume 183 of LIPIcs, pages 11:1-11:23. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2021. URL: https://doi.org/10.4230/LIPIcs.CSL.2021.11.
  6. E. Bishop. Foundations of constructive analysis, volume 60. McGraw-Hill New York, 1967. Google Scholar
  7. Simon Boulier, Pierre-Marie Pédrot, and Nicolas Tabareau. The next 700 syntactical models of type theory. In Yves Bertot and Viktor Vafeiadis, editors, CPP 2017, pages 182-194. ACM, 2017. URL: https://doi.org/10.1145/3018610.3018620.
  8. Douglas Bridges and Fred Richman. Varieties of Constructive Mathematics. London Mathematical Society Lecture Notes Series. Cambridge University Press, 1987. URL: http://books.google.com/books?id=oN5nsPkXhhsC.
  9. L. E. J Brouwer. Begründung der mengenlehre unabhängig vom logischen satz vom ausgeschlossen dritten. zweiter teil: Theorie der punkmengen. Koninklijke Nederlandse Akademie van Wetenschappen te Amsterdam, 12(7), 1919. Google Scholar
  10. Paul J. Cohen. The independence of the continuum hypothesis. the National Academy of Sciences of the United States of America, 50(6):1143-1148, December 1963. Google Scholar
  11. Paul J. Cohen. The independence of the continuum hypothesis ii. the National Academy of Sciences of the United States of America, 51(1):105-110, January 1964. Google Scholar
  12. Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundam. Inform., 100(1-4):43-52, 2010. URL: https://doi.org/10.3233/FI-2010-262.
  13. Thierry Coquand and Guilhem Jaber. A computational interpretation of forcing in type theory. In Peter Dybjer, Sten Lindström, Erik Palmgren, and Göran Sundholm, editors, Epistemology versus Ontology, volume 27 of Logic, Epistemology, and the Unity of Science, pages 203-213. Springer, 2012. URL: https://doi.org/10.1007/978-94-007-4435-6_10.
  14. Thierry Coquand and Bassel Mannaa. The independence of markov’s principle in type theory. In Delia Kesner and Brigitte Pientka, editors, FSCD 2016, volume 52 of LIPIcs, pages 17:1-17:18. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2016. URL: https://doi.org/10.4230/LIPIcs.FSCD.2016.17.
  15. Karl Crary. Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Cornell University, Ithaca, NY, August 1998. Google Scholar
  16. M. J. Cresswell and G. E. Hughes. A New Introduction to Modal Logic. Routledge, 1996. Google Scholar
  17. Michael A. E. Dummett. Elements of Intuitionism. Clarendon Press, second edition, 2000. Google Scholar
  18. VH Dyson and Georg Kreisel. Analysis of Beth’s semantic construction of intuitionistic logic. Stanford University. Applied Mathematics and Statistics Laboratories, 1961. Google Scholar
  19. Michael P. Fourman. Notions of choice sequence. In A.S. Troelstra and D. van Dalen, editors, The L. E. J. Brouwer Centenary Symposium, volume 110 of Studies in Logic and the Foundations of Mathematics, pages 91-105. Elsevier, 1982. URL: https://doi.org/10.1016/S0049-237X(09)70125-9.
  20. Daniel Gratzer, G. A. Kavvos, Andreas Nuyts, and Lars Birkedal. Multimodal dependent type theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS, pages 492-506. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394736.
  21. Daniel Gratzer, Jonathan Sterling, and Lars Birkedal. Implementing a modal dependent type theory. Proc. ACM Program. Lang., 3(ICFP):107:1-107:29, 2019. URL: https://doi.org/10.1145/3341711.
  22. Arend Heyting. Intuitionism: an introduction. North-Holland Pub. Co., 1956. Google Scholar
  23. Guilhem Jaber, Gabriel Lewertowski, Pierre-Marie Pédrot, Matthieu Sozeau, and Nicolas Tabareau. The definitional side of the forcing. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, LICS '16, pages 367-376. ACM, 2016. URL: https://doi.org/10.1145/2933575.2935320.
  24. Stephen C. Kleene and Richard E. Vesley. The Foundations of Intuitionistic Mathematics, especially in relation to recursive functions. North-Holland Publishing Company, 1965. Google Scholar
  25. Georg Kreisel. A remark on free choice sequences and the topological completeness proofs. J. Symb. Log., 23(4):369-388, 1958. URL: https://doi.org/10.2307/2964012.
  26. Georg Kreisel and Anne S. Troelstra. Formal systems for some branches of intuitionistic analysis. Annals of Mathematical Logic, 1(3):229-387, 1970. URL: https://doi.org/10.1016/0003-4843(70)90001-X.
  27. Georg Kreisel and Anne S. Troelstra. Formal systems for some branches of intuitionistic analysis. Annals of mathematical logic, 1(3):229-387, 1970. Google Scholar
  28. Saul A. Kripke. Semantical analysis of modal logic i. normal propositional calculi. Zeitschrift fur mathematische Logik und Grundlagen der Mathematik, 9(5-6):67-96, 1963. URL: https://doi.org/10.1002/malq.19630090502.
  29. Saul A. Kripke. Semantical analysis of intuitionistic logic i. In J.N. Crossley and M.A.E. Dummett, editors, Formal Systems and Recursive Functions, volume 40 of Studies in Logic and the Foundations of Mathematics, pages 92-130. Elsevier, 1965. URL: https://doi.org/10.1016/S0049-237X(08)71685-9.
  30. Joan R. Moschovakis. An intuitionistic theory of lawlike, choice and lawless sequences. In Logic Colloquium'90: ASL Summer Meeting in Helsinki, pages 191-209. Association for Symbolic Logic, 1993. Google Scholar
  31. Christine Paulin-Mohring. Introduction to the Calculus of Inductive Constructions. In Bruno Woltzenlogel Paleo and David Delahaye, editors, All about Proofs, Proofs for All, volume 55 of Studies in Logic (Mathematical logic and foundations). College Publications, January 2015. URL: https://hal.inria.fr/hal-01094195.
  32. Pierre-Marie Pédrot. Russian constructivism in a prefascist theory. In Holger Hermanns, Lijun Zhang, Naoki Kobayashi, and Dale Miller, editors, LICS, pages 782-794. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394740.
  33. Pierre-Marie Pédrot and Nicolas Tabareau. An effectful way to eliminate addiction to dependence. In LICS 2017, pages 1-12. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005113.
  34. Pierre-Marie Pédrot and Nicolas Tabareau. Failure is not an option - an exceptional type theory. In Amal Ahmed, editor, ESOP 2018, volume 10801 of LNCS, pages 245-271. Springer, 2018. URL: https://doi.org/10.1007/978-3-319-89884-1_9.
  35. Pierre-Marie Pédrot and Nicolas Tabareau. The fire triangle: how to mix substitution, dependent elimination, and effects. Proc. ACM Program. Lang., 4(POPL):58:1-58:28, 2020. URL: https://doi.org/10.1145/3371126.
  36. Pierre-Marie Pédrot, Nicolas Tabareau, Hans Jacob Fehrmann, and Éric Tanter. A reasonably exceptional type theory. Proc. ACM Program. Lang., 3(ICFP):108:1-108:29, 2019. URL: https://doi.org/10.1145/3341712.
  37. Andrew M Pitts. Nominal sets: Names and symmetry in computer science, volume 57 of cambridge tracts in theoretical computer science, 2013. Google Scholar
  38. Anne S. Troelstra. Choice sequences: a chapter of intuitionistic mathematics. Clarendon Press Oxford, 1977. Google Scholar
  39. Anne S. Troelstra. Choice sequences and informal rigour. Synthese, 62(2):217-227, 1985. Google Scholar
  40. Mark van Atten and Dirk van Dalen. Arguments for the continuity principle. Bulletin of Symbolic Logic, 8(3):329-347, 2002. URL: http://www.math.ucla.edu/~asl/bsl/0803/0803-001.ps, URL: https://doi.org/10.2178/bsl/1182353892.
  41. Dirk van Dalen. An interpretation of intuitionistic analysis. Annals of mathematical logic, 13(1):1-43, 1978. Google Scholar
  42. Gerrit Van Der Hoeven and Ieke Moerdijk. Sheaf models for choice sequences. Annals of Pure and Applied Logic, 27(1):63-107, 1984. URL: https://doi.org/10.1016/0168-0072(84)90035-6.
  43. Wim Veldman. Understanding and using Brouwer’s continuity principle. In Reuniting the Antipodes — Constructive and Nonstandard Views of the Continuum, volume 306 of Synthese Library, pages 285-302. Springer Netherlands, 2001. URL: https://doi.org/10.1007/978-94-015-9757-9_24.
  44. Beth E. W. Semantic construction of intuitionistic logic. Journal of Symbolic Logic, 22(4):363-365, 1957. 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 Imprint Privacy Contact