Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: ✔ Analytic LPO and real numbers

Madeleine Birchfield (Jan 18 2024 at 04:19):

In constructive mathematics, does the analytic LPO, which states that the Dedekind real numbers have decidable equality, imply that the Dedekind real numbers are equivalent to the Cauchy real numbers, which are equivalence classes of Cauchy sequences of rationals?

Madeleine Birchfield (Jan 18 2024 at 04:51):

The answer to this question is yes. Suppose that the Dedekind real numbers have decidable equality. This implies that the negation of equality $x \neq y$ is a tight apartness relation, which by definition of ordered field implies that

$$x \neq y \iff (x \lt y) \vee (y \lt x)$$

Thus, we have for all $x, y \in \mathbb{R}$ that

$$(x \lt y) \vee (x = y) \vee (x \gt y)$$

and that $(x \lt y) \vee \neg (x \lt y)$.

Auke Booij proved in theorem 6.10.3 of his thesis https://etheses.bham.ac.uk/id/eprint/10411/7/Booij2020PhD.pdf about real analysis that for every Cauchy real number there exists a locator. In dependent type theory, a locator for a real number $x$ is an element of the dependent product

$$\prod_{y:\mathbb{R}} \prod_{z:\mathbb{R}} (y \lt z) \to (y \lt x) + (x \lt z)$$

Then, since $(x \lt y) \vee \neg (x \lt y)$ for all real numbers $x$ and $y$ we could just adapt the proof of Lemma 6.1.3 in his thesis to construct a locator for every Dedekind real number, which by theorem 6.10.3 then implies that every Dedekind real number is a Cauchy real number. Since the Cauchy real numbers embed into the Dedekind real numbers, this implies that the Dedekind and Cauchy real numbers are the same.

Mike Shulman (Jan 18 2024 at 04:57):

According to [[principle of omnsicience]], the analytic LPO is stronger than the statement that the real numbers have decidable equality.

Madeleine Birchfield (Jan 18 2024 at 05:00):

Mike Shulman said:

According to [[principle of omnsicience]], the analytic LPO is stronger than the statement that the real numbers have decidable equality.

Well in section 8.3 of your paper "Brouwer's fixed-point theorem in real-cohesive homotopy type theory" https://arxiv.org/abs/1509.07584 you write that

"The analytic LPO claims that $\mathbb{R}$ has decidable equality."

where $\mathbb{R}$ refers to the Dedekind real numbers throughout your paper.

Mike Shulman (Jan 18 2024 at 05:01):

I follow your argument if $\neq$ refers to the usual apartness relation on the reals, with the statement of analytic LPO being that that relation is decidable, or equivalently trichotomy holds. But I don't follow why decidability of equality implies that disequality coincides with apartness?

Madeleine Birchfield (Jan 18 2024 at 05:05):

So there are apparently two different notions of the analytic LPO used in the literature, depending on what relation one takes to be decidable, the apartness relation or equality.

Mike Shulman (Jan 18 2024 at 05:06):

Interesting. Toby added the stronger version to the nLab page in 2016, after my paper, but he doesn't seem to have remarked on it at the nForum that I can find.

Mike Shulman (Jan 18 2024 at 05:08):

Before that, the page said that the analytic LPO means the reals have decidable equality. I presume Toby decided later for some reason that decidability of apartness was a better notion.

Mike Shulman (Jan 18 2024 at 05:09):

Anyway, does your argument work with the weaker version (decidable equality)?

Madeleine Birchfield (Jan 18 2024 at 05:12):

I'm not sure if it does, but I don't really care about the weaker version if it isn't the same as the stronger version. I just assumed that they were the same because your paper said "decidable equality" while the nLab said "decidable apartness" for the analytic LPO.

Mike Shulman (Jan 18 2024 at 05:13):

If it doesn't, then I guess that might be one reason for preferring the stronger version.

Mike Shulman (Jan 18 2024 at 05:13):

Or, perhaps, depending on one's preference, for preferring the weaker version...

Madeleine Birchfield (Jan 18 2024 at 05:28):

Also, I guess I just assumed that if the negation $\neg P$ of a proposition $P$ is decidable, then the proposition itself is decidable. But that isn't true; the double negation $\neg \neg P$ of any proposition $P$ is always decidable, but $\neg P$ is in general not provable to be decidable.

And that's why there are different versions of the analytic LPO for apartness and for equality.

Notification Bot (Jan 18 2024 at 05:35):

Madeleine Birchfield has marked this topic as resolved.

Graham Manuell (Jan 18 2024 at 11:38):

Madeleine Birchfield said:

Also, I guess I just assumed that if the negation $\neg P$ of a proposition $P$ is decidable, then the proposition itself is decidable. But that isn't true; the double negation $\neg \neg P$ of any proposition $P$ is always decidable, but $\neg P$ is in general not provable to be decidable.

And that's why there are different versions of the analytic LPO for apartness and for equality.

Fwiw, $\neg \neg P$ is not always decidable, but the rest of what you said is true.