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: LPO and sigma-frame structure on booleans

Madeleine Birchfield (Jun 23 2024 at 12:11):

We're working in constructive mathematics so that the set of booleans isn't provably a frame.

What's the relationship between the limited principle of omniscience for natural numbers and the statement that the set of booleans forms a sigma-frame - that it has natural-number-indexed disjunctions that distribute over conjunction?

Andrew Swan (Jun 23 2024 at 14:53):

It's equivalent to WLPO, if I understand the question right - because the join of countably many booleans is 0 iff each boolean in the sequence is equal to 0, and the join has to be either 0 or 1.

Madeleine Birchfield (Jun 23 2024 at 17:34):

If so, then WLPO would be the weakest axiom for which one can construct (a version of) the Dedekind real numbers using the booleans - since a sigma-frame is sufficient for the Dedekind cut construction.

Madeleine Birchfield (Jun 23 2024 at 18:57):

So I'm guessing that LPO is equivalent to the booleans having countable meets in addition to countable joins.

Andrew Swan (Jun 23 2024 at 20:10):

I'm not sure if this is what you mean, but WLPO would be enough to show that defining the Dedekind real numbers with only decidable cuts gives a Cauchy complete field, I think.

Andrew Swan (Jun 23 2024 at 20:12):

WLPO would also be enough to get countable meets. LPO says that if $\bigvee_{i \in \mathbb{N}} s_i = \top$ then $s_i = \top$ for some $i$.

Madeleine Birchfield (Jun 23 2024 at 20:30):

Andrew Swan said:

I'm not sure if this is what you mean, but WLPO would be enough to show that defining the Dedekind real numbers with only decidable cuts gives a Cauchy complete field, I think.

Yeah, that's what I mean. The resulting field is also Dedekind complete in the sense that if one tried the Dedekind real number construction using decidable cuts on the new field one would get an isomorphic field.

Madeleine Birchfield (Jun 23 2024 at 22:49):

But I think that LPO guarantees that the real numbers constructed here also have decidable strict order, because the strict order relation on the real numbers is defined as an existential quantifier in the rationals, which is decidable if LPO holds.

While WLPO only guarantees that these real numbers have decidable equality.

Andrew Swan (Jun 24 2024 at 08:04):

Right, I agree.

Madeleine Birchfield (Jun 24 2024 at 20:21):

