On Weak Markov's Principle
Ulrich Kohlenbach · Mathematical logic quarterly · 2002
We show that the so-called weak Markov's principle (WMP) which states that every pseudo-positive real number is positive is underivable in 𝒯ω ≔ E-HAω + AC. Since 𝒯ω allows one to formalize (atl eastl arge parts of) Bishop's constructive mathematics, this makes it unlikely that WMP can be proved within the framework of Bishop-style mathematics (which has been open for about 20 years). The underivability even holds if the ine.ective schema of full comprehension (in all types) for negated formulas (in particular for ∃-free formulas) is added, which allows one to derive the law of excluded middle for such formulas.