Separating Markov's Principles

Markov's principle (MP) is an axiom in some varieties of constructive mathematics, stating that Σ 0 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 Σ 0 1 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 paper, we clarify the status of three natural variants of MP in constructive mathematics, by giving respective equivalence proofs to different formulations of Post's theorem, to stability of termination of computations, to completeness of various proof systems w.r.t. some model-theoretic semantics for Σ 0 1 -theories, and to finiteness principles for both extended natural numbers and trees. The first definition (MP P ) uses a purely propositional definition of Σ 0 1 for predicates on natural numbers N, while the second one (MP B ) relies on functions N → B, and the third one (MP PR ) on a subset of these functions expressible in an explicit model of computation.

We then prove that MP P is strictly stronger than MP B , and that MP B is strictly stronger than MP PR for variants of Martin-Löf's constructive type theory (MLTT), leading to separation results for the above theorems. These separations are achieved through a model construction of MLTT in TT □ C , a type theory parameterised by effects, which can be syntactically restricted as needed. We replicate effectful techniques going back to Kreisel twice to refute different logical principles (first MP B , then MP P ), while simultaneously satisfying variants of those principles (first MP PR , then MP B ) when effects are restricted.

All our results are checked by a proof assistant.