Equivalents of disjunctive Markov's principle

TL;DR

This paper shows that many classical Euclidean geometry theorems are equivalent to the disjunctive Markov's principle MP$^ v$, revealing a deep connection between geometry and constructive logic.

Contribution

It identifies numerous simple Euclidean geometry theorems as equivalent to MP$^ v$ in reverse constructive mathematics.

Findings

Many Euclidean geometry theorems are equivalent to MP$^ v$

Classical interpretations of inequalities relate to logical principles

Highlights the logical strength of geometric theorems in constructive context

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 $\leqslant$ and $\neq$) are equivalent to disjunctive Markov's principle MP$^\vee$. We give an example of this phenomenon.