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

Andrew Swan (Jan 18 2024 at 14:57):

Analytic LPO should say that every real number is either equal to zero or apart from zero. To say every real number is equal to zero or not equal to zero would be analytic WLPO (which implies the WLPO with binary sequences, but not LPO).

Madeleine Birchfield (Jan 18 2024 at 15:02):

Graham Manuell said:

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

Right. That's only the case if weak excluded middle is true (which incidentally implies that $\neg P$ is decidable, because $\neg P$ is the same as $\neg \neg \neg P$. But even if weak excluded middle is true, it is still not provable that $\neg P$ being decidable implies that $P$ is decidable, which is the relevant situation here, where $P$ is apartness of reals and $\neg P$ is equality of reals.

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

Also, does the statement that the locale of real numbers is spatial imply the analytic LPO?

Andrew Swan (Jan 18 2024 at 16:26):

Function realizability satisfies both dependent choice and the fan theorem, which should probably be enough to show the locale of real numbers has enough points, but it does not satisfy LPO (which is equivalent to analytic LPO here because countable choice holds).

Madeleine Birchfield (Jan 18 2024 at 16:58):

Okay, then does the locale of real numbers having enough points imply that the Dedekind and Cauchy real numbers coincide?

Andrew Swan (Jan 18 2024 at 21:25):

You can use a result in an old paper by Fourman and Grayson https://doi.org/10.1016/S0049-237X(09)70126-0 . They showed (section 4) the formal real numbers have enough points iff the space [0, 1] is compact. Another paper from around the same time by Fourman and Hyland https://doi.org/10.1007/BFb0061823 shows (theorem 3.2) this is true in any spartial topos. There are many spatial toposes where the Dedekind reals and Cauchy reals are different, e.g. sheaves on the reals, which is also in the Fourman and Hyland paper.

Andrew Swan (Jan 19 2024 at 09:42):

I realised this morning there should a better way of looking at this. Since $\mathrm{Sh}(\mathbb{R})$ is the classifying topos for Dedekind cuts, the internal locale of formal reals should have enough points automatically, I think.

Madeleine Birchfield (Feb 29 2024 at 15:49):

Is the analytic LPO sufficient to prove the fundamental theorem of algebra for the Dedekind complex numbers $\mathbb{C} \coloneqq \mathbb{R}[i]/(i^2 + 1)$?

Andrew Swan (Feb 29 2024 at 16:02):

Analytic LPO would be enough to show every Dedekind real is a Cauchy real, right? So then you can apply the fundamental theorem of algebra for Cauchy reals from this Ruitenburg paper https://ncatlab.org/nlab/files/Ruitenberg-Roots.pdf since analytic LPO would also show the polynomial has a well defined degree.