Timeline for Strength of Bishop style constructive mathematics vs $\mathsf{RCA}_0$
Current License: CC BY-SA 3.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 11, 2013 at 21:26 | comment | added | Andrej Bauer | BISH does not prove that for all $h$ the map $f$ has a root. | |
| Jul 11, 2013 at 20:11 | comment | added | user5810 | Okay, I just deleted that sentence. $\:$ | |
| Jul 11, 2013 at 20:11 | history | edited | user5810 | CC BY-SA 3.0 |
deleted last sentence
|
| Jul 11, 2013 at 20:04 | comment | added | Jason Rute | I think Carl's and Henry's answers seem to suggest that "everything that can be proved 'constructively', can be proved in $RCA_0$" is not true. (Although you left yourself wiggle room by your use of quotes.) | |
| Jul 11, 2013 at 18:49 | comment | added | user5810 | ... where "this" is the intermediate value theorem, or the last sentence of my answer? $\hspace{.73 in}$ | |
| Jul 11, 2013 at 11:20 | comment | added | Andrej Bauer | BISH does not prove this. | |
| Jul 11, 2013 at 9:45 | history | answered | user5810 | CC BY-SA 3.0 |