Markov's principle

Markov's principle (MP) is a first-order reasoning principle. It states that for any predicate \phi(x)

 	\left(\forall x.\ \phi(x) \lor \lnot \phi(x)\right)
  	\rightarrow   
  \lnot\forall x. \lnot\phi(x)
  	\rightarrow
   \exists x. \phi(x)

In words: if for a decidable predicate \phi(x) it is not true that \phi(x) is false for every x, then there must be some x for which it is true.

This principle is valid in classical logic, but not always true constructively. In particular, it is rejected by Brouwerian intuitionists, but accepted by the Russian school.

Kleene realizability

This principle is obviously reliazable in Kleene realizability, if we reason classically in our informal metatheory.

Let \phi(x) be decidable, and hence realizable. If the realizer e \Vdash \psi(x) does not have the property that y = \phi_e(n)\downarrow and y \Vdash \phi(\underline{n}) for all n \in \mathbb{N}... then there must be some n for which this is false. And in that case, it must be that y \Vdash \lnot\phi(\underline{n}), whence \langle n, y \rangle \Vdash \exists x. \psi(x).

References

• This principle is named for Andrey Markov Jr., not Andrey Markov Sr.