[Math] Can nonstandard analysis be used to prove results in constructive or computable analysis

computable-analysislo.logicnonstandard-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?

Best Answer

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'.

Related Question