Thanks first to Andrej for drawing attention to
my paper on the IVT,
and indeed for his contributions to the work itself.
This paper is the introduction to Abstract Stone Duality
(my theory of computable general topology) for the general mathematician,
but Sections 1 and 2 discuss the IVT in traditional language first.
The following are hints at the ideas that you will find there and
at the end of Section 14.
I think it's worth starting with a warning about the computable
situation in ${\bf R}^2$, where it is customary to talk about fixed
points instead of zeroes.
Gunter Baigger
described
a computable endofunction of the square.
The classical Brouwer thereom says that it has a fixed point,
but no such fixed point can be defined by a program.
This is in contrast to the classical response to the constructive
IVT, that either there is a computable zero, or the function
hovers at zero over an interval.
(I have not yet managed to incorporate Baigger's counterexample
into my thinking.)
Returning to ${\bf R}^1$, we have a lamentable failure of classical
and contructive mathematicians to engage in a meaningful debate.
The former claim that the result in full generality is "obvious",
and argue by
quoting random fragments of what their opponents have said in
order to make them look stupid.
On the other hand, to say that
"constructively, the intermediate value theorem fails"
by showing that it implies excluded middle
is equally unconstructive.
Even amongst mainstream mathematicians several arguments are conflated,
so I would like to sort them out on the basis of
the generality of the functions to which they apply.
On the cone hand we have the classical IVT, and the approximate
construtive one that Neel mentions. These apply to any
continuous function with $f(0) < 0 < f(1)$.
There are several other results that impose other pre-conditions:
the exact constructive IVT, for non-hovering functions,
described by Reid;
using Newton's algorithm,
for continuously differentiable functions
such that $f(x)$ and $f'(x)$ are never simultaneously zero; and
the Brouwer degree,
with an analogous condition in higher dimensions.
These conditions are all weaker forms of saying that the function is
an open map.
Any continuous function $f:X\to Y$ between compact Hausdorff spaces
is proper: the inverse image $Z=f^{-1}(0)\subset X$
of $0\in Y$ is compact (albeit possibly empty).
If $f:X\to Y$ is also an open map then $Z$ is overt too.
I'll come back to that word in a moment.
When $f$ is an open map between compact Hausdorff spaces and $Z$
is nonempty, there is a compact subspace $K\subset X$ and an open
one $V\subset Y$ with $0\in V$ and $V\subset f(K)$.
So for real manifolds we might think of $K$ is a (filled-in) ball
and $f(K)\setminus V$ as the non-zero values that $f$
takes on the enclosing sphere.
Could I have forgotten that the original question was about
computability?
No, that's exactly what I'm getting at.
In ${\bf R}^1$ an enclosing sphere is a straddling interval,
$[d,u]$ such that $f(d) < 0 < f(u)$ or $f(d) > 0 > f(u)$.
The interval-halving (or, I suspect, any computational) algorithm
generates a convergent sequence of straddling intervals.
More abstractly, write $\lozenge U$ if the open subset $U$ contains
a straddling interval.
The interval-halving algorithm (known historically as the
Bolzano--Weierstrass theorem or
lion hunting)
depends exactly on the property that $\lozenge$ takes unions to
disjunctions, and in particular
$$ \lozenge(U\cup V) \Longrightarrow \lozenge U \lor \lozenge V. $$
(Compare this with the Brouwer degree, which takes disjoint unions
to sums of integers.)
I claim, therefore, that the formulation of the constructive IVT
should be the identification of suitable conditions (more than
continuity but less than openness) on $f$ in order to prove the
above property of $\lozenge$.
Alternatively, instead of restricting the function $f$,
we could restrict the open subsets $U$ and $V$.
This is what the argument at the end of
Section 14
of my paper does.
This gives a factorisation $f=g\cdot p$ of any continuous
function $f:{\bf R}\to{\bf R}$ into a proper surjection $p$
with compact connected fibres and a non-hovering map $g$.
To a classical mathematician, $p$ is obviously surjective
in the pointwise sense, whereas this is precisely the situation
that a constructivist finds unacceptable.
Meanwhile, they agree on finding zeroes of $g$.
In fact, this process finds interval-valued zeroes of
any continuous function that takes opposite signs, which was
the common sense answer to the question in the first place.
The operator $\lozenge$ defines an overt subspace,
but I'll leave you to read the paper to find out what that means.
