Markov's principle

An artistic representation of a Turing machine. Markov's principle says that if it is impossible that a Turing machine will not halt, then it must halt.

Markov's principle, named after Andrey Markov Jr, is a specific statement in computability theory that is obvious true classically (i.e. it is a tautology), but must be proved when using constructive mathematics. There are many equivalent formulations of Markov's principle.

Statements of the principle

In the language of computability theory, Markov's principle is a formal expression of the claim that if it is impossible that an algorithm does not terminate, then it does terminate. This is equivalent to the claim that if a set and its complement are both computably enumerable, then the set is decidable.

In predicate logic, if P is a predicate over the natural numbers, it is expressed as:

$(\forall n(P(n)\vee \neg P(n))\wedge (\neg \forall n\neg P(n)))\rightarrow (\exists n\;P(n)).$

That is, if P is decidable, and it cannot be false for every natural number n, then it is true for some n. (In general, a predicate P over some domain is called decidable if for every x in the domain, either P(x) is true, or P(x) is not true, which is not always the case constructively.)

It is equivalent in the language of arithmetic to:

$\neg \neg \exists n\;f(n)=0\rightarrow \exists n\;f(n)=0,$

for $f$ a total recursive function on the natural numbers.

It is equivalent, in the language of real analysis, to the following principles:

• For each real number x, if it is contradictory that x is equal to 0, then there exists y ∈ Q such that 0 < y < |x|, often expressed by saying that x is apart from, or constructively unequal to, 0.
• For each real number x, if it is contradictory that x is equal to 0, then there exists y ∈ R such that xy = 1.

Realizability

Realizability can be used to justify Markov's principle: a realizer is the unbounded search that successively checks if $P(0),P(1),P(2),\dots$ is true. Because $P$ is not everywhere false, the search cannot go on forever. Using classical logic one concludes that the search therefore stops, namely at a value at which $P$ holds.

Modified realizability does not justify Markov's principle, even if classical logic is used in the meta-theory: there is no realizer in the language of simply typed lambda calculus as this language is not Turing-complete and arbitrary loops cannot be defined in it.

Markov's rule

Markov's rule is the formulation of Markov's principle as a rule. It states that $\exists n\;P(n)$ is derivable as soon as $\neg \neg \exists n\;P(n)$ is, for $P$ decidable. It was proved by Anne S. Troelstra[1] that Markov's rule is an admissible rule in Heyting arithmetic. Later on, the logician Harvey Friedman showed that Markov's rule is an admissible rule in all of intuitionistic logic, Heyting arithmetic, and various other intuitionistic theories,[2] using the Friedman translation.

Weak Markov's principle

A weaker form of Markov's principle may be stated in the language of analysis as

$\forall x\in {\mathbb {R}}\ (\forall y\in {\mathbb {R}}\ \neg \neg (0

This form can be justified by Brouwer's continuity principles, whereas the stronger form contradicts them. Thus it can be derived from intuitionistic, realizability, and classical reasoning, in each case for different reasons, but this principle is not valid in the general constructive sense of Bishop.[3]

References

1. ^ Anne S. Troelstra. Metamathematical Investigation of Intuitionistic Arithmetic and Analysis, Springer Verlag (1973), Theorem 4.2.4 of the 2nd edition.
2. ^ Harvey Friedman. Classically and Intuitionistically Provably Recursive Functions. In Scott, D. S. and Muller, G. H. Editors, Higher Set Theory, Volume 699 of Lecture Notes in Mathematics, Springer Verlag (1978), pp. 21–28.
3. ^ Ulrich Kohlenbach, "On weak Markov's principle". Mathematical Logic Quarterly (2002), vol 48, issue S1, pp. 59–65.