I think we might be able to prove that the higher inductive Cauchy reals constructed in section 11.3 of the HoTT book are a discrete type in real-cohesive HoTT like the usual Cauchy reals, assuming crisp LEM and C1. (I asked @Mike Shulman about this a few years ago but he didn't know how to prove it at the time.)

The idea is that the LPO for natural numbers holds for cohesive types in real-cohesive HoTT if crisp LEM and C1 holds, according to theorem 8.29 in Shulman's Brouwer's fixed point theorem in real-cohesive HoTT paper. Let us use $\mathbb{R}_C$ for the Cauchy real numbers, $\mathbb{R}_H$ for the higher inductive type reals defined in section 11.3 of the HoTT book, $\mathbb{R}_2$ for the Dedekind real numbers constructed using decidable Dedekind cuts, which is allowed because LPO implies that the booleans are a sigma-frame, and $\mathbb{R}_D$ for the usual Dedekind real numbers. We have inclusions of Archimedean ordered fields

$$\mathbb{R}_C \subseteq \mathbb{R}_H \subseteq \mathbb{R}_2 \subseteq \mathbb{R}_D$$

The LPO also implies that $\mathbb{R}_2$ has decidable strict order, which is the analytic LPO for $\mathbb{R}_2$, which in turns implies that $\mathbb{R}_2$ is isomorphic to both $\mathbb{R}_C$ and $\mathbb{R}_H$ in the cohesive mode via the proof in corollary 11.4.3 in the HoTT book. Since C1 implies that $\mathbb{R}_C$ is a discrete type by theorem 8.26, this implies that $\mathbb{R}_H$ is a discrete type too.

This also implies that $\mathbb{R}_C$ is Cauchy complete in the cohesive mode with only crisp excluded middle. One doesn't need the full crisp axiom of choice as used in theorem 8.27.

However, the other three notions of real numbers are still not equivalent to the usual Dedekind real numbers if $\mathbb{R} \flat$ holds.

Andrew Swan (Jun 24 2024 at 21:15):

I think there should also be a more direct proof also using Lemma 11.4.1 in the HoTT book - you first show that LPO implies analytic LPO (or maybe just WLPO) for the Cauchy reals, then use the argument of 11.4.1 to explicitly define a "canonical" Cauchy sequence for each Cauchy real, which can then be used to show the Cauchy reals are Cauchy complete, which implies they are the same as the HIT Cauchy reals.
But I like your proof idea - the decidable Dedekind reals are an interesting construction.

Madeleine Birchfield (Jun 24 2024 at 22:45):

I wonder if the booleans being a sigma-frame also implies that it is the initial sigma-frame? Because then the decidable Dedekind reals is simply the Dedekind reals constructed using the initial sigma-frame as discussed in section 11.2 of the HoTT book.

Graham Manuell (Jun 25 2024 at 05:11):

De Morgan's law implies the two-element Boolean algebra is a frame, but it is only the initial frame if excluded middle holds. Presumably something similar happens for sigma-frames.

Madeleine Birchfield (Jun 25 2024 at 12:01):

Andrew Swan said:

But I like your proof idea - the decidable Dedekind reals are an interesting construction.

I also wonder if the decidable Dedekind reals is also the type $\flat \mathbb{R}$ in real-cohesive HoTT assuming crisp LEM.

Madeleine Birchfield (Jun 25 2024 at 12:02):

Graham Manuell said:

De Morgan's law implies the two-element Boolean algebra is a frame, but it is only the initial frame if excluded middle holds. Presumably something similar happens for sigma-frames.

I think in this situation the analogue of de Morgan's law is WLPO and the analogue of excluded middle is LPO.

Andrew Swan (Jun 25 2024 at 15:07):

Yes, that works. The subobject classifier $\Omega$ is always a frame, there is at most one frame homomorphism $2 \to \Omega$ and if it exists it has to send $0$ to $\bot$ and $1$ to $\top$. This map preserves joins iff the condition I mentioned above holds (if $\bigvee_{i \in \mathbb{N}} s_i = \top$ then there exists $i$ such that $s_i = \top$), which is equivalent to LPO.

Madeleine Birchfield (Jun 26 2024 at 19:58):

Madeleine Birchfield said:

I think we might be able to prove that the higher inductive Cauchy reals constructed in section 11.3 of the HoTT book are a discrete type in real-cohesive HoTT like the usual Cauchy reals, assuming crisp LEM and C1. (I asked Mike Shulman about this a few years ago but he didn't know how to prove it at the time.)

The idea is that the LPO for natural numbers holds for cohesive types in real-cohesive HoTT if crisp LEM and C1 holds, according to theorem 8.29 in Shulman's Brouwer's fixed point theorem in real-cohesive HoTT paper.

The LPO for natural numbers still holds for cohesive types in real-cohesive HoTT if crisp LPO for natural numbers (and C1) holds, since the proof of theorem 8.29 only relies on crisp LPO for natural numbers rather than the full crisp LEM.

Madeleine Birchfield said:

Also, by theorem 8.28 we have that the Cauchy reals is isomorphic to $\flat \mathbb{R}$ in real-cohesive HoTT assuming crisp LEM, so we also have that the decidable Dedekind reals are isomorphic to $\flat \mathbb{R}$ - they are the Dedekind reals in classical mathematics, equipped with the discrete topology.

Theorem 8.28 relies on theorem 6.33, which relies on theorem 6.32, which can be proven using only the weaker crisp analytic LPO for Dedekind reals instead of full crisp LEM or countable choice, along with C1. So crisp analytic LPO and C1 is sufficient to get

$\mathbb{R}_C \simeq \mathbb{R}_H \simeq \mathbb{R}_2 \simeq \flat \mathbb{R}_D$

However, I suspect other theorems from the Shulman paper might need more - for example Corollary 11.7 will probably need at least the Heine-Borel theorem, so that continuous functions are uniformly continuous. While some like theorems 8.12, 8.32, and 12.3 probably need the full strength of crisp LEM.