Markov's principle
Markov's principle, named after Andrey Markov Jr, is a specific statement in computability theory that is obviously true classically (i.e. it is a logical validity), but must be proved when using constructive mathematics. There are many equivalent formulations of Markov's 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:
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:
for a total recursive function on the natural numbers.
It is equivalent, in the language of real analysis, to the following principles:
...
Wikipedia