Document Open Access Logo

The Independence of Markov’s Principle in Type Theory

Authors Thierry Coquand, Bassel Mannaa

PDF
Thumbnail PDF

File

LIPIcs.FSCD.2016.17.pdf
  • Filesize: 0.6 MB
  • 18 pages

Document Identifiers

Author Details

Thierry Coquand
Bassel Mannaa

Cite As Get BibTex

Thierry Coquand and Bassel Mannaa. The Independence of Markov’s Principle in Type Theory. In 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016). Leibniz International Proceedings in Informatics (LIPIcs), Volume 52, pp. 17:1-17:18, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2016) https://doi.org/10.4230/LIPIcs.FSCD.2016.17

Abstract

In this paper, we show that Markov's principle is not derivable in
dependent type theory with natural numbers and one universe. One
tentative way to prove this would be to remark that Markov's principle
does not hold in a sheaf model of type theory over Cantor space, since
Markov's principle does not hold for the generic point of this model.
It is however not clear how to interpret the universe in a sheaf
model. Instead we design an extension of type theory, which
intuitively extends type theory by the addition of a generic point of
Cantor space. We then show the consistency of this extension by a
normalization argument. Markov's principle does not hold in this
extension, and it follows that it cannot be proved in type theory.

Subject Classification

Keywords
  • Forcing
  • Dependent type theory
  • Markov's Principle
  • Cantor Space

Metrics

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

References

  1. Andreas Abel and Gabriel Scherer. On irrelevance and algorithmic equality in predicative type theory. Logical Methods in Computer Science, 8(1):1-36, 2012. URL: http://dx.doi.org/10.2168/LMCS-8(1:29)2012.
  2. Peter Aczel. On relating type theories and set theories. In Thorsten Altenkirch, Bernhard Reus, and Wolfgang Naraschewski, editors, Types for Proofs and Programs: International Workshop, TYPES' 98 Kloster Irsee, Germany, March 27-31, 1998 Selected Papers, pages 1-18, Berlin, Heidelberg, 1999. Springer Berlin Heidelberg. Google Scholar
  3. Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967. Google Scholar
  4. L. E. J. Brouwer. Essentially negative properties. In A. Heyting, editor, Collected Works, volume I, pages 478 - 479. North-Holland, 1975. Google Scholar
  5. Paul J Cohen. The independence of the continuum hypothesis. Proceedings of the National Academy of Sciences of the United States of America, 50(6):1143-1148, 12 1963. Google Scholar
  6. Robert L. Constable and Scott Fraser Smith. Partial objects in constructive type theory. In Proceedings of Second IEEE Symposium on Logic in Computer Science, pages 183-193, 1987. Google Scholar
  7. Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundamenta Informaticae, 100(1-4):43-52, 2010. Google Scholar
  8. Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525-549, 2000. Google Scholar
  9. Martin Hofmann and Thomas Streicher. Lifting grothendieck universes. unpublished note, publication year unknown. URL: http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
  10. J.M.E. Hyland and C.-H.L. Ong. Modified realizability toposes and strong normalization proofs (extended abstract). In Typed Lambda Calculi and Applications, LNCS 664, pages 179-194. Springer-Verlag, 1993. Google Scholar
  11. Alexei Kopylov and Aleksey Nogin. Markov’s principle for propositional type theory. In Laurent Fribourg, editor, Computer Science Logic: 15th International Workshop, CSL 2001 10th Annual Conference of the EACSL Paris, France, September 10-13, 2001, Proceedings, pages 570-584, Berlin, Heidelberg, 2001. Springer Berlin Heidelberg. Google Scholar
  12. Georg Kreisel. Interpretation of analysis by means of constructive functionals of finite types. In A. Heyting, editor, Constructivity in Mathematics, pages 101-128. Amsterdam, North-Holland Pub. Co., 1959. Google Scholar
  13. Kenneth Kunen. Set Theory: An Introduction to Independence Proofs, volume 102 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1980. Google Scholar
  14. Maurice Margenstern. L’école constructive de Markov. Revue d'histoire des mathématiques, 1(2):271-305, 1995. Google Scholar
  15. Per Martin-Löf. An intuitionistic theory of types. reprinted in Twenty-five years of constructive type theory, Oxford University Press, 1998, 127-172, 1972. Google Scholar
  16. Ulf Norell. Towards a practical programming language based on dependent type theory. PhD thesis, Department of Computer Science and Engineering, Chalmers University of Technology, SE-412 96 Göteborg, Sweden, September 2007. Google Scholar
  17. Thomas Streicher. Universes in toposes. In Laura Crosilla and Peter Schuster, editors, From Sets and Types to Topology and Analysis: Towards practicable foundations for constructive mathematics, pages 78-90. Oxford University Press, 2005. Google Scholar
  18. William W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198-212, 1967. Google Scholar
  19. Dirk van Dalen. An interpretation of intuitionistic analysis. Annals of Mathematical Logic, 13(1):1 - 43, 1978. Google Scholar
  20. Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38 - 94, 1994. Google Scholar
  21. Chuangjie Xu and Martín Escardó. Universes in sheaf models. University of Birmingham, 2016. 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