Approximate intermediate value theorem in pure constructive mathematics

Question

The ordinary intermediate value theorem (IVT) is not provable in constructive mathematics. To show this, one can construct a Brouwerian "weak counterexample" and also promote it to a precise countermodel: the basic idea is that the root may not depend continuously or computably on the function, since a small perturbation in a function's value may cause a root to appear or disappear.

There are, however, many variants of the IVT that are constructively provable. This question is about the approximate IVT, which says that if $f(a)<0<f(b)$ then for any $\epsilon>0$ there is a point $x$ with $|f(x)|<\epsilon$. It seems to be well-known that the approximate IVT can be proven assuming either (1) countable (or maybe dependent) choice, or (2) that $f$ is uniformly continuous. This paper contains many versions of approximate IVT using somewhat weaker hypotheses such as "strong continuity" of $f$. But I would like to know:

Can the approximate IVT be proven constructively about an arbitrary (pointwise) continuous function $f$, without using any form of choice or excluded middle (e.g. in the mathematics valid in any elementary topos with NNO)?

If the answer is no, I would like to see at least a weak counterexample, or even better a specific countermodel (e.g. a topos in which it fails).

Edit: To clarify, the functions in question are from the real numbers (or some interval therein) to the real numbers. I'll accept an answer that defines "the real numbers" either as equivalence classes of Cauchy sequences or as Dedekind cuts (but not as a "setoid" of Cauchy sequences).

Answer 1

Here's a constructive proof of the approximate Intermediate Value Theorem from pointwise continuity, not relying on Dependent Choice and not relying on a setoid construction of the reals.

Theorem: If $f$ is pointwise continuous with $f(a)<0, \ f(b)>0,\ \epsilon>0$ then there is some $x$ with $|f(x)|<\epsilon$.

Proof: Define the following inductively:   $$a_1 = a$$ $$b_1 = b$$ $$c_n = (a_n+b_n) / 2$$ $$d_n = \max( 0, \min( \textstyle\frac{1}{2}+ \frac{ f(c_n)}{\epsilon}, 1))$$ $$a_{n+1} = c_n - d_n (b-a)/2^n $$ $$b_{n+1} = b_n - d_n (b-a)/2^n$$ Then $b_n - a_n = (b-a)/2^{n-1}.$   So the $c_n$'s converge to some $c.$

By pointwise continuity at $c$, let $\delta$ be such that $ |x-c|<\delta$ implies $|f(x)-f(c)| < \epsilon.$

Claim:  For any $m\in\mathbb{N}$, either (i) $\exists j \le m,\ |f(c_j)| < \epsilon$ or (ii) $f(a_m) < 0 $ and$ f(b_m) > 0$.

Proof of theorem from claim:

Choose $c_m$ such that $|c-c_m| < \delta / 2$ and $(a-b)/2^m < \delta / 2$, and apply the claim.

In the first case of the claim, the theorem is immediate.

In the second case of the claim,  $$ |c-a_m| \le |c-c_m| + |c_m-a_m| < \delta, \text{ so }|f(c)-f(a_m)| < \epsilon$$ $$ |c-b_m| \le |c-c_m| + |c_m-b_m| < \delta, \text{ so }|f(c)-f(b_m)| < \epsilon$$ So $f(c)$ is within $\epsilon$ of both a negative and a positive number, and $| f(c)| < \epsilon$, QED.

Proof of claim by induction on $m$. The base case is given by $ f(a) < 0, \ f(b) > 0.$

Now assume the claim for $m$. In case (i), for some $ j < m,\ |f(c_j)| < \epsilon$, and the inductive step is trivial.

In case (ii), use trichotomy with either $f(c_m) < -\epsilon/2, \ |f(c_m)| < \epsilon$, or $f(c_m) > \epsilon/2.$   If $|f(c_m)| < \epsilon$, then the inductive step is again trivial.   If $f(c_m) > \epsilon/2$, then                 $$d_m = 1$$ $$a_{m+1} = a_m, \text{ so }f(a_{m+1}) < 0$$ $$b_{m+1} = c_m,\text{ so } f(b_{m+1}) > 0$$

If $f(c_m) < - \epsilon/2$, then                 $$d_m = 0$$ $$a_{m+1} = c_m, \text{ so }f(a_{m+1}) < 0$$ $$b_{m+1} = b_m,\text{ so } f(b_{m+1}) > 0$$

QED (claim and theorem).

