Markov's principle (MP) is a first-order reasoning principle. It states that for any predicate
In words: if for a decidable predicate it is not true that is false for every , then there must be some 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.
This principle is obviously reliazable in Kleene realizability, if we reason classically in our informal metatheory.
Let be decidable, and hence realizable. If the realizer does not have the property that and for all ... then there must be some for which this is false. And in that case, it must be that , whence .