Equivalents of disjunctive Markov's principle

Abstract

The purpose of this short note is to point out a rich source of natural equivalents of the weak semi-intuitionistic principle MP${}^{\vee }$ in reverse constructive mathematics: many simple theorems from Euclidean geometry when read classically (for example with $<$ interpreted as $⩽$ and $\ne$) are equivalent to disjunctive Markov's principle MP${}^{\vee }$. We give an example of this phenomenon.