Timeline for What is the strength of “if $c≥0$ then $[0,c] = c·[0,1]$” in constructive math (w.r.t., LPO, WLPO, LLPO, etc.)?
Current License: CC BY-SA 4.0
18 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 18, 2022 at 12:00 | comment | added | wlad | This proposal validates everything that's been said so far, and appears to answer Gro Tsen's question. In particular, letting $T$ be the compact subspace of $\mathbb R^2$ for which $0 \leq y \leq x$ and $x \leq 1$, we can show that LLPO is true, CPO is not, and $\varepsilon$-CPO is. While it's not rigorous, it seems very promising to me. | |
| Dec 18, 2022 at 11:57 | comment | added | wlad | @AndrejBauer There appears to be a non-realisability direction to the problem of showing that $LLPO \not\implies CPO$. The statement CPO has the shape $\forall\exists$, and I suspect that this can be given a topological meaning that validates LLPO but not CPO. Namely, (taking $T$ to be a topological space) the semantic meaning of $(\forall x \in T) (\exists y \in T) \phi(x,y)$ can be that there exists a finite closed covering of $T$, for which each closed set can be open-covered, and for each set in the resulting set covering we can attach a continuous function sending $x$ to $y$. | |
| Dec 18, 2022 at 10:29 | comment | added | Andrej Bauer | @Gro-Tsen: thanks for the explanation. Yes, I got my implications reversed, sorry. The shortest explanation of TTE is that it is the relative realizability topos $\mathsf{RT}(\mathbb{N}^\mathbb{N}, (\mathbb{N}^\mathbb{N})_{\mathsf{eff}})$, also known as the Kleene-Vesley topos. | |
| Dec 18, 2022 at 0:10 | comment | added | Gro-Tsen | (In the topos of sheaves over $\mathbb{R}$, compactness of $[0,1]$ holds as I understand the latter statement, but $\mathbf{CPO}$ or even $\mathbf{LLPO}_{\mathbb{R}}$ do not hold. So probably the sentence “we should constructively expect that compactness of $[0,1]$ yields CPO” wasn't intended to mean ②.) | |
| Dec 18, 2022 at 0:07 | comment | added | Gro-Tsen | @AndrejBauer I don't know what “TTE” is, but your above comments appear to be saying that ①compactness of $[0,1]$ holds in TTE (“for free”), and that you expect ②compactness of $[0,1]$ to imply $\mathbf{CPO}$; now since ③$\mathbf{CPO}$ implies $\mathbf{LLPO}_{\mathbb{R}}$ as pointed out in the question, putting together ①, ② and ③ demands that $\mathbf{LLPO}_{\mathbb{R}}$ hold in TTE. But probably ② is not what you meant to say. | |
| Dec 17, 2022 at 15:30 | comment | added | Andrej Bauer | @wlad: Please be explicit about what you are referring to. Did I claim that LLPO is valid in TTE? Where? | |
| Dec 17, 2022 at 15:00 | comment | added | wlad | @AndrejBauer What you said doesn't make sense. TTE does not imply LLPO, so how can it imply CPO? TTE is conservative and computable, and LLPO is non-constructive and uncomputable. | |
| Dec 17, 2022 at 12:47 | comment | added | Andrej Bauer | @Arno: Excellent, this means we should constructively expect that compactness of $[0,1]$ yields CPO. (Note that in TTE compactness of $[0,1]$ is “free” – an artifact of working in a particular realizability model.) | |
| Dec 17, 2022 at 2:18 | comment | added | Arno | @Gro-Tsen I've added the link to an introduction/survey paper on Weihrauch reducibility. | |
| Dec 17, 2022 at 2:17 | history | edited | Arno | CC BY-SA 4.0 |
added background reference on Weihrauch degrees
|
| Dec 17, 2022 at 2:14 | comment | added | Arno | @AndrejBauer Parameterizing LLPO by $\mathbb{N}$ already gives us WKL, which can do CPO and IVT. For all the separations, the restrictions to "finitely many uses" is definitely needed (but the finitely many uses could be sequential in principle). | |
| Dec 16, 2022 at 21:42 | comment | added | wlad | @AndrejBauer What about IVT vs LLPO? Do you know whether they've been separated? | |
| Dec 16, 2022 at 10:17 | comment | added | Andrej Bauer | @Arno, can you prove a stronger result that CPO is not reducible to any parameterization of LLPO (in analogy to Section 2.5 of arxiv.org/pdf/2106.01734.pdf)? (A special case often considered in the Weihrauch land is parametrization by $\mathbb{N}$, which gives countably many instances – but in general we can relace $\mathbb{N}$ by and represented space or an assembly.) | |
| Dec 16, 2022 at 10:15 | comment | added | Andrej Bauer | Arno's result implies that in the internal logic of a topos one cannot derive CPO. If we could, then we could derive LLPO in the Kleene-Vesley topos. It also implies that there is no instance reduction in constructive mathematics from CPO to finitely many instance of LLPO. If there were, we woudl have one in the Kleene-Vesley topos, contradicting Arno's result. So if there is a constructive proof that LLPO implies it CPO, it must be a very unusual one. | |
| Dec 15, 2022 at 9:50 | comment | added | wlad | I'm wondering whether Weihrauch reducibility can help produce a model of choiceless constructivism where CPO is true and IVT is not. Dependent Choice can be restricted to only Turing computable things, and therefore not be applicable to anything that needs CPO to be true. | |
| Dec 14, 2022 at 16:41 | comment | added | Gro-Tsen | I'm not familiar with Weihrauch reducibility, but this seems quite interesting: can you suggest a starting point for someone already familiar with (not-too-fancy) constructive math in general, and with Turing-reducibility if this helps? | |
| Dec 14, 2022 at 15:34 | comment | added | LSpice | The title of that second paper is quite provocative! | |
| Dec 14, 2022 at 13:33 | history | answered | Arno | CC BY-SA 4.0 |