nLab analytic Markov's principle

Idea

In real analysis, there is a principle on the Cauchy real numbers which is equivalent in strength to Markov's principle for natural numbers, and states that the tight apartness relation on the Cauchy real numbers is a stable relation. This principle can be generalised from the Cauchy real numbers to all notions of real numbers, such as the Dedekind real numbers, and is hence called the analytic Markov’s principle. In classical mathematics, all of these are implied by excluded middle; however, in neutral constructive mathematics, the different analytic Markov’s principles are different principles of different strength, because the Cauchy and Dedekind real numbers and any other notion of real numbers between the Cauchy and Dedekind real numbers cannot be proven to coincide.

Definition

There are many different notions of real numbers in constructive mathematics. What all these real numbers have in common are that they are an Archimedean ordered field extension $R$ of the field of (sequential, modulated) Cauchy real numbers $\mathrm{R}_C$; i.e. there are unique ring homomorphisms of ordered fields

$$\mathbb{R}_C \hookrightarrow R \hookrightarrow \mathbb{R}_D$$

where $\mathbb{R}_D$ is the ordered field of Dedekind real numbers - the homomorphism into $\mathbb{R}_D$ always exists since $\mathbb{R}_D$ is the terminal Archimedean ordered field. In general the ring homomorphisms are not provably isomorphisms unless the Dedekind real numbers and Cauchy real numbers coincide. Thus, there are many different notions of the analytic Markov’s principle; the analytic Markov’s principles are defined for each Archimedean ordered field extension of the Cauchy real numbers.

Definition

Let $R$ be an Archimedean ordered field extension of the field of (sequential, modulated) Cauchy real numbers $\mathrm{R}_C$. The analytic Markov’s principle for $R$ states that the pseudo-order on $R$ is a stable relation, or equivalently, the tight apartness relation is a stable relation, or equivalently.

Warning. Given an Archimedean ordered field extension $R$ of the field of (sequential, modulated) Cauchy real numbers, the analytic Markov’s principle for $R$ is not to be confused with the Markov's principle for $R$ - the latter is the statement that for every function $f$ from $R$ to the boolean domain, the existential quantifier “there exists an $x$ in $R$ such that $f(x) = 1$” is stable. For $R$ the Cauchy real numbers, the analytic Markov’s principle for the Cauchy real numbers is equivalent to the Markov’s principle for the natural numbers, while the Markov’s principle for the Cauchy real numbers is much stronger than the Markov’s principle for the natural numbers.

Let $R$ be any Archimedean ordered field extension of the Cauchy real numbers. The analytic Markov’s principle makes sense for any Archimedean ordered local Artinian $R$-algebra $A$ 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. In this case, the analytic Markov’s principle for the Weil $R$-algebra $A$ says that the apartness relation or strict weak order on $A$ is a stable relation, and the quotient of $A$ by its nilradical is the field of real numbers $R$ satisfying the analytic Markov’s principle.

Properties

Theorem

Suppose that there is an Archimedean ordered field $R$ which is a field extension of the Cauchy real numbers $\mathbb{R}_C$. Then the analytic Markov’s principle for $R$ is equivalent to the statement which says that for all elements $x \in R$, $\neg (x \leq 0)$ implies $0 \lt x$, the definition of analytic Markov’s principle in Shulman 2018.

Proof

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$, the analytic Markov’s principle.

Theorem

The analytic Markov’s principle for the (sequential, modulated) Cauchy real numbers $\mathbb{R}_C$ implies Markov’s principle for natural numbers.

Proof

Let $f$ be a function from the natural numbers to the boolean domain. Define the sequence $u$ on the rationals as

$$u(n) = \sum_{x = 0}^k \frac{f(n)}{2^x}$$

This sequence is a Cauchy sequence with a modulus of continuity, so taking the limit of this Cauchy sequence yields a Cauchy real number $[u]$. The analytic Markov’s principle on the Cauchy reals implies that $\neg ([u] = 0)$ implies that $[u] \# 0$. $[u] \# 0$ holds if and only if $[u] \gt \frac{1}{2^k}$ for some natural number $k$ so there exists an $n$ such that $f(n) = 1$, and $[u] = 0$ holds if and only if $f(n) = 0$ for all $n$. Thus, $\neg ([u] = 0)$ implies that $[u] \# 0$ if and only if “$f(n) = 0$ for all $n$” being false implies that “there exists an $n$ such that $f(n) = 1$”, which is Markov’s principle for natural numbers.

Theorem

Suppose that there are two Archimedean ordered fields $R$ and $R'$ such that both are field extensions of the Cauchy real numbers $\mathbb{R}_C$ and $R'$ is a field extension of $R$. Then, the analytic Markov’s principle for $R'$ implies the analytic Markov’s principle for $R$.

Proof

Suppose that the analytic Markov’s principle for $R'$ holds for all elements $x$ and $y$ in $R'$. Then the analytic Markov’s principle holds for all elements $x$ and $y$ in any subset of $R'$ whose subset inclusion preserves and reflects the tight apartness relation, and in particular, it holds for any subfield $R$ of $R'$ which is also a field extension of the Cauchy real numbers.

Lemma

Suppose that there is an Archimedean ordered field $R$ which is a field extension of the Cauchy real numbers $\mathbb{R}_C$. Then, the analytic Markov’s principle for $R$ implies Markov’s principle for natural numbers.

Proof

Since the field of Cauchy real numbers is a (trivial) field extension of itself, the analytic Markov’s principle for $R$ implies the analytic Markov’s principle for the Cauchy real numbers, which implies Markov’s principle for the natural numbers.

Theorem

Markov’s principle for natural numbers implies the analytic Markov’s principle for the (sequential, modulated) Cauchy real numbers $\mathbb{R}_C$.

Proof

TBD…

Lemma

Markov’s principle for natural numbers is equivalent to the analytic Markov’s principle for the (sequential, modulated) Cauchy real numbers $\mathbb{R}_C$.

Thus, one has a hierarchy of analytic Markov’s principles of omniscience, where

• The (sequential-, modulated-, Cantor-, Cauchy-, $\mathbb{R}_C$-) analytic Markov’s principle is the weakest and equivalent to Markov’s principle for the natural numbers;

• The (Dedekind-, $\mathbb{R}_D$-)analytic Markov’s principle is the strongest.

• For any other Archimedean ordered field extension of the Cauchy real numbers $R$ which is neither equivalent to the Cauchy real numbers or the Dedekind real numbers, the $R$-analytic Markov’s principle are intermediate in strength between the Cauchy-analytic Markov’s principle and the Dedekind-analytic Markov’s principle.

Models

• The analytic Markov’s principle for Dedekind real numbers holds in Johnstone’s topological topos.

• The analytic Markov’s principle for Dedekind real numbers holds in the cohesive types of Mike Shulman‘s real-cohesive homotopy type theory, which model Euclidean-topological infinity-groupoids.

See also

• Markov's principle

• axiom of real cohesion

• analytic LPO

• analytic WLPO

• analytic LLPO

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)

• Chris Grossack, Life in Johnstone’s Topological Topos 3 – Bonus Axioms (web)