Question: Wikipedia says that the [intermediate value theorem](https://en.wikipedia.org/wiki/Intermediate_value_theorem) “depends on (and is actually equivalent to) the completeness of the real numbers.” It then offers a simple counterexample to the analogous proposition on ℚ and a proof of the theorem in terms of the completeness property.

Does an analogous result hold for the computable reals (perhaps assuming that the function in question is computable)? If not, is there a nice counterexample?

Answer: 
Let me assume that you are speaking about computable reals and functions in the sense of
[computable analysis](https://en.wikipedia.org/wiki/Computable_analysis), which is one of the most successful approaches to the topic. (One must be careful, since there are several incompatible notions of computability on the reals.)

In computable analysis, the [computable real numbers](https://en.wikipedia.org/wiki/Computable_real_number) are those that can be computed to within any desired precision by a finite, terminating algorithm (e.g. using Turing machines). One should imagine receiving rational approximations to the given real. In this subject, functions on the reals are said to be computable, if there is an algorithm that can compute, for any desired degree of accuracy, the value of the function, for any algorithm that produces approximations to the input with sufficient accuracy. That is, if we want to know f(x) to within epsilon, then the algorithm is allowed to ask for x to within any delta it cares to.

The **Computable Intermediate Value Theorem** would be the assertion that if f is a computable continuous function and f(a)< c<f(b) for computable reals a, b, c, then there is a computable real d with f(d)=c.

The book [Computable analysis: an introduction](https://books.google.com/books?id=OPolVWVFDJYC&dq=computable+analysis&printsec=frontcover&source=bl&ots=_QlUjkXhSy&sig=5m7E0aXQ-CVl8HcF77tzW2AW5Pk&hl=en&ei=Eh8pS93oN4Oj8AbDoIW1DQ&sa=X&oi=book_result&ct=result&resnum=10&ved=0CEIQ6AEwCQ#v=onepage&q=&f=false) by Klaus Weihrauch discusses exactly this question in Example 6.3.6.

The basic situation is as follows. The answer is **Yes**. If f happens to be increasing, then the usual bisection proof of existence turns out to be effective. For other f, however, one can use a trisection proof. Theorem 6.3.8 says that if f is computable and f(x)\*f(z)<0, then f has a computable zero. This implies the Computable Intermediate Value theorem above.

In contrast, the same theorem also says that there is a non-negative computable continuous function f on [0,1], such that the sets of zeros of f has Lebesgue measure greater than 1/2, but f has no computable zero.

In summary, if the function crosses the line, you can compute a crossing point, but if it stays on one side, then you might not be able to compute a kissing point, even if it is kissing on a large measure set.
This question and its answers confused me for a while, but I think I get it now, so I'll describe my experience in the hopes that it will help other non-experts, and the experts can tell me if I've still got anything wrong.

My initial reaction was: given a computable function f : [a, b] → ℝ with f(a) < 0 and f(b) > 0, "of course" we can compute an element z of [a, b] with f(z) = 0, as follows: choose c to be the midpoint (a+b)/2, check whether f(c) is positive or negative, report that z is in [a, c] or [c, b] respectively, and recurse on that interval. Ironically, the problem is that f(c) might actually be exactly 0. If so, we can ask for its value to arbitrarily large precision, but will never learn anything about whether it is positive, negative, or zero, so we cannot output c as the answer, nor guarantee that either subinterval [a, c] or [c, b] contains a root of f.

Under the locally non-constant hypothesis, however, we can choose c' near c (so that both intervals [a, c'] and [c', b] are less than k times as wide as [a, b] for some fixed k < 1) so that f(c) and f(c') are distinct. Then we can compute f(c) and f(c') in parallel, stopping when we know that one of them is either positive or negative, as must eventually happen since they cannot both be zero, and proceed as before.

It's also clear now why classically there is a computable root of f without any hypotheses besides computability of f: either some number of the form a + (s/2r)(b-a) is a root of f—these numbers are all computable—or the original algorithm will succeed forever and thus compute a root of f.