Approximate intermediate value theorem in pure constructive mathematics

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

• In most varieties of constructive math, the functions which are defined on [a,b] and provably pointwise continuous on [a,b] are also provably uniformly continuous on [a,b]; the inferential rule is valid even though the implication is not provable. Or so I suspect, though I've only seen proofs of related things and not of this specifically. In any case, because of this I wouldn't expect to see a weak counterexample. – Matt F. Oct 25 '16 at 19:56
• @MattF. I thought I'd seen a weak counterexample to the statement "every pointwise continuous function on [a,b] is uniformly continuous", though I don't remember it offhand. But in any case, as I said, a strong countermodel would be even better. – Mike Shulman Oct 25 '16 at 21:20
• For anyone looking for a counterexample let me remark that the most naive example does not work: Let $f : \mathbb{R} \to \mathbb{R}$ be a fixed continuous function. Let $X$ be a metric space. The object of Dedekind real numbers in the sheaf topos $\mathrm{Sh}(X)$ is the sheaf $\mathcal{C}_X$ of continuous functions on $X$. The function $f$ induces a morphism $\mathcal{C}_X \to \mathcal{C}_X$ by postcomposition, that is internally a function $\mathbb{R} \to \mathbb{R}$. From the internal point of view, this function is continuous and verifies the strong IVT. – Ingo Blechschmidt Oct 26 '16 at 14:22
• Claim: Let $x,y$ range over $[a,b]$ and $m,n$ over $\mathbf{N}$. If $\phi(m,n,x) \rightarrow \phi(m+1,n,x)$, then we can transform a constructive proof of $\forall n\ \forall x\ \exists m\ \phi(m,n,x)$ into a constructive proof of $\forall n\ \exists m\ \forall x\ \phi(m,n,x)$. Special case with $$\phi(m,n,x) = \forall y\ ( |x-y|<1/m \rightarrow |f(x)-f(y)|<1/n)$$: if pointwise continuity is constructively provable then so is uniform continuity. Question for the crowd: is there a known result from which the claim follows? – Matt F. Oct 26 '16 at 14:56
• To construct a function that's not uniformly continuous, one typically uses Kleene's first realizability model and considers Kleene's singular tree. By embedding Cantor space into [0,1] one obtains an unbounded function, which therefore cannot be uniformly continuous. This should be in Beeson's book. It can also be found in Troelstra/van Dalen or Bridges/Richman - Varieties of constructive mathematics. I seem to recall that one can combine realizability with forcing to obtain a model without countable choice and fan. However, I do not recall the source. Still, this does not yet contradict IVT. – Bas Spitters Oct 27 '16 at 17:57

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.

• And I do believe that this works! I'll sleep on it before being too sure, but it seems right to me: the idea is that at the point when we make a "choice" in the proof, we can instead interpolate between the two options. – Mike Shulman Nov 23 '16 at 3:31
• Beautiful! I think this is a genuinely new idea about the bisection method. – Andrej Bauer Nov 23 '16 at 12:11
• I agree, this is very nice! Totally worth 200 rep. – Mike Shulman Nov 23 '16 at 16:29
• @MattF., could you please contact me in real life. I think this should be published or at least presented somewhere outside of MO. – Andrej Bauer Nov 24 '16 at 10:37
• Following up on @AndrejBauer 's comment, Matt F's paper, Interpolating Between Choices for the Approximate Intermediate Value Theorem is now here: arxiv.org/abs/1701.02227 May I say, it's very nice. – David Roberts Jan 16 '17 at 5:46

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.

• This proof uses the typical Bishop trick of treating sets as setoids (set + equivalence relation). It is not valid in a topos. It is not valid in a model if intuitionistic set theory. It is not valid in homotopy type theory. You have simply circumvented the use of countable choice (you don't need dependent choice for your construction, even when you do honest equality) by replacing equality relation with an equivalence relation. – Andrej Bauer Nov 18 '16 at 9:00
• @AndrejBauer, I agree with your first and last sentences. I might express the homotopy type theory comment as "this proof will not work if we treat the reals as in homotopy type theory". I'll leave it to the OP to say whether this answers his question. – Matt F. Nov 18 '16 at 10:44
• Andrej is right, this is not a proof about the real numbers but about Cauchy sequences -- a real number is an equivalence class of Cauchy sequences. – Mike Shulman Nov 18 '16 at 17:31
• Downvoters, does this really qualify as an egregiously sloppy, no-effort-expended, or clearly and perhaps dangerously incorrect answer to the original version of the question? If the setoid approach is legitimate in constructive math, as I think it is, then "not what the OP had in mind" seems fairer than "incorrect". Or is it just that, given the edit to the question, it would be better to remove the answer? – Matt F. Nov 18 '16 at 23:27
• Please leave the answer, because someone else searching for an answer to the original question, but who does want the Bishop setting, will find it useful. Also, other answers might be able to reference yours. (For reference sake, I upvoted your answer since I thought it carefully thought out and useful) – David Roberts Nov 19 '16 at 0:58

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

• This may be interesting, but it does not answer the question, which was specifically about "an arbitrary pointwise continuous function". – Mike Shulman Nov 25 '16 at 19:27
• Like I said, in CLASS, INT and RUSS we can prove that "an arbitrary pointwise continuous function" coincides with "a #-morphism". That is why I consider my answer to be an answer. For a much more detailed answer see my reply to your same question on constructive-news. – Frank'a Waaldijk Nov 26 '16 at 10:38
• I still don't have enough reputation to comment on any other answer except my own... So I'll be a little creative.By the way, I said that in Matt's first proof there is a hidden use of countable choice, but it really is a hidden use of dependent choice. This is the "only" failure that I see in that answer (well, it ceases to be an answer then I suppose), and I am surprised that no one noticed the use of DC in that proof. – Frank'a Waaldijk Nov 26 '16 at 11:21
• Oops, I hit enter when I was still editing my comment. Because I wanted to start with saying that I really think that Matt's second proof is very beautiful! I have to get the hang of MO, sorry. – Frank'a Waaldijk Nov 26 '16 at 11:23