Document Open Access Logo

Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle

Authors Mark Bickford , Liron Cohen , Robert L. Constable, Vincent Rahli

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.11.pdf
  • Filesize: 0.74 MB
  • 23 pages

Document Identifiers

Author Details

Mark Bickford
  • Cornell University, Ithaca, NY, USA
Liron Cohen
  • Ben Gurion University of the Negev, Beer Sheva, Israel
Robert L. Constable
  • Cornell University, Ithaca, NY, USA
Vincent Rahli
  • University of Birmingham, UK

Cite AsGet BibTex

Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle. In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 11:1-11:23, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.11

Abstract

One of the differences between Brouwerian intuitionistic logic and classical logic is their treatment of time. In classical logic truth is atemporal, whereas in intuitionistic logic it is time-relative. Thus, in intuitionistic logic it is possible to acquire new knowledge as time progresses, whereas the classical Law of Excluded Middle (LEM) is essentially flattening the notion of time stating that it is possible to decide whether or not some knowledge will ever be acquired. This paper demonstrates that, nonetheless, the two approaches are not necessarily incompatible by introducing an intuitionistic type theory along with a Beth-like model for it that provide some middle ground. On one hand they incorporate a notion of progressing time and include evolving mathematical entities in the form of choice sequences, and on the other hand they are consistent with a variant of the classical LEM. Accordingly, this new type theory provides the basis for a more classically inclined Brouwerian intuitionistic type theory.

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
  • Classical Logic
  • Law of Excluded Middle
  • Theorem proving
  • Coq

Metrics

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

Supplementary Materials

