Timeline for Difference between constructive Dedekind and Cauchy reals in computation
Current License: CC BY-SA 4.0
7 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| May 11 at 7:50 | history | edited | Martin Sleziak | CC BY-SA 4.0 |
added 39 characters in body
|
| Nov 28, 2022 at 9:03 | comment | added | Martin Sleziak | I will mention at least in a comment that the linked PDF for Jeffry L. Hirst: Representations of reals in reverse mathematics can be now found here: appstate.edu/~hirstjl/bib/pdf/rrepsproof.pdf - the original link no longer works, but I did not want to bump the question just for this. | |
| Apr 19, 2016 at 18:22 | comment | added | Carl Mummert | Moreover, the program of Proof Mining makes use of exactly the same framework, which is subsystems of higher-type classical and intuitionistic arithmetic, e.g. $\text{PA}^\omega$ and $\text{HA}^\omega$. | |
| Apr 19, 2016 at 18:15 | comment | added | Carl Mummert | I am not sure if there is any evidence that can satisfy an opinion that computable analysis is not actually related to computational content, but at least I can point out that there are implementations of exact real arithmetic that are based on various representations from computable analysis. | |
| Apr 19, 2016 at 16:45 | comment | added | Paul Taylor | Is there, behind this answer, any work in which the "computational content" is actually contained in a computer? | |
| Apr 19, 2016 at 14:09 | comment | added | Carl Mummert | It is very unclear. I also find it hard sometimes because the notion of "Dedekind cut" varies so much from place to place (e.g. in computable analysis we would treat the cut as decidable, while in some other places the cut is only assumed to be enumerated). So comparing results becomes challenging. | |
| Apr 19, 2016 at 13:52 | history | answered | Carl Mummert | CC BY-SA 3.0 |