I think this one works; I look forward to seeing what MO says.

Answer 2

Update: this answer was before the edit to the question rejecting this setoid approach.

We can prove the approximate intermediate value theorem constructively using only pointwise continuity. The proof has the same feel as $\forall x \in \mathbf{R}\ \exists n \in \mathbf{N} \ n > r$, which is constructively valid but with $n$ chosen in a way that depends on the particular rational sequence defining $x$.

A real number $x$ is defined to be a sequence of rationals $x^n$ such that $|x^m-x^n|\le 1/m+1/n$. (Since there are no positive exponents in this proof, all positive superscripts will be these rational approximations.) So $|x-x^n| \le 1/n$ and, e.g. we can choose the $n$ above to be $\lceil x^1 \rceil + 2.$

Now we are given $a,\ b,\ \epsilon,\ f$ as in the question. Let $a_1=a$, $b_1=b$.

$$\text{Let }c_n = (a_n+b_n)/2.$$ $$\text{If }f(c_n)^n < 0,\text{ then let }a_{n+1} = c_n,\ b_{n+1}=b_n.$$ $$\text{If }f(c_n)^n \ge 0,\text{ then let }a_{n+1} = a_n,\ b_{n+1}=c_n.$$

Unlike the version referenced in the 11/16 comment, this is deterministic at each stage, so the construction of the $c$'s requires only unique choice and not dependent choice. (If there's a hidden use of dependent choice, please let me know!)

The intervals $[a_n,b_n]$ have lengths decreasing by halves with intersection $c$. Furthermore, $f(a_n)^n < 1/n$ and $f(b_n)^n \ge -1/n$ for all $n$.

By pointwise continuity of $f$, choose $\delta$ such that $|x-c|<\delta$ implies $|f(x)-f(c)|<\epsilon/3$.

Choose $m$ with $(a-b)2^{-m} < \delta$ and $1/m < \epsilon/3$. Then

$$|a_m-c|<(a-b)2^{-m} < \delta, \ \text{ and }\ f(c) \le f(a_m) + \epsilon/3 \le f(a_m)^m + 1/m + \epsilon/3 \le \epsilon.$$ By similar comparison with the $b$'s, $f(c) \ge -\epsilon$. So $c$ is as desired to prove the approximate intermediate value theorem, QED.

Answer 3

[I just started here and do not have enough reputation to comment...so I´m kind of forced to give an answer.]

I believe there is a different way to eliminate countable choice in the proof of aIVT (approximate intermediate value theorem). I've described this way on the constructive-news forum https://groups.google.com/forum/#!topic/constructivenews/e3JfKk_W2jI

I'm not sure if that description is too specialist to post here. But what it boils down to is this: in Matt's first proof, using bisection, there is a hidden use of countable choice. Because to evaluate the real number $f(c_n)$, one has to pick a representative of its equivalence class. (This is brilliantly avoided in Matt's second proof).

My first attempt to avoid this involved looking at recursive mathematics. If we take $a,b$ and $f$ to be recursive, then if we pick (recursive) representatives $a', b'$ we can apply the bisection method without using countable choice. Because taking the mean is a recursive function $m(a,b)=\frac{(a+b)}{2}$, we see that every iterative construction and evaluation of $f(c_n)$ is recursive in $a', b'$.

This approach can be characterized as: `we only need countable choice because the objects that we are working with have been insufficiently specified beforehand'. In other words: we have left too much choice in $a,b$ AND $f$

However I believe there is a more general way to avoid choice in the construction of $a,b$ AND $f$. By describing R and continuous real functions in a different way, namely R as a #-quotient and continuous real functions as #-morphisms on Baire space, we can apply the bisection method without using countable choice.

The reason for this is comparable to the recursive situation. If we pick #-representatives $a'',b''$ of $a,b$ AND #-representatives $m'', f''$ of the functions $m, f$, there is no choice left in the bisection procedure using $a'', b'', m'', f''$, because composition of #-morphisms is completely deterministic.

In CLASS, INT and RUSS I believe we can prove that every continuous real function can be represented by such a #-morphism. This proof can be found in my book Natural Topology [but it really should be checked by some more people]. A preprint which I submitted to LMCS three years ago (!) is still under reviewer's consideration.

So I believe that using #-morphisms in BISH is a general way to avoid countable choice in theorems comparable to aIVT. Since #-quotient representations can be found for any Polish space, this goes a lot further than just real functions.