Externalizing A Concrete Application of Double Negation Toposes

Question

I'm trying to come up with concrete problems which can be solved via topos theory, and I've found a good case study which has been really instructive. I've spent the past few weeks trying to understand how it interacts with double negation sheaves, but I can't quite get it straight in my head. Hopefully somebody here will be able to help ^_^.

For completeness, recall the Weierstrass Approximation Theorem, which says

$$\forall f : C \big ( [0,1], \ \mathbb{R} \big ) . \ \forall \epsilon : \mathbb{R}_{> 0} . \ \exists p : \mathbb{R}[t] . \ \forall t : [0,1] . \ | f(t) - p(t) | < \epsilon$$

Now say we have a continuous family of functions $f_x : [0,1] \to \mathbb{R}$ instead. so $f : X \times [0,1] \to \mathbb{R}$ for some topological space $X$. It's reasonable to ask if the polynomials $p_x$ approximating $f_x$ vary continuously in $X$.

We might expect the Weierstrass Approximation Theorem to be constructive. After all, the argument by Bernstein Polynomials actually gives us a sequence in-hand of approximating polynomials.

Then, inside the topos $\mathsf{Sh}(X)$, the theorem is true, and externally we would be able to see that

For all $f : X \times [0,1] \to \mathbb{R}$ continuous, for all $\epsilon > 0$, there is an open cover $U_\alpha$ of $X$ and polynomials $p_\alpha$ with coefficients continuous on $U_\alpha$ so that $|f(x,t) - p_\alpha(x,t)| < \epsilon$ for every $t \in [0,1]$.

which gives us a local solution to our problem.

Unfortunately, in the usual proof that the bernstein polynomials really do approximate $f$ we do the standard analysis trick of separating into "good" and "bad" parts, then we show the good parts are small, and there aren't many bad parts. This uses LEM when we assert that every summand is either good or bad.

From here, it's reasonable to pass to the double negation sheaves $\mathsf{Sh}_{\lnot \lnot}(X)$, where the argument goes through... But I can't figure out how to externalize the claim! I know that $\mathsf{Sh}_{\lnot \lnot}(X)$ is equivalent to sheaves on the locale of regular opens. But usually this is a pointfree locale, and I'm not sure how the (dedekind) real numbers there (which, I think, are continuous maps from the locale of regular opens to the locale $\mathbb{R}$) relates to the real numbers in $\mathsf{Sh}(X)$ (which are continuous maps $X \to \mathbb{R}$). I've heard that truth in the double negation sheaves is the same as "truth on a dense open set", so that our claim reads something like "there is a dense open set $V$ and an open cover $U_\alpha$ of $V$ so that ...." but I'm still not sure if that works.

Any guidance on externalizing statements from the double negation sheaves would be fantastic! Ideally a concrete example like this, with some explanation as to how the translation goes.

(Also, I'm aware of the truly constructive proof in Bridges Constructive Functional Analysis, Chapter $4.3$, which gets us out of this hole. But this is a good case study in working with double negation sheaves, so I would still like to know how to externalize the claim in the more complicated way.)

Answer 1

Very nice idea for a case study!

First, I agree with everything you wrote.

You are right that $\mathrm{Sh}_{\neg\neg}(X)$ coincides with $\mathrm{Sh}(X_{\neg\neg})$, the topos of sheaves over the smallest dense sublocale of $X$. For many kinds of spaces, this sublocale doesn't have any points (even though it is dense in $X$ and hence trivial only if $X$ is trivial). But for some spaces, such as integral schemes or more generally spaces which contain a point $\xi$ such that $\overline{\{\xi\}} = X$, this sublocale will coincide with the one-point subspace $\{\xi\}$, hence will be accessible even without familiarity with pointfree spaces.

But I bet that you don't really need the object of Dedekind reals of $\mathrm{Sh}(X_{\neg\neg})$ (which is the sheaf of continuous maps from opens of $X_{\neg\neg}$ to the (locale of) Dedekind reals).

Rather, you need the $\neg\neg$-sheafification of the object $R$ of Dedekind reals of $\mathrm{Sh}(X)$. These two constructions will not coincide, as forming the set of Dedekind reals is not a geometric construction.

But also, the $\neg\neg$-sheafification of $R$ is easier to describe. Since $R$ is already $\neg\neg$-separated ($\forall x,y:R. \neg\neg(x=y)\Rightarrow x=y$ holds in the internal language), you need to apply the plus construction only once to obtain the sheafification (instead of the usual two times). For details of this construction, see Definition 6.8 in these notes of mine. Roughly speaking, a section of $R^+$ over an open $U$ is a section of $R$ on some dense open $V \subseteq U$, modulo an appropriate equivalence relation.

That said, probably you can even avoid the $\neg\neg$-sheafification of $R$. Instead, you could try to show, constructively, that $$\forall f : C([0,1],\mathbb{R}). \forall \epsilon : \mathbb{R}_{>0}. \neg\neg \exists p : \mathbb{R}[t]. \forall t : [0,1]. |f(t) - p(t)| < \epsilon.$$

I bet that you could mostly copy the classical proof, exploiting the two (awesome!) intuitionistic tautologies $$ \neg\neg(\varphi \vee \neg\varphi) \quad\text{and}\quad \neg\neg\varphi \wedge (\varphi \Rightarrow \psi) \Longrightarrow \neg\neg\psi.$$ They allow you, when proving doubly negated statements, to apply the law of excluded middle a finite number of times. Also useful in this context is the aforementioned $\neg\neg$-separatedness of the reals, which allows you to escape the double negation modaility.

Regarding the connection between "$\neg\neg$" and "on a dense open", we have that $U \models \neg\neg\varphi$ iff the truth value $⟦ \varphi ⟧ = \bigcup \{ V \subseteq U \text{ open} \,|\, V \models \varphi \} \subseteq U$ is dense in $U$ iff there is an open dense $V \subseteq U$ such that $V \models \varphi$.

Hope this answers your question, feel free to ask for more details!