The Independence of Markov's Principle in Type Theory

TL;DR

This paper demonstrates that Markov's principle cannot be derived in dependent type theory with natural numbers and one universe by extending the theory with a generic point of Cantor space and proving its consistency.

Contribution

It introduces a new extension of type theory with a generic point of Cantor space and proves that Markov's principle is independent of the base theory.

Findings

Markov's principle does not hold in the sheaf model over Cantor space.

The extended type theory with a generic point is consistent.

Markov's principle cannot be proved in the original type theory.

Abstract

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.