# Constructive proofs of existence in analysis using locales

There are several basic theorems in analysis asserting the existence of a point in some space such as the following results:

1. The intermediate value theorem: for every continuous function $f : [0,1] \to \mathbb{R}$ such that $f(0) \leq 0$ and $f(1) \geq 0$, there exists a point in the space $f^{-1}(0)$.
2. Brouwer's fixed-point theorem: for every function $f$ on (say) the closed disk $D$, there exists a point in the space $\{ x \in D\ |\ f(x) = x \}$.
3. The fundamental theorem of algebra: for every nonconstant polynomial $p$ with complex coefficients, there exists a point in the space $p^{-1}(0)$.

These results are not provable constructively as stated. Sometimes such theorems can be reformulated so that they become provable. These modifications are all ad hoc, but there is one general idea that we can apply in all of these cases. First, we need to replace spaces with corresponding locales. Moreover, since the existence of points of locales is often not provable constructively, we should replace the condition "has a point" with "is nontrivial".

Are these theorems provable constructively when formulated in this way?

Note that if this is true, then this implies classical results since assuming LEM these locales are spatial.

• There is a standard definition of this locale: ncatlab.org/nlab/show/locale+of+real+numbers. Classically, it coincides with the usual spatial locale, but it may not be spatial constructively. Dec 19, 2017 at 6:23
• @François: Just as classically you can define the space $\mathbb{R}$ by first taking the set of Dedekind cuts and then equipping this set with a suitable topology, you can (in just one step!) define the locale $\mathbb{R}$ as the locale of Dedekind cuts (more formally, the classifying locale of the theory of a Dedekind cut). The points of this locale will then precisely be the usual real numbers (defined using Dedekind cuts). But the locale behaves better than the topological space in intuitionistic mathematics. For instance, the locale $[0,1]$ is compact, while the space might not be. Dec 19, 2017 at 10:28
• @ValeryIsaev I don't understand your remark. Both Brouwer's and Bishop's constructive definitions of $\mathbb{R}$ yield a complete metric space. Bishop uses Cauchy sequences, Brouwer has interesting alternatives (which if pushed further yield very efficient representations for exact computation). Brouwer's approach also incorporates Cauchy sequences and decimal expansions, it is interesting to compare all these versions. The Cauchy sequences form a complete metric space also constructively, the decimal expansions do not. FTA holds for any common definition making $\mathbb{C}$ complete. Dec 20, 2017 at 18:01
• @FrankWaaldijk There are many variations of constructive mathematics. I guess you allow countable choice, which is computationally OK. Assuming countable choice many different definitions of reals become equivalent. In particular, Cauchy reals are complete. But I prefer a more general framework of constructive mathematics where we do not assume any kind of choice. Then there are several nonequivalent definitions of real numbers and FTA does not hold for all of them. Dec 20, 2017 at 19:45
• @FrankWaaldijk Well, this is kind of the point of this question. Dec 20, 2017 at 21:25

I claim that the following result have constructive* proof:

1) Let $f : [0,1] \rightarrow \mathbb{R}$ be a uniformly continuous function such that $f(0)\leqslant 0$ and $f(1) \geqslant 0$ then (as a locale) $\{x, |f(x)=0 \}$ is not empty.

2) Let $f :D \rightarrow D$ be a uniformly continuous function then the locale $\{x | f(x)=x\}$ is not empty.

3) let $p$ be a complex polynomial, with at least one coeficient $|a_i|>0$ other than the constant coeficient, then the locale $\{x |p(x)=0 \}$ is not empty.

each time " $F$ not empty" really just mean that $F = \emptyset \Rightarrow False$

and the "*" on constructive refer to the fact that these are proof relying on Barr's theorem, cf below.

All of them follow the same scheme which I will explain below (and I will explain precesely what I mean by 'constructive' as there is a small subtleties here)

A first remark: I added "uniformly continuous" because, asking that a function from $[0,1]$ or $D$ to $\mathbb{R}$ extend to a function between the corresponding locales is the same as saying that the function is uniformly continuous. So if every time you interpret those as functions on the corresponding locale, then you can remove the uniform continuity hypothesis, and I only put it to remind of this.

Now let's move to the proof of those claim. They point is to prove them internally in a Grothendieck $T$ using Barr's covering theorem which assert that every topos $T$ admit a surjection from a topos $E \twoheadrightarrow T$ such that the internal logic of $E$ satisfies LEM and AC. (surjection mean that $f^*$ is conservative)

More precisely:

• Every Grothendieck topos admit a surjection $E \twoheadrightarrow T$ where $E$ is a boolean locale. (hence its logic satisfies LEM)

• Assuming AC (in the topos of set) the internal logic of every boolean locale satisifes AC.

The proof strategy for each points is the following:

You start with the problem in a topos $T$, you pull it back to a problem in $E$ where you now how to prove it because you have LEM and AC in $E$. And then you are able to deduce the result in $T$ using that $E \twoheadrightarrow T$ is a surjection. I will explain in more detail at the very end of my answer how this is done.

This gives a non constructive proof that these theorems hold in every Grothendieck topos. If you have a proof of the claims $1,2$ or $3$ that uses LEM but not AC, then you actually obtain a constructive but non predicative proof that it holds in every Grothendieck topos, and in particular in the topos of sets.

Moreover in each case you can construct a "classyfing topos for the assumption", for exemple for $(1)$ one can construct the classifying locales of all function $f:[0,1] \rightarrow \mathbb{R}$ such that $f(0) \leqslant 0$ and $f(1) \geqslant 0$ simply because $[0,1]$ is exponentiable in the category of locale and similarly. You can then apply the argument above to these classyfing topos for the assumption to deduce that the theorem holds in these specific toposes (locales). As classyfing topos have a "syntactical" description in terms of geometric logic, this actually implies that each of the claim $1$, $2$ and $3$ have a proof purely in the language of geometric logic. this puts us is the following situation:

We have given a non-constructive proof that these claim have constructive and even predicative proofs.

Whether you accept that as a constructive proof depends on your philosophical stance:

• If you are interested in constructivity only because of topos theoretic interpretation (or other models of constructive mathematics) then you should accept that as a constructive proof.

• If you are interested in constructivity for philosophical reason, this shouldn't be a satisfying proof.

• If you are interested in "constructive proof <-> algotrithm" correspondence, then this is only partially satisfying: it says that "there exists an algorithm" that will do the corresponding task, but it does not say what the algorithm is.

And in all case, it does mean that a constructive proof do exists, so we should be able to find it. (and if those results are important to you or you plan to publish somehting that rely on them I would suggest to try to find actual construct proof for them instead of this argument, it is a lot easier to find a proof once one knows that it exists !)

Finally, let me clarify the proof that the validity of such statement in $E$ implies their Validity in $T$. I will do that for point $2$ in full detail, but this is exactly the same for all of them.

First, if we have $p:E \rightarrow T$, and interally in $T$ some function $f:D \rightarrow D$ then this can be pulled back as:

$p^{\sharp} f : p^{\sharp} D \rightarrow p^{\sharp} D$ in $E$, where $p^{\sharp}$ is how I denote the pullback of locales along a geometric morphism. And (for the locales of real numbers) $p^{\sharp} D$ is just $D$ so we have the exact same situation in $E$.

The sublocale of $D$, $\{ x \in D |f(x)=x \}$ is defined as a certain pullback so it is preserved by pullback as well:

$p^{\sharp} (\{ x \in D | x= f(x) \}) = \{ x \in p^{\sharp} D | x = p^{\sharp}(f)(x) \}$

The key point is the following: if $K$ is a locale in some topos, one can consider the proposition $K=\emptyset"$ (which, as any proposition is a subterminal object of our topos. I claim that when $K$ is a compact locale (internally in $T$) then:

$p^*(K=\emptyset") =  p^{\sharp} K = \emptyset"$

intuitively, this is becasue (say when $T$ is a locale), a compact locale $K$ in $T$ is a proper geometric morphism $K \rightarrow T$, in particular, it is a closed map, hence its image is closed and the open complement of its image is the proposition in $T$, $K= \emptyset$ and this is stable under any pullback (but it only works because $K \rightarrow T$ is stably closed).

For a more precise proof, it is essentially the Beck-Chevalley condition for proper map of toposes (C3.2.6 in sketches of an elephant).

This implies that if $K$ is some locale in $T$ such that for $p : E \twoheadrightarrow T$ a surjection, if $p^\sharp K = \emptyset \Rightarrow False$ in $E$ than $K= \emptyset \Rightarrow False$ in $T$.

Indeed $K= \emptyset \Rightarrow False$ can be written as the fact that $\emptyset \hookrightarrow  K = \emptyset''$ is an isomorphism, and th $\emptyset \hookrightarrow  p^{\sharp}K = \emptyset''$ is exactly the pullback of this map by $p^*$, so the conservativity of $p^*$ implies the result.

• Thanks for the nice answer. I was not aware of the fact about uniform continuity. Do you have a reference for this result? Jan 14, 2018 at 22:23
• @ValeryIsaev : Yes and no: it follows from the constructive version of the following two fact: a continuous function on a compact is uniformly continuous, and a uniformly continuous function from a metric space to a complete metric space extend uniquely to the completion of its domain (and the locale of real number is the localic metric completion of the set of rational/real number). The first fact is very easy to obtain constructively. For the second, you need a little bit of theory of metric locales and metric completion whose constructive version is treated in my paper (...) Jan 15, 2018 at 10:15
• arxiv.org/pdf/1411.0898.pdf, precisely proposition 3.3.11. There were also previous treatment of localic completion (notably by S.Vickers and E.Palmgren) that might be sufficient for this but I have not work on that for a long time, so I don't really remember what they cover. See the references in the nLab page ncatlab.org/nlab/show/localic+completion for more details. Jan 15, 2018 at 10:19

[I don't have enough points to comment; this is just a partial answer, at best]

Steve Vickers' paper https://www.cs.bham.ac.uk/~sjv/CViet.pdf has a constructive version of 1 (IVT). Theorem 41 in Section 7.3 (page 37). Broadly, the view taken there is that 'there exists $x$ such that $f(x)=0$' is interpreted as 'the inf of the modulus of $f$ is zero'. The paper also talks about a number of other issues that are being discussed in this thread.

• "I don't have enough points to comment": that was a pun, right? :) Jan 11, 2018 at 13:59
• Ha - no, not by intention no. However I am pleased to say that I do now have enough points to comment so I won't have to repeat this slight abuse of the system. Jan 12, 2018 at 8:23