eng
Schloss Dagstuhl – Leibniz-Zentrum für Informatik
Leibniz International Proceedings in Informatics
1868-8969
2016-06-17
17:1
17:18
10.4230/LIPIcs.FSCD.2016.17
article
The Independence of Markov’s Principle in Type Theory
Coquand, Thierry
Mannaa, Bassel
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.
https://drops.dagstuhl.de/storage/00lipics/lipics-vol052-fscd2016/LIPIcs.FSCD.2016.17/LIPIcs.FSCD.2016.17.pdf
Forcing
Dependent type theory
Markov's Principle
Cantor Space