constructive mathematics and the Markov principle

Someone asked me recently about constructivism in mathematics, which led me to the Douglas Bridges’ article in Stanford Encyclopedia of Philosophy on constructive mathematics. What is constructivism? It is a philsophy of mathematics that “asserts that it is necessary to find (or “construct”) a mathematical object to prove that it exists” (wikipedia), as opposed to classical mathematics where it is enough to assume that the object does not exist and derive a contradiction.

In the Bridges’ article, I found a priceless illustrative example, the Markov Principle (MP):

For each binary sequence (an), if it is contradictory that all the terms an equal 0, then there exists a term equal to 1.


Markov’s Principle represents an unbounded search: if you have a proof that all terms an being 0 leads to a contradiction, then, by testing the terms a1,a2,a3, 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. 

[Photomedia Forum post by T.Neugebauer from  May 6, 2006 ]