# Can nonstandard analysis be used to prove results in constructive or computable analysis?

Nonstandard analysis is a useful tool which can be used to prove a number of results in analysis.

## Question

Can it also be used to prove results in computable or constructive analysis?

If so, what are some examples? (They don't need to be ground-breaking.)

## Motivation

There seems to be this analogy involving small worlds and big worlds (model is probably a more accurate term).

computable math

• small: computable real numbers
• big: real numbers

nonstandard analysis:

• small: standard real numbers
• big: nonstandard real numbers

This analogy is quite common in logic (ground model vs forcing extension for another example).

Can statements about the computably of finite objects be moved to the "computability" of nonstandard finite objects, and then transferred to the computability of standard infinite objects?

I am aware of Sam Sanders' program to connect Bishop-style constructive analysis with nonstandard analysis, but I am not aware (possibly mistakenly) that it has been used to prove statements in computable/constructive mathematics.

## Possible examples

1. Can one use nonstandard analysis to show that the supremum of a computable function $f$ on $[0,1]$ is computable uniformly from $f$? (The corresponding finitary statement about finite functions of rationals is clearly true.)

2. What about the computability of the Riemann integral?

-
It think Sam Sanders is the expert on this question, I'll alert him to its existence. –  Andrej Bauer Apr 26 '13 at 8:29
Sam Sanders had given a talk at the Newton Institute on related matters, perhaps it is useful: newton.ac.uk/programmes/SAS/seminars/2012012616301.html –  Tanmay Inamdar Apr 26 '13 at 10:32
Sam says he is going to give an answer in "due time", whatever that means. –  Andrej Bauer Apr 26 '13 at 11:12
Tanmay, I was there. But thank you for the reference. I forgot it was recorded. –  Jason Rute Apr 26 '13 at 14:58
I do not know whether this is what you are looking for but Keita Yokoama used non-standard analysis to analyze the strength of the Riemann mapping theorem in terms of reverse mathematics, see math.tohoku.ac.jp/~y-keita/papers/nonst-r-mapping.pdf –  alexod Apr 26 '13 at 20:11

Nonstandard Analysis (NSA) can be used to prove results in computable/constructive analysis; The central notion is $\Omega$-invariance, defined as follows.

[As usual, the set $N$ consists of the standard/finite/natural numbers; The set ${^{\star}}N$ is an end-extension of $N$ and $\Omega={^{\star}}N\setminus N$ consists of the infinite/nonstandard numbers. For a standard formula or function $A(n)$ defined on $N$, the object $^\star A(n)$ is defined on $^\star N$. Let $R$ be the set of real numbers.]

($\Omega$-invariance)

1) For a standard bounded formula $\varphi(n,m)$, and an infinite number $\omega\in \Omega$, the formula $^\star\varphi(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star\varphi(n,\omega)\leftrightarrow {^\star}\varphi(n,\omega')].$$

2) For a standard function $f:N\times N\rightarrow N$, and an infinite number $\omega\in \Omega$, the function $^\star f(n,\omega)$ is $\Omega$-invariant if $$(\forall n\in N)(\forall \omega'\in\Omega)[^\star f(n,\omega)= {^\star}f(n,\omega')].$$

3) For a standard function $F:R\times N\rightarrow R$, and an infinite number $\omega\in \Omega$, the function $^\star F(x,\omega)$ is $\Omega$-invariant if $$(\forall x\in R)(\forall \omega'\in\Omega)[^\star F(x,\omega)\approx {^\star}F(x,\omega')].$$

Note that $\Omega$-invariance is essentially "independence of the choice of infinitesimal".

Now, $\Omega$-CA is the comprehension axiom for $\Omega$-invariant formulas as follows: For all $\Omega$-invariant $^\star\varphi(n,\omega)$, we have $(\exists X^s \subset N)(^\star\varphi(n,\omega) \leftrightarrow n\in X^s)$. Here, the superscript $^s$' refers to the fact that $X^s$ is a standard set.

Recently, Antonio Montalbán and me showed the following:

1) $^\star$RCA$_0+\Omega$-CA is a conservative extension (in the standard language) of RCA$_0$. Here, $^\star$RCA$_0$ is a nonstandard version of $\text{RCA}_0$.

2) In $^\star I\Sigma_1$, $\Omega$-CA implies $\Delta_1^0$-comprehension.

3) $^\star$RCA$_0+\Omega$-CA proves that for every $\Omega$-invariant $^\star F(x,\omega)$, there is a standard $G:R\rightarrow R$ such that $(\forall x\in R)(^\star F(x,\omega)\approx {^\star}G(x)$.

If I am not mistaken, the previous three observations answer your question regarding computable analysis: As long as one produces $\Omega$-invariant functions, the results are computable. (There is/should be some analogue to the Gaifman-Dimitracopoulos theorem here.)

One can refine the above to 'constructive analysis', but explaining that would take up too much space.

One a philosophical note, one might argue that most/all of the infinitesimal calculus used throughout physics is $\Omega$-invariant, and therefore computable.

Three final remarks:

0) There are a number of analogies one can use to compare NSA and constructive/computable analysis. To me, these analogies are quite helpful/insightful. Jason is right in pointing out his analogy. Not everyone seems to agree on this, however.

1) The above view of NSA is called 'Robinsonian'. The same definitions etc. can be made in Nelson's internal' framework without any problem.

2) Somehow, mathoverflow does not parse '*' very well: one has to use '\star'.

-
Thanks for a very interesting answer. Is there a home for this "Antonio Montalbán and me showed"? –  katz Apr 28 '13 at 11:45
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. –  Jason Rute Apr 28 '13 at 21:00
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? –  Jason Rute Apr 28 '13 at 22:15
...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$.) –  Jason Rute Apr 28 '13 at 22:42
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'? –  Sam Sanders Apr 29 '13 at 7:38