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).
Best Answer
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.