Timeline for How are real numbers defined in elementary recursive arithmetic?
Current License: CC BY-SA 4.0
9 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jun 22 at 17:31 | comment | added | Sam Sanders | Of course, that is easy to prove, but it is also just one direction. How do you know that ALL continuous functions have a code? Same for open sets, metric spaces, ... | |
| Jun 22 at 13:37 | comment | added | user507115 | @SamSanders In my opinion, codes that behave like continuous real functions ARE continuous real functions | |
| Jun 15 at 9:23 | comment | added | Sam Sanders | @EmilJeřábek CODES for continuous real functions can be defined there. | |
| Jun 15 at 6:05 | comment | added | Emil Jeřábek | Reals, sequences of reals, or continuous real functions can be defined in $\mathrm{RCA}^*_0$, which is a conservative extension of EA (that Friedman calls EFA). | |
| Jun 15 at 1:38 | comment | added | JoshuaZ | Maybe worth noting that many theorems we recognize as theorems about real numbers can be phrased purely in terms of rationals. For example, "$\sqrt{2}$ is irrational" can be phrased as the equivalent statement "There is no rational number $x$ such that $x^2=2$" And more subtle ones can also be phrased this way. One can even make a statement equivalent to "Pi is transcendental" in EFA, albeit in a pretty convoluted way. | |
| Jun 14 at 20:09 | vote | accept | CommunityBot | ||
| Jun 14 at 20:06 | comment | added | Noah Schweber | @richardIII Yes, rational numbers - even algebraic numbers - are no more complicated than naturals or integers in this sense. I don't know a particularly good source on this, but the basics are surely folklore (e.g. that EFA proves, appropriately formalized, the statement "the rationals from a dense linear order without endpoints" and so on). | |
| Jun 14 at 20:01 | comment | added | user507115 | This makes sense, thank you for your answer. What about rational numbers? I guess you could write them as pairs, but was it actually done? | |
| Jun 14 at 19:50 | history | answered | Noah Schweber | CC BY-SA 4.0 |