In the internal language of the topos of sheaves on a topological space, can we define locally constant real-valued functions?

Question

For the purposes of this question, in a Grothendieck topos, we will call “definable” the objects and relations obtained from the terminal object, the natural numbers object and the subobject classifier, by taking finite products, finite coproducts, exponentials (internal homs) and taking subobjects defined by [edit 2021-02-16] finitary formulas in the internal language (using previously defined objects and relations). (I'm saying this a bit concisely in the hope that there are no major subtleties.)

In particular, if $X$ is a topological space and we consider the topos of sheaves on $X$, the sheaf of continuous functions with values in each one of the following is definable (along with its usual algebraic structure):

• $\mathbb{N}$ with the discrete topology (this is the natural numbers object),

• $\mathbb{Z}$ with the discrete topology (this is the Grothendieck group of the previous),

• $\mathbb{Q}$ with the discrete topology (this is the fraction field of the previous),

• $\mathbb{R}$ with the usual (Euclidean) topology (by Dedekind cuts).

Let us call $\mathbf{N}, \mathbf{Z}, \mathbf{Q}, \mathbf{R}$ the corresponding definable objects of the topos.

Now for a long time I thought one could not define the sheaf of continuous functions with values in

• $\mathbb{Q}$ with the usual (i.e. induced by $\mathbb{R}$) topology,

but I serendipitously realized that you can, namely it is given by the following object:

$$\{x\in\mathbf{R} : \forall y\in\mathbf{R}. ((\forall z\in\mathbf{Q}.(y\mathrel{\#}z)) \Rightarrow (x\mathrel{\#}y))\}$$

where $x\mathrel{\#}y$ stands for $(x<y)\lor(x>y)$ or, equivalently, $\exists z\in\mathbf{R}.(z\cdot(x-y)=1)$.

(This is easy to see: first note that $\{x\in\mathbf{R} : \forall y\in\mathbf{Q}. (x\mathrel{\#}y)\}$ defines the sheaf of continuous functions with values in $\mathbb{R}\setminus\mathbb{Q}$ with the usual topology, then repeat the reasoning.)

So now I am curious to know whether the “converse” is possible:

• $\mathbb{R}$ with the discrete topology;

in other words:

Question: is the sheaf of locally constant real-valued functions on $X$ definable, uniformly in $X$, as a subobject of $\mathbf{R}$ in the topos of sheaves on $X$?

I imagine there is little hope of finding a good answer to the very general question “for which topological spaces $Y$ is the sheaf of continuous $Y$-valued functions on $X$ definable as an object in the topos?”, but of course, if someone wants a crack at it rather than the particular case above, by all means do!

Answer 1

I can offer a helpful observation. Andrew Swan and I proved in Every metric space is separable in function realizability that in Kleene's function realizability topos every metric space is separable. One consequence of this is that in the internal language of a topos one cannot construct a non-separable metric space, or an uncountable set with decidable equality. Moreover, it is consistent to assume that every set with decidable equality is countable (Theorem 2.5, but see the comment following it.)

While this is not a complete answer to your question, it shows that if there is a definition of the discrete $\mathbb{R}$ in sheaves, we will not be able to prove intuitionistically that it is uncountable and has decidable equality.

Answer 2

It seems to me that for any set $S$ (e.g. $S = \mathbb R$), the classifying topos for locally-constant $S$-valued functions is the slice topos $Set/S$ of $S$-indexed sets, as this is equivalent to the topos of sheaves on $S$ regarded as a discrete topological space.

So because locally-constant $S$-valued functions admit a classifying topos, they can be axiomatized by a theory $T_S$ in geometric logic. I don't know what the axiomatization says, exactly, but one should be able to work it out from the literature. I don't know if a truly infinitary definition in geometric logic counts as "definable" for you, but I think this gives some form of positive answer.

If "locally constant $\mathbb R$-valued function" is supposed to mean something more closely related to the internal Dedekind reals $\mathbf R$ which doesn't agree with $T_{\mathbb R}$, then it's not clear to me what this distinct meaning is supposed to be. That is, if the theory $T_{\mathbb R}$ is not what you're looking for, then what is an example of a topos $\mathcal E$ where locally-constant $\mathbf R$-valued functions are not the same as models of $T_{\mathbb R}$?