4
$\begingroup$

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.

$\endgroup$

1 Answer 1

1
$\begingroup$

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.

$\endgroup$
4
  • $\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$
    – Jason Rute
    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$
    – Jason Rute
    Nov 25, 2015 at 17:54

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.