Approximate intermediate value theorem in pure constructive mathematics

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.

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.

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