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
21 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Dec 14, 2022 at 20:36 | history | edited | wlad | CC BY-SA 4.0 |
clarification
|
| Dec 14, 2022 at 20:21 | history | edited | wlad | CC BY-SA 4.0 |
added 404 characters in body
|
| Dec 14, 2022 at 20:16 | history | edited | wlad | CC BY-SA 4.0 |
added 404 characters in body
|
| Dec 14, 2022 at 15:39 | comment | added | LSpice | The article referenced by @SamSanders: Rathjen and Chen - Lifschitz realizability for intuitionistic Zermelo-Fraenkel set theory. | |
| Dec 14, 2022 at 15:38 | history | edited | LSpice | CC BY-SA 4.0 |
Name of paper; $-$ -> $\text-$
|
| Dec 14, 2022 at 12:54 | history | edited | wlad | CC BY-SA 4.0 |
deleted 38 characters in body
|
| Dec 14, 2022 at 12:45 | history | edited | wlad | CC BY-SA 4.0 |
added 17 characters in body
|
| Dec 14, 2022 at 12:39 | history | edited | wlad | CC BY-SA 4.0 |
formatting
|
| Dec 14, 2022 at 12:34 | comment | added | wlad | @SamSanders Link? | |
| Dec 14, 2022 at 12:34 | history | edited | wlad | CC BY-SA 4.0 |
formatting
|
| Dec 14, 2022 at 12:27 | comment | added | wlad | @Gro-Tsen Yes, that's right. | |
| Dec 14, 2022 at 10:40 | comment | added | Sam Sanders | There is a paper by Michael Rathjen and Ray-Ming Chen about LLPO in the absence of choice (see google). | |
| Dec 14, 2022 at 9:50 | history | edited | François G. Dorais | CC BY-SA 4.0 |
extra clarification since some very weak systems have limited induction
|
| Dec 14, 2022 at 9:30 | comment | added | Gro-Tsen | Just to be sure, what you call $ε\mathbf{CPO}$ is the statement that: “for all $0≤x≤c$ there exist $0 ≤ t_1 ≤ t_2 ≤ 1$ with $t_2-t_1≤ ε$ such that $c·t_1 ≤ x ≤ c·t_2$”, is this correct? | |
| Dec 14, 2022 at 9:15 | history | edited | wlad | CC BY-SA 4.0 |
deleted 2 characters in body
|
| Dec 14, 2022 at 9:03 | history | edited | wlad | CC BY-SA 4.0 |
added 346 characters in body
|
| Dec 13, 2022 at 22:10 | history | edited | wlad | CC BY-SA 4.0 |
added 249 characters in body
|
| Dec 13, 2022 at 21:36 | history | edited | wlad | CC BY-SA 4.0 |
added 168 characters in body
|
| Dec 13, 2022 at 21:27 | history | edited | wlad | CC BY-SA 4.0 |
added 3 characters in body
|
| Dec 13, 2022 at 21:15 | history | edited | wlad | CC BY-SA 4.0 |
added 77 characters in body
|
| Dec 13, 2022 at 21:09 | history | answered | wlad | CC BY-SA 4.0 |