The Independence of Markov’s Principle in Type Theory
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.
Forcing
Dependent type theory
Markov's Principle
Cantor Space
17:1-17:18
Regular Paper
Thierry
Coquand
Thierry Coquand
Bassel
Mannaa
Bassel Mannaa
10.4230/LIPIcs.FSCD.2016.17
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.
http://dx.doi.org/10.2168/LMCS-8(1:29)2012
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.
Errett Bishop. Foundations of Constructive Analysis. McGraw-Hill, 1967.
L. E. J. Brouwer. Essentially negative properties. In A. Heyting, editor, Collected Works, volume I, pages 478 - 479. North-Holland, 1975.
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.
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.
Thierry Coquand and Guilhem Jaber. A note on forcing and type theory. Fundamenta Informaticae, 100(1-4):43-52, 2010.
Peter Dybjer. A general formulation of simultaneous inductive-recursive definitions in type theory. The Journal of Symbolic Logic, 65(2):525-549, 2000.
Martin Hofmann and Thomas Streicher. Lifting grothendieck universes. unpublished note, publication year unknown. URL: http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf.
http://www.mathematik.tu-darmstadt.de/~streicher/NOTES/lift.pdf
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.
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.
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.
Kenneth Kunen. Set Theory: An Introduction to Independence Proofs, volume 102 of Studies in Logic and the Foundations of Mathematics. Elsevier, 1980.
Maurice Margenstern. L’école constructive de Markov. Revue d'histoire des mathématiques, 1(2):271-305, 1995.
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.
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.
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.
William W. Tait. Intensional interpretations of functionals of finite type I. Journal of Symbolic Logic, 32(2):198-212, 1967.
Dirk van Dalen. An interpretation of intuitionistic analysis. Annals of Mathematical Logic, 13(1):1 - 43, 1978.
Andrew K. Wright and Matthias Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38 - 94, 1994.
Chuangjie Xu and Martín Escardó. Universes in sheaf models. University of Birmingham, 2016.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode