The Independence of Markov's Principle in Type Theory

Thierry Coquand, Bassel Mannaa

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer review


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 [HS99, Str05, XE16]. 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.
Titel1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016) : Leibniz International Proceedings in Informatics
ForlagDagstuhl Publishing, Germany
Publikationsdato15 feb. 2016
StatusUdgivet - 15 feb. 2016
Udgivet eksterntJa


  • cs.LO
  • F.4.1