In constructive mathematics, Markov's principle is the (classically trivial) statement that any infinite sequence of and that is not all s must have a somewhere. Stated in a more logical form, if is a predicate on natural numbers, then
Compare this to
In standard constructive mathematics (such as in the internal logic of a topos), it is possible that the only Markovian sets are the Kuratowski-finite sets. Thus, Markov's principle, stating that the set of natural numbers is Markovian, is nontrivial. (It is true, of course, in a Boolean topos; that is, Markov's principle follows from the principle of excluded middle.)
А. А. Марков Jr? (the one who proved undecidability theorems, and son of the great stochastician) belonged to the Russian school of constructivism, which saw mathematics as about computability. From this perpsective, Markov's principle is justified as follows: We are justified in concluding if we can actually compute a value of such that can be proved; since is decidable, it's enough to compute such that is true. And to compute this, you just set a computer working, deciding , until it finds . Other constructivists find this argument unconvincing, since they're not convinced that the computer will ever stop, even though it's impossible that it continue forever.
Note that the contrapositives of these are all valid regardless of Markov's principle.