Markov's Principle - Realizability

Realizability

Realizability can be used to justify Markov's principle: a realizer is the unbounded search that successively checks if is true. Because is not everywhere false, the search cannot go on forever. Using classical logic one concludes that the search therefore stops, namely at a value at which holds.

Modified realizability does not justify Markov's principle, even if classical logic is used in the meta-theory: there is no realizer in the language of simply typed lambda calculus as this language is not Turing-complete and arbitrary loops cannot be defined in it.