I'm trying to learn a bit about intuitionistic/constructive mathematics, as I want to understand a little about topos theory and homotopy type theory (HoTT). I'm confused as to why the intermediate value theorem doesn't hold in constructive analysis.
Suppose $f: \mathbb{R} \to \mathbb{R}$ is a continuous function on the interval $(a, b)$. Further, suppose $f(a) < 0$ and $f(b) > 0$. By classical analysis, there exists a point $c \in (a, b)$ such that $f(c) = 0$. I'm told that this doesn't generally hold in constructive or intuitionistic logic. I would like to know why the following "construction" does not constitute an outline of a proof.
Let $a_n$ be a sequence of points defined as follows:
$a_0 = \frac{a + b}{2}$
$a_n = \frac{a + a_{n-1}}{2}$ if $f(a_{n-1}) > 0$
$a_n = \frac{b + a_{n-1}}{2}$ if $f(a_{n-1}) < 0$
$a_n = a_{n-1}$ if $f(a_{n-1}) = 0$.
Define $c = \lim_{n \rightarrow \infty} a_n$. Then $f(c) = 0$. This provides an algorithmic construction (using the bisection algorithm) which not only shows that a 0 exists but actually gives a way to compute a zero. Why is this outline of a proof not valid in constructive logic? What am I missing?
The problem is that, in general, there is no way to tell whether $f(a_i) = 0$.
When working in constructive mathematics, we have to think about how each mathematical object is given - what information do we have about the object and what can we do with the object? For a continuous function $f$, if we have a real number $x$ we can compute a sequence of rational numbers $(b_i)$ that converge to $f(x)$ and so that we know a modulus of convergence for $(b_i)$.
However, suppose that we see $b_1 = 1/4$, $b_2 = 1/8$, $b_3 = 1/16$, etc. We can keep computing approximations, and they may all seem compatible with $f(x) = 0$, but at any time we could see that the next approximation makes $f(x) > 0$ or makes $f(x) < 0$. For example, if we know from the modulus of convergence that each term $b_i$ is within $1/2^{i}$ of the limit, then having $b_3 = 1/16$ is compatible with $\lim b_i = 0$, but having $b_5 = 1/16$ is not.
In the end, we cannot prove constructively that $(\forall x)(f(x) > 0 \lor f(x) = 0 \lor f(x) < 0)$. So we cannot prove that the three cases in the proof are exhaustive, and so the proof is not constructively correct.
This phenomenon is closely related to issues in computability theory. In particular, if we had a single algorithm to tell whether arbitrary real numbers were zero or not (given by convergent Cauchy sequences), we could use that to solve the halting problem.