nLab Markov's principle

Definition

In constructive mathematics, Markov's principle is the (classically trivial) statement that any infinite sequence of $0$ and $1$ that is not all $1$s must have a $0$ somewhere. Stated in a more logical form, if $P$ is a predicate on natural numbers, then

$$\forall{n}\, \big(P(n) \vee \neg{P(n)}\big) \Rightarrow \neg\forall{n}\, P(n) \Rightarrow \exists{n}\, \neg{P(n)} .$$

Compare this to

$$\neg\exists{n}\, P(n) \Rightarrow \forall{n}\, \neg{P(n)} ,$$

which is a theorem of intuitionistic logic.

Stated set theoretically, this says that given a subset $P \in \mathcal{P}(\mathbb{N})$, if $P$ is a decidable subset of $\mathbb{N}$ ($P \cup \bar{P} = \mathbb{N}$), then if $\neg (\bar{P} = \mathbb{N})$, then $P$ is inhabited, where, $\bar{P}$ is the complement of $P$.

More generally, a set $S$ may be called Markovian if this principle holds for all predicates or subsets on $S$. Every Kuratowski-finite set is Markovian, for example.

Markov's principle is often stated in terms of infinite sequences of natural numbers, using Greek letters for sequences and Latin letters for individual numbers:

$$\forall{\alpha}\, \big(\neg\forall{n}\, (\alpha_n = 0) \Rightarrow \exists{n}\, (\alpha_n \ne 0)\big) .$$

Here, $P(n)$ is the statement that $\alpha_n = 0$, and the hypothesis $\forall{n} (P(n) \vee \neg{P(n)})$ is true for any sequence of natural numbers. Conversely, given any predicate $P$ satisfying this hypothesis, we can define $\alpha$ by $\alpha_n = 0$ if $P(n)$ is true and $\alpha_n = 1$ if $P(n)$ is false, so the two versions of Markov's principle are equivalent.

In the antithesis interpretation

In the antithesis interpretation of constructive mathematics, propositions are functions from from the boolean domain $\{0,1\}$ to the set of truth values $\Omega$. Given any set $A$ and function $f$ from $A$ to $\{0,1\}$, the antithesis proposition $b \mapsto f(x) = b$ is mutually exclusive and decidable by the induction principle of the boolean domain. As a result, the affine existential quantifier $\bigsqcup_{x \in A} (b \mapsto f(x) = b)$ is mutually exclusive and affirmative and the the affine universal quantifier $\bigsqcap_{x \in A} (b \mapsto f(x) = b)$ is mutually exclusive and refutative. Markov’s principle for $A$ ($MP_A$) states that, given any function $f$ from $A$ to the boolean domain $\{0,1\}$, $\bigsqcup_{x \in A} (b \mapsto f(x) = b)$ is refutative or equivalently $\bigsqcap_{x \in A} (b \mapsto f(x) = b)$ is affirmative.

Discussion

In standard constructive mathematics (such as in the internal logic of a topos), it is possible that the only Markovian sets are the Kuratowski-finite sets. Thus, Markov's principle, stating that the set of natural numbers is Markovian, is nontrivial. (It is true, of course, in a Boolean topos; that is, Markov's principle follows from the principle of excluded middle.)

Andrey Markov Jr (the one who proved undecidability theorems, and son of the great stochastician) belonged to the Russian school of constructivism, which saw mathematics as about computability. From this perspective, Markov's principle is justified as follows: We are justified in concluding $\exists{n}\, \neg{P(n)}$ if we can actually compute a value of $n$ such that $\neg{P(n)}$ can be proved; since $P$ is decidable, it's enough to compute $n$ such that $\neg{P(n)}$ is true. And to compute this, you just set a computer working, deciding $P(0), P(1), P(2), \ldots$, until it finds $n$. Other constructivists find this argument unconvincing, since they're not convinced that the computer will ever stop, even though it's impossible that it continue forever.

Equivalent forms:

• If a Turing machine does not run forever, then it halts.
• If an extended natural number is not infinite, then it is finite.
• If a modulated Cantor real number does not equal zero, then it is apart from zero in that it has a multiplicative inverse.

Note that the contrapositives of these are all valid regardless of Markov's principle.