References

  1. Amal J. Ahmed, Andrew W. Appel, and Roberto Virga. A stratified semantics of general references embeddable in higher-order logic. In LICS, page 75. IEEE Computer Society, 2002. URL: https://doi.org/10.1109/LICS.2002.1029818.
  2. Amal Jamil Ahmed. Semantics of Types for Mutable State. PhD thesis, Princeton University, 2004. Google Scholar
  3. 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
  4. Stuart F. Allen. A Non-Type-Theoretic Semantics for Type-Theoretic Language. PhD thesis, Cornell University, 1987. Google Scholar
  5. Stuart F. Allen, Mark Bickford, Robert L. Constable, Richard Eaton, Christoph Kreitz, Lori Lorigo, and Evan Moran. Innovations in computational type theory using Nuprl. J. Applied Logic, 4(4):428-469, 2006. URL: https://doi.org/10.1016/j.jal.2005.10.005.
  6. Abhishek Anand and Vincent Rahli. Towards a formally verified proof assistant. In Gerwin Klein and Ruben Gamboa, editors, ITP 2014, volume 8558 of LNCS, pages 27-44. Springer, 2014. URL: https://doi.org/10.1007/978-3-319-08970-6_3.
  7. Evert Willem Beth. The foundations of mathematics: A study in the philosophy of science. Harper and Row, 1966. Google Scholar
  8. 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.
  9. Mark Bickford, Liron Cohen, Robert L. Constable, and Vincent Rahli. Open bar - a brouwerian intuitionistic logic with a pinch of excluded middle. Extended version of our CSL 2021 paper avaible at https://vrahli.github.io/articles/open-bar-long.pdf, 2020.
  10. Lars Birkedal, Bernhard Reus, Jan Schwinghammer, Kristian Støvring, Jacob Thamsborg, and Hongseok Yang. Step-indexed kripke models over recursive worlds. In Thomas Ball and Mooly Sagiv, editors, POPL, pages 119-132. ACM, 2011. URL: https://doi.org/10.1145/1926385.1926401.
  11. Lars Birkedal, Kristian Støvring, and Jacob Thamsborg. Realisability semantics of parametric polymorphism, general references and recursive types. Mathematical Structures in Computer Science, 20(4):655-703, 2010. URL: https://doi.org/10.1017/S0960129510000162.
  12. 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.
  13. Venanzio Capretta. A polymorphic representation of induction-recursion, 2004. URL: https://www.cs.ru.nl/~venanzio/publications/induction_recursion.ps.
  14. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, Robert W. Harper, Douglas J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. Implementing mathematics with the Nuprl proof development system. Prentice-Hall, Inc., Upper Saddle River, NJ, USA, 1986. Google Scholar
  15. 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.
  16. Thierry Coquand, Bassel Mannaa, and Fabian Ruch. Stack semantics of type theory. In LICS 2017, pages 1-11. IEEE Computer Society, 2017. URL: https://doi.org/10.1109/LICS.2017.8005130.
  17. Karl Crary. Type-Theoretic Methodology for Practical Programming Languages. PhD thesis, Cornell University, Ithaca, NY, August 1998. Google Scholar
  18. Jacques Dubucs and Michel Bourdeau. Constructivity and Computability in Historical and Philosophical Perspective, volume 34. Springer, January 2014. URL: https://doi.org/10.1007/978-94-017-9217-2.
  19. Michael A. E. Dummett. Elements of Intuitionism. Clarendon Press, second edition, 2000. Google Scholar
  20. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. J. Symb. Log., 65(2):525-549, 2000. URL: http://projecteuclid.org/euclid.jsl/1183746062.
  21. VH Dyson and Georg Kreisel. Analysis of Beth’s semantic construction of intuitionistic logic. Stanford University. Applied Mathematics and Statistics Laboratories, 1961. Google Scholar
  22. Martín H. Escardó and Chuangjie Xu. The inconsistency of a Brouwerian continuity principle with the Curry-Howard interpretation. In TLCA 2015, volume 38 of LIPIcs, pages 153-164. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015. URL: https://doi.org/10.4230/LIPIcs.TLCA.2015.153.
  23. Gilda Ferreira and Paulo Oliva. On various negative translations. In Steffen van Bakel, Stefano Berardi, and Ulrich Berger, editors, CL&C, volume 47 of EPTCS, pages 21-33, 2010. URL: https://doi.org/10.4204/EPTCS.47.4.
  24. Arend Heyting. Intuitionism: an introduction. North-Holland Pub. Co., 1956. Google Scholar
  25. Douglas J. Howe. Equality in lazy computation systems. In LICS 1989, pages 198-203. IEEE Computer Society, 1989. Google Scholar
  26. 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
  27. Alexei Kopylov and Aleksey Nogin. Markov’s principle for propositional type theory. In CSL 2001, volume 2142 of LNCS, pages 570-584. Springer, 2001. URL: https://doi.org/10.1007/3-540-44802-0_40.
  28. 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.
  29. Georg Kreisel. On weak completeness of intuitionistic predicate logic. J. Symb. Log., 27(2):139-158, 1962. URL: https://doi.org/10.2307/2964110.
  30. Georg Kreisel. Lawless sequences of natural numbers. Compositio Mathematica, 20:222-248, 1968. Google Scholar
  31. 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.
  32. 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.
  33. 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.
  34. Paul Blain Levy. Possible world semantics for general storage in call-by-value. In Julian C. Bradfield, editor, CSL 2002, volume 2471 of LNCS, pages 232-246. Springer, 2002. URL: https://doi.org/10.1007/3-540-45793-3_16.
  35. Chuck Liang and Dale Miller. Kripke semantics and proof systems for combining intuitionistic logic and classical logic. Ann. Pure Appl. Log., 164(2):86-111, 2013. URL: https://doi.org/10.1016/j.apal.2012.09.005.
  36. 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
  37. Joan Rand Moschovakis. Choice sequences and their uses, 2015. URL: https://www.math.ucla.edu/~joan/stockholm2015handout.pdf.
  38. Joan Rand Moschovakis. Intuitionistic analysis at the end of time. Bulletin of Symbolic Logic, 23(3):279-295, 2017. URL: https://doi.org/10.1017/bsl.2017.25.
  39. Vincent Rahli and Mark Bickford. A nominal exploration of intuitionism. In Jeremy Avigad and Adam Chlipala, editors, CPP 2016, pages 130-141. ACM, 2016. Extended version: http://www.nuprl.org/html/Nuprl2Coq/continuity-long.pdf. URL: https://doi.org/10.1145/2854065.2854077.
  40. Vincent Rahli and Mark Bickford. Validating brouwer’s continuity principle for numbers using named exceptions. Mathematical Structures in Computer Science, pages 1–-49, 2017. URL: https://doi.org/10.1017/S0960129517000172.
  41. Vincent Rahli, Liron Cohen, and Mark Bickford. A verified theorem prover backend supported by a monotonic library. In Gilles Barthe, Geoff Sutcliffe, and Margus Veanes, editors, LPAR-22., volume 57 of EPiC Series in Computing, pages 564-582. EasyChair, 2018. URL: http://www.easychair.org/publications/paper/hp5j.
  42. A. S. Troelstra. Analysing choice sequences. J. Philosophical Logic, 12(2):197-260, 1983. URL: https://doi.org/10.1007/BF00247189.
  43. Anne S. Troelstra. Choice sequences: a chapter of intuitionistic mathematics. Clarendon Press Oxford, 1977. Google Scholar
  44. Anne S. Troelstra. Choice sequences and informal rigour. Synthese, 62(2):217-227, 1985. Google Scholar
  45. A.S. Troelstra. Choice Sequences: A Chapter of Intuitionistic Mathematics. Clarendon Press, 1977. Google Scholar
  46. A.S. Troelstra. A note on non-extensional operations in connection with continuity and recursiveness. Indagationes Mathematicae, 39(5):455-462, 1977. URL: https://doi.org/10.1016/1385-7258(77)90060-9.
  47. Mark van Atten. On Brouwer. Wadsworth Philosophers. Cengage Learning, 2004. Google Scholar
  48. 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.
  49. Dirk van Dalen. An interpretation of intuitionistic analysis. Annals of mathematical logic, 13(1):1-43, 1978. Google Scholar
  50. 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.
  51. 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