Timeline for Can nonstandard analysis be used to prove results in constructive or computable analysis?
Current License: CC BY-SA 3.0
13 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Apr 29, 2013 at 9:58 | vote | accept | Jason Rute | ||
| Apr 29, 2013 at 9:57 | comment | added | Jason Rute | I am not sure this answers all my questions, but it seems to get me much closer, so I am accepting it. Thanks again for taking the time to answer my question! | |
| Apr 29, 2013 at 9:44 | comment | added | Sam Sanders | Jason. I understand your question better now, I think. The result in RCA$_0$ should in principle read "For F coded in $L_2$ by...". As you correctly point out, this reduces the generality. The results concerning F are proved in RCA$_0$, but could be generalized to any other suitable (higher-order) system. | |
| Apr 29, 2013 at 8:57 | comment | added | Jason Rute | Sam, as for $F$ being continuous, the language of $\mathsf{RCA}_0$ is second order arithmetic and can only talk about first and second order objects. It can't talk about arbitrary functions from the reals to the reals. Are you are working in higher order reverse math instead? That might be my confusion. | |
| Apr 29, 2013 at 7:40 | comment | added | Sam Sanders | @ Katz; We are currently in the process of writing up our results. The latter also connect to areas like Constructive Analysis, so things are not "finished" yet. | |
| Apr 29, 2013 at 7:38 | comment | added | Sam Sanders | Jason, I tried to use the 'standard' notation of NSA as much as possible, not the notation of Yokoyama-san's paper. The notation in the latter is perfectly non-ambiguous, but rather heavy. Thus, $^\star f$ and $^\star F$ are indeed the image of the (standard) $f$ and $F$ under the embedding operation (like the usual Robinson star morphism). What do you mean by '$F$ must be continuous'? | |
| Apr 29, 2013 at 7:32 | history | edited | Sam Sanders | CC BY-SA 3.0 |
deleted 1 characters in body
|
| Apr 28, 2013 at 22:42 | comment | added | Jason Rute |
...or maybe you just mean $^*f$ and $^*F$ are nonstandard variables. (I am confused because you say "For a standard $f$ ...$^*f$..." implying that $^*f$ comes from $f$.)
|
|
| Apr 28, 2013 at 22:15 | comment | added | Jason Rute |
Sam, to clarify, the language of $^*\mathsf{RCA}_0$ has standard and nonstandard versions of each symbol, e.g. $0^s, +^s, \in^s, \ldots, 0^*, +^*, \in^*, \ldots$ as well as an embedding operator $\surd$. (This terminology is from math.tohoku.ac.jp/~y-keita/papers/ns-WWKL-100415.pdf.) When you say $^*\varphi$, you mean replacing the standard symbols with the nonstandard ones. When you say $^*f$ and $^*F$, you mean the image of $f$ and $F$ under the embedding operator. Further $F$ must be continuous. Is all this correct?
|
|
| Apr 28, 2013 at 21:00 | comment | added | Jason Rute |
Sam, welcome to Mathoverflow! Thanks for the answer. Let me carefully read through it. Two quick comments. There is a typo in my name. Also if you want the $*$ to work, the trick is to enclose your $\LaTeX$ with backquotes (see the "How to write math" box on the right). Otherwise it tries to format $*...*$ as italics.
|
|
| Apr 28, 2013 at 11:45 | comment | added | Mikhail Katz | Thanks for a very interesting answer. Is there a home for this "Antonio Montalbán and me showed"? | |
| Apr 28, 2013 at 10:57 | history | edited | Sam Sanders | CC BY-SA 3.0 |
added 3 characters in body
|
| Apr 28, 2013 at 10:51 | history | answered | Sam Sanders | CC BY-SA 3.0 |