The other major historical school of constructivism, Brouwer's intuitionism, rejects Markov's principle. Brouwer's viewpoint has since his time been formalized, and via this formalization Markov's principle can be proved false. Namely, Kripke's schema with MP proves Excluded Middle, and Excluded Middle is incompatible with continuity?. Several models have been built satisfying Kripke's schema and continuity, thereby falsifying MP. These include topological models (e.g. M. Krol, “Topological model for intuitionistic analysis with Kripke’s Scheme,“ Zeitschr. f. math. Logic und Grundlagen d. Math. 24, p. 427-436, 1978), Beth models (e.g. D. van Dalen, “ interpretation of intuitionistic analysis,” Annals of Mathematical Logic 13(1), p. 1-43), realizability models (e.g. J. van Oosten, Realizability, Elsevier, 2008), and a Kripke model BridgesRichman, p138. Note however that some intuitionists have advocated in favour of Markov's principle (and presumably then against Kripke's schema).

Weak Markov's Principle

More recently, a weakened form of Markov's principle has been identified (first in (Mandelkern 1988)) and seen to be of interest, aptly named Weak Markov's Principle. It states that if a binary sequence is pseudo-positive then it is positive:

$$\forall \alpha \, \Big(\forall \beta \, \Big(\neg\neg\exists n \, (\beta(n)=1)\vee \neg\neg\exists n \, \big((\alpha(n)=1)\wedge(\beta(n)=0)\big)\Big)\rightarrow\exists n \, (\alpha(n)=1)\Big).$$

Analytic Markov's Principle

Markov's principle is equivalent to the assertion that for every modulated Cantor real number $a$, if $a \leq 0$ is false, then $a \gt 0$. Another way to say this is that the standard tight apartness relation on modulated Cantor reals is a stable relation.

The analogous statement for Dedekind real numbers might be called the analytic Markov's principle, by analogy with the analytic LPO. The Russian constructivists, who used Markov's principle most, accepted countable choice, or at least $AC_{0,0}$, which implies that these two principles are equivalent. However, in other varieties of constructive mathematics, the analytic Markov's principle is stronger.

Choiceless Markov’s principle

There is another generalization of Markov’s principle defined in King 2024, which was suggested to be called choiceless Markov’s principle. The choiceless Markov’s principle for a set $A$ states that given a set $A$ and a pair of predicates $P$ and $Q$ such that $P(x) \vee Q(x)$ holds for all $x \in A$, then if it is not true that for all $x \in A$, $Q(x)$, then there exists $x \in A$ such that $P(x)$.

$$\forall x \in A.P(x) \vee Q(x) \Rightarrow (\neg \forall x \in A.Q(x)) \Rightarrow \exists x \in A.P(x))$$

The idea behind the term “choiceless” is that one isn’t forced to choose between $P(x)$ or $Q(x)$ in this version of the Markov’s principle. One gets back the usual Markov’s principle if $P(x)$ and $Q(x)$ are mutually exclusive propositions for all $x \in A$, from which $Q(x)$ if and only if $\neg P(x)$ for all $x \in A$.

We can also state the principle set-theoretically. Given a set $A$, the choiceless Markov’s principle for $A$ states that given subsets $P, Q \in \mathcal{P}(A)$, if $P \cup Q = A$, then if $\neg (Q = A)$, then $P$ is inhabited. One gets back the usual Markov’s principle if $P$ and $Q$ are disjoint subsets $P \cap Q = \emptyset$, from which $Q = \bar{P}$, where $\bar{P}$ is the complement of $P$.

The choiceless Markov’s principle for the natural numbers $\mathbb{N}$ implies the analytic Markov's principle for all sets of real numbers, as shown in King 2024.

Related concepts

• principle of omniscience

• limited principle of omniscience

• weak limited principle of omniscience

• lesser limited principle of omniscience

• double negation law

References

• Mark Mandelkern, Constructively Complete Finite Sets, Mathematical Logic Quarterly 34, issue 2 (1988) 97–103, doi:10.1002/malq.19880340202.

• Henri Lombardi, Claude Quitté (2010): Commutative algebra: Constructive methods (Finite projective modules) Translated by Tania K. Roblo, Springer (2015) (doi:10.1007/978-94-017-9944-7, pdf)

• Hannes Diener, Constructive reverse mathematics, Habilitationsschrift Fakultät IV - Naturwissenschaftlich-Technische Fakultät, 2018. (arXiv:1804.05495, dspace:ubsi/1306)

• Felix Cherubini, Thierry Coquand, Freek Geerligs, Hugo Moeneclaey, A Foundation for Synthetic Stone Duality (arXiv:2412.03203)

• Christopher King, What are these generalizations of the principles of omniscience called?, MathOverflow, 15 February 2024. (web)

For a recent comparison see:

• Matt Hendtlass and Robert Lubarsky, Separating fragments of WLEM, LPO, and MP, PDF.

• Douglas Bridges and Fred Richman, Varieties of Constructive Mathematics.

category: foundational axiom