Is the Intermediate Value Theorem strictly stronger than LLPO?

Question

(The context is Intuitionistic ZF set theory, or HoTT, or the internal logic of a topos with a Natural Number Object. The real numbers here mean the Dedekind reals.)

By LLPO, I mean the statement that $\forall x \in \mathbb R: x \leq 0 \vee x \geq 0$. This should be understood not as a statement about the ordering of $\mathbb R$, but rather as a significant fragment of the Law of Excluded Middle.

By IVT (the Intermediate Value Theorem), I mean the statement that for all continuous functions $f:[0,1]\to\mathbb R$ where $f(0)\leq0\leq f(1)$, there is a $t \in [0,1]$ for which $f(t)=0$. Note that there are reasonable substitutes for the classical Intermediate Value Theorem (such as the one discussed by Paul Taylor in A lambda calculus for real analysis), but we are not considering those here.

IVT is at least as strong as LLPO. Why? Briefly, here's why. The proof that $\mathbf{IVT}\implies \mathbf{LLPO}$ follows from using IVT on $f:[0,1]\to\mathbb R, t \mapsto t\max(x,0) + (1-t)\min(x,0)$, given $x \in \mathbb R$. You may fill in the rest.

Assuming Countable Choice, IVT and LLPO become equivalent. Why? $\mathbf{LLPO} \implies \mathbf{IVT}$ follows by using Countable Choice to obtain an indicator function $P:\mathbb Q \cap [0,1] \to \{0,1\}$ which indicates for any $x \in \mathbb Q$ whether $f(x) \leq 0$ or $f(x) \geq 0$; using this, the proof then performs the usual interval bisection on $f$ using $P$ to decide which interval to recurse into.

Anyway, the proof of logical equivalence uses Countable Choice. Is it known whether or not LLPO implies IVT unconditionally?

Answer 1

In Lifschitz realizability $\mathbf{LLPO}$ holds but the intermediate value theorem fails.

The fact that $\mathbf{LLPO}$ holds is a standard property of Lifschitz realizability. The analytic version of $\mathbf{LLPO}$ follows from this together with the fact that Dedekind reals are equal to Cauchy reals in Lifschitz realizability (so we can argue using Cauchy sequences).

To show $\mathbf{IVT}$ fails we can argue by continuity using a fixed point argument. We only need to consider linear functions, i.e. $f(x) = mx + c$. If $\mathbf{IVT}$ held in the Lifschitz realizability model it would yield a computable function that takes numbers encoding $m$ and $c$ as input and yields an encoding of a finite set of roots of $f$. This encoding consists of a finite list of "potential roots" together with a computable enumeration of potential roots that are not actual roots. Call this function $F$.

Note that given any finite set of Cauchy sequences we can find a rational apart from each element of the finite set. Moreover, this can be done computably, in the following strong sense. There is a computable partial function taking a list of numbers as input $G([e_1,\ldots,e_n])$ such that if all $e_i$ encode a Cauchy sequence (with given modulus of convergence, say $1/k$), then $G([e_1,\ldots,e_n])$ halts, and whenever $G([e_1,\ldots,e_n])$ halts and $e_i$ encodes a Cauchy sequence, $G([e_1,\ldots,e_n])$ is a rational apart from $e_i$ (even if $e_j$ is not a valid Cauchy sequence for some $j \neq i$).

We now simultaneously define $m$ and $c$ above as computable Cauchy sequences described explicitly by an algorithm. By the fixed point theorem, we may assume the algorithm has access to a number $e$ encoding $m$ and $c$. We define the $k$th entry of the Cauchy sequences as follows. We first apply the function $F$ above to numbers encoding $m$ and $c$ and check if it halts within $k$ steps. If it does, we take set of potential roots, and remove any false roots that are enumerated within $k$ steps. We then apply $G$ to this finite list and check if it halts within $k$ steps. If it does we choose $m$ and $c$ so that $|m|, |c| < 1/k$ and the only root of $m x + c$ is the one given by $G$. If any step fails, we return $0$.

Note that the above algorithm always returns valid Cauchy sequences with modulus of convergence $1/k$, falling back to $0$ if we didn't know that either $F$ or $G$ does not halt at all. Hence (using Markov's principle) in fact both $F$ and $G$ do eventually halt at sufficiently large $k$. However, this gives a contradiction, since the only root of $m x + c$ lies outside the finite list of roots given by $F$.

Answer 2

There is, in my view, a regrettable custom, amongst even the most eminent people, that I call unconstructive mathematics, namely taking some classical result verbatim and showing that this implies excluded middle or some other classical principle. One should instead find a new result that is constructive in both the mathematical and plain English sense, that reduces to the classical "in the limit". The same complaint would apply to the alleged necessity of the Axiom of Choice, for example in Tychonov's theorem about compactness of product topologies, and to more extreme classical principles.

For analogy, suppose that Einstein's reaction to the Michelson-Morley experiment had been to say that "the physics of Newton and Maxwell are inconsistent", then we would not have learned Special Relativity.

The Intermediate Value Theorem is a topological question and deserves a answer in constructive topology.

The key constructive counterexample (or better, teaching example) is of a function that "hovers" or is "locally constant" with value(s) indistinguishable from zero.

The approximate constructive intermediate value theorem says that points can be found where the function value is within $\epsilon$ of zero. In my opinion this is still "running away" from the problem, albeit only by $\epsilon$.

The IVT is valid constructively and computationally when there is some point enclosed in arbitrarily small mini-IVTs or straddling intervals, ie where the function value is definitely positive on one side and definitely negative on the other.

If we write $\lozenge U$ for the property of an open subset that it contains a straddling interval, $\lozenge$ preserves unions (or rather, takes them to existential quantifiers) so long as the function does not hover.

This leads to the notion of an overtness, which is lattice-dual to compactness and is explained using IVT as its leading example in my paper A lambda calculus for real analysis.

There is even a version of this with the same hypotheses as the classical result, but where the result is a closed interval instead of a point, or alternatively the line is quotiented to turn these intervals into points. Beware, however, that the endpoints of the interval are one-sided, not the familiar Euclidean-Eudoxan-Dedekind, reals. This is discussed at the end of the paper, although it is of limited value since it can't be generalised to ${\mathbb R}^n$.

So for the classical/constructive interface, there are two possible questions: what logical principle is needed

• to ensure decidable equality of real numbers (for which of course you have a choice of definitions); and

• to select a point in a compact connected subspace that is non-empty in the sense that I called occupied in my paper (and with one-sided real endpoints, else one of them serves as the chosen point).

A space (or locale, to make this more precise) $X$ is compact occupied if the map $f:X\to 1$ has $f_*;f^*=id_1$ where $f^*\dashv f_*$. I wonder what logical principle would force such a space to have a point.

Even the dual situation is not clear: $X$ is overt inhabited if $f_!;f^*=id_1$ where $f_!\vdashv f^*$. I think I can prove that this has a point if $X$ is locally compact and countably based, but I have no idea otherwise.