 Markov’s principle represents an unbounded search: if you have a proof that all terms \(a_n\) being 0 leads to a contradiction, then, by testing the terms \(a_1,a_2,a_3,\ldots\) in turn, you are guaranteed to come across a term equal to 1; but this guarantee does not extend to an assurance that you will find the desired term before the end of the universe. Most practitioners of constructive mathematics view Markov’s principle with at least suspicion, if not downright disbelief. Such views are reinforced by the observation that there is a Kripke Model showing that MP is not constructively derivable (Bridges &amp; Richman [1987], 137–138.)