Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ1-propositions (i.e. existential quantification over a decidable predicate on N) are stable under double negation. However, there are various non-equivalent definitions of decidable predicates and thus Σ1-propositions in constructive foundations, leading to non-equivalent Markov's principles. While this fact is well-reported in the literature, it is often overlooked, leading to wrong claims in standard references and published papers.

In this talk, I will illustrate the status of three natural variants of MP in Martin-Löf's constructive type theory (MLTT), by first giving respective equivalence proofs to different formulations of Post's theorem, stability of termination of computations, completeness of various proof systems w.r.t. some model-theoretic semantics for Σ1-theories, and finiteness principles for both extended natural numbers and trees. Afterwards, I describe how these three variants of MP can be separated using effectful models of MLTT, adapting Kreisel’s original proof strategy using free choice sequences to Cohen and Rahli’s framework of stateful type theories.