nLab
Markov's principle

Markov's Principle

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

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

Compare this to

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

which is a theorem of intuitionistic logic. More generally, a set SS may be called Markovian if this principle holds for all predicates on SS.

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.)

А. А. Марков 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 n,¬P(n)\exists n, \neg{P(n)} if we can actually compute a value of nn such that P(n)P(n) can be proved; since PP is decidable, it's enough to compute nn such that P(n)P(n) is true. And to compute this, you just set a computer working, deciding P(0),P(1),P(2),P(0), P(1), P(2), \ldots, until it finds nn. 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 Cauchy 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 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), and realizability models (e.g. J. van Oosten, Realizability, Elsevier, 2008).

Weak Markov's Principle

More recently, a weakened form of Markov's principle has been identified (first in M. Mandelkern, “Constructively complete finite sets,” Zeitschr. f. math. Logic und Grundlagen d. Math. 34, p. 97-103, 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:

α[β(¬¬n(β(n)=1)¬¬n(α(n)=1β(n)=0))nα(n)=1]. \forall \alpha \; [\forall \beta \; (\neg\neg\exists n \; (\beta(n)=1)\vee \neg\neg\exists n \; (\alpha(n)=1\wedge\beta(n)=0))\rightarrow\exists n \; \alpha(n)=1].

References

For a recent comparison see:

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

Revised on August 1, 2014 01:57:54 by Bas Spitters (62.131.159.150)