Markov's principle

From Wikipedia, the free encyclopedia

Markov's principle, named after Andrey Markov Jr, is a classical tautology that is not intuitionistically valid but that may be justified by constructive means. There are many equivalent formulations of Markov's principle. In predicate logic, it is expressed as $\neg \neg \exists x\;P(x) \rightarrow \exists x\;P(x)$ for $P$ decidable (a predicate is decidable if it is either true or false for all natural numbers). It is equivalent in the language of arithmetic to $\neg \neg \exists x\;f(x)=0 \rightarrow \exists x\;f(x)=0$ for $f$ a total recursive function.

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

For each binary sequence, if it is contradictory that all the terms are equal 0, then there exists a term equal to 1.
For each real number x, if it is contradictory that x equal 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 equal 0, then there exists y ∈ R such that xy = 1.
For each one-one continuous mapping ƒ : [0,1] → R, if x ≠ y, then ƒ(x) ≠ ƒ(y).

Recursive realizability constructively justifies Markov's principle: a realizer is the program that successively checks if $P(0), P(1), P(2),\dots$ is true. The process must stop because $P$ is not everywhere false.

Modified realizability does not justify Markov's principle: 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.

1 Markov's rule
2 Weak Markov's principle
3 See also
4 References
5 External links

[edit] Markov's rule

Markov's rule is the formulation of Markov's principle as a rule. It states that $\exists x\;P(x)$ is derivable as soon as $\neg \neg \exists x\;P(x)$ is, for $P$ decidable. The logician Harvey Friedman showed that Markov's rule is an admissible rule in intuitionistic logic, Heyting arithmetic, and various other intuitionistic theories^[1].

[edit] 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<y) \vee \neg\neg(y<x)) \to 0<x$ .

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

[edit] See also

Church's thesis (constructive mathematics)

[edit] References

^ 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.
^ Kohlenbach, On weak Markov's principle. Mathematical Logic Quarterly (2002), vol 48, issue S1 pp 59-65.