nLab analytic Markov's principle

Definition

The analytic Markov’s principle states that the pseudo-order on the Dedekind real numbers is a stable relation: for all real numbers $r \in \mathbb{R}$ and $s \in \mathbb{R}$, $\neg \neg (r \lt s)$ implies $r \lt s$.

This is equivalent to the usual formulation of the analytic Markov’s principle, which says that for all real numbers $x \in \mathbb{R}$, $\neg (x \leq 0)$ implies $0 \lt x$. For if we take $x = s - r$, this becomes $\neg (s - r \leq 0)$ implies $0 \lt s - r$, and by the order and arithmetic properties of the real numbers, this is equivalent to $\neg (s \leq r)$ implies $r \lt s$, which is the same as $\neg \neg (r \lt s)$ implies $r \lt s$.

Other equivalent statements include that the tight apartness relation on the Dedekind real numbers is a stable relation.

The analytic Markov’s principle makes sense for any ordered local Artinian $\mathbb{R}$-algebra as well, where the relation $\lt$ is in general only a strict weak order instead of a pseudo-order, the preorder $\geq$ is not a partial order, and the equivalence relation $a \approx b$ derived from the preorder holds if and only if $a - b$ is nilpotent. The quotient of the Weil $\mathbb{R}$-algebra by its nilradical is the Dedekind real numbers satisfying the analytic Markov’s principle.

See also

• Markov's principle

• axiom of real cohesion

• intermediate value theorem

References

• Mike Shulman, Brouwer’s fixed-point theorem in real-cohesive homotopy type theory, Mathematical Structures in Computer Science Vol 28 (6) (2018): 856-941 (arXiv:1509.07584, doi:10.1017/S0960129517000147)