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
12 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 23, 2022 at 7:43 | comment | added | Gro-Tsen | @FrançoisG.Dorais The statement “for all $a\in\mathbb{R}$ there is $u\in[-1,1]$ such that $a=u·|a|$”, which I had initially written in my footnote 1, is equivalent to LLPO (to prove that it is implied by it, just use $u=1$ if $a≥0$ and $u=-1$ if $a≤0$; to see that it implies it, distinguish $u<1$ and $u>-1$ as in the text of the question). If it turns out to be equivalent to CPO, this answers the question. But I don't know how to do it, and I believe not (and at any rate, that's not what I had wanted to write). | |
| Dec 23, 2022 at 0:16 | comment | added | François G. Dorais | The correction doesn't seem necessary to me. Am I missing something? | |
| Dec 22, 2022 at 22:08 | history | edited | Gro-Tsen | CC BY-SA 4.0 |
fix thinko in footnote (as per wlad's comment)
|
| Dec 18, 2022 at 11:53 | comment | added | wlad | Your "alternative form" of CPO is in fact equivalent to LLPO, unconditionally. I haven't been able to show that your "alternative" is equivalent to your original. In fact, I think we have evidence that your original is strictly stronger. | |
| Dec 14, 2022 at 20:12 | comment | added | wlad | Countable Choice + LLPO is enough to imply IVT. Use Countable Choice to define a function $P : \mathbb Q \to \{0,1\}$ so that $P(q) = 1$ implies $f(q) \geq 0$, and $P(q) = 0$ implies $f(q) \leq 0$. Then using $P$, it is possible to do interval bisection without further application of Countable Choice or LLPO. | |
| Dec 14, 2022 at 13:33 | answer | added | Arno | timeline score: 4 | |
| Dec 14, 2022 at 8:53 | comment | added | wlad | @FrançoisG.Dorais I proved that his original form is equivalent to LLPO (assuming DC), so your alternative is much stronger | |
| Dec 14, 2022 at 5:36 | comment | added | François G. Dorais | Quick observation: the "uniform" form of CPO ($\exists f\,\forall x\,x = f(x)|x|$, for example) gives a discontinuous function, so that seemingly stronger form implies at least WLPO. | |
| Dec 13, 2022 at 21:09 | answer | added | wlad | timeline score: 3 | |
| Dec 13, 2022 at 20:49 | comment | added | Hanul Jeon | Could you formulate a binary sequence form of CPO under DC? Many independence results about constructive recursive mathematics use Cauchy reals or binary sequences, so formulating binary sequence version of CPO would be helpful to work on independence results. | |
| Dec 13, 2022 at 20:42 | comment | added | wlad | It seems closer in strength to LLPO than LPO. | |
| Dec 13, 2022 at 20:10 | history | asked | Gro-Tsen | CC BY-SA 4.0 |