Markov's principle

Markov's principle, named after Andrey Markov Jr, is a conditional existence statement for which there are many equivalent formulations, as discussed below. The principle is logically valid classically, but not in intuitionistic constructive mathematics. However, many particular instances of it are nevertheless provable in a constructive context as well. The principle was first studied and adopted by the Russian school of constructivism, together with choice principles and often with a realizability perspective on the notion of mathematical function. 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 for some input 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, 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. This is not trivially true constructively. For a decidable predicate P over the natural numbers, Markov's principle then reads: That is, if P cannot be false for all natural numbers n, then it is true for some n. Markov's rule is the formulation of Markov's principle as a rule. It states that is derivable as soon as is, for decidable. Formally, Anne Troelstra proved that it is an admissible rule in Heyting arithmetic. Later, 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, using the Friedman translation. Markov's principle is equivalent in the language of arithmetic to: for a total recursive function on the natural numbers. In the presence of Church's thesis principle, the principle is equivalent to its form for primitive recursive functions.