Simpson's Subsystems of Second Order Arithmetic (pp. 134ff.) uses RCA$_0$ to prove various theorems of analysis for all continuous functions with a suitable modulus of uniform continuity. And he notes that RCA$_0$ itself proves "any continuous function which arises in practice" does have such a modulus. Is there a place I can go to see many examples of the functions this covers? I am especially interested in various complex analytic functions arising in analytic number theory.
1 Answer
On a space like $\mathbb{R}^n$, $[0,1]^n$, or $\mathbb{C}$, every uniformly continuous function that "arises in practice" (more on this in a bit) has a computable modulus of continuity.
To find examples, just open up a book on your favorite subject (in this case complex analysis). Every particular uniformly continuous function in that book will likely have a computable modulus of uniform continuity. To find this modulus of continuity, just follow that proof that your particular function is uniformly continuous.
For example, $e^x$ is uniformly continuous on $[0,1]$. Just use that $e^x$ has a computable Taylor series and the error estimate with that Taylor series is computable and uniform over $[0,1]$. The same goes for other functions like $\sin(x)$.
It might help to also know that if $f\colon K \rightarrow X$ is a computable function on a computable complete compact metric space $K$ to a computable Polish space $X$, then $f$ also has a computable uniform modulus of continuity. (To see this, follow the proof the every continuous function $f\colon K \rightarrow X$ is uniformly continuous. I imagine the details can be found in Weihrauch's book---but I haven't checked.)
Additional Remarks: Let's call this principle the "continuity thesis":
Every uniformly continuous function that "arises in practice" has a computable modulus of continuity
The continuity thesis is not something that I know how to state formally, much less prove.$^*$ Nonetheless, it seems to be a deep principle in mathematics, similar to the Church-Turing thesis.
I basically take the continuity thesis to be a given whenever I do research in the area. Nonetheless, just like the Church-Turing thesis, it is very instructive to go through a large number of examples to convince yourself why it is true.
As for why the continuity thesis holds, it seems to be that the only way one can prove that a function on, say, $[0,1]$ is continuous is to explicitly give it's modulus of uniform continuity (or a similar quantitative witness to uniform continuity).
Last, I am sure many mathematicians wouldn't say this principle is as strong as the Church-Turing thesis, since "arises in practice" is quite vague. Nonetheless, I challenge them to find a counterexample in an analysis book.
$^*$ Concerning the provability of the continuity principle, I think you (slightly) misrepresented Simpson's quote (pp.136-137 in the second edition):
However, it is interesting to note that “any continuous function which arises in practice” can be proved in $\mathsf{RCA}_0$ to have a modulus of uniform continuity on any closed bounded subset of its domain.
-
$\begingroup$ Yes, this works as long as "computable" means primitive recursive computable. Your advice is that instead of looking for a reference that has already organized a lot of this, I should do it from scratch myself. You may be right. I do not think I misrepresented anything, though. I wrote of "suitable" moduli, and naturally you would expect these to be on closed bounded sets. $\endgroup$ Nov 25, 2015 at 17:40
-
$\begingroup$ @ColinMcLarty, I don't see why you need primitive recursive? Can you explain. $\endgroup$ Nov 25, 2015 at 17:42
-
$\begingroup$ Oh yes, I see the need for Primitive recursive is not stated. The point is that I want to use this, eventually, in Exponential Function Arithmetic, where I am pretty sure it has not been much explored in print up to now. I hope to find published proofs for PRA that would easily admit exponential bounds. I expect that proofs for RCA$_0$ will generally in fact be primitive recursive. $\endgroup$ Nov 25, 2015 at 17:46
-
1$\begingroup$ @ColinMcLarty, as for Simpson's quote, when I first read your question, I though you were implying that Simpson gave a proof of (what I am calling) the continuity thesis, which I found doubtful. It is more that your sentence can be read with two interpretations: (1) $RCA_0 \vdash$ "any continuous function which arises in practice does have such a modulus". (2) For any continuous function $f$ which arises in practice, $RCA_0 \vdash$ "$f$ has such a modulus". I thought at first it was (1), but now I think you meant (2). $\endgroup$ Nov 25, 2015 at 17:54