Thierry Coquand ; Bassel Mannaa - The Independence of Markov's Principle in Type Theory

lmcs:2565 - Logical Methods in Computer Science, August 15, 2017, Volume 13, Issue 3 - https://doi.org/10.23638/LMCS-13(3:10)2017
The Independence of Markov's Principle in Type TheoryArticle

Authors: Thierry Coquand ; Bassel Mannaa

    In this paper, we show that Markov's principle is not derivable in dependent type theory with natural numbers and one universe. One 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. 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.


    Volume: Volume 13, Issue 3
    Published on: August 15, 2017
    Accepted on: June 24, 2017
    Submitted on: August 15, 2017
    Keywords: Computer Science - Logic in Computer Science,F.4.1

    Consultation statistics

    This page has been seen 1427 times.
    This article's PDF has been downloaded 521 times.