Markov's Principle - Statements of The 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:

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:

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