Re: a question of Lubarsky

["Prof. Peter Johnstone" <P.T.Johnstone@dpmms.cam.ac.uk>]

The answer to the general question is surely "no": the sentences
which hold in Sh(X + X) are exactly those which hold in Sh(X).
Whether one can separate Sh(R) from Sh([0,\infty)) in this way
is a more interesting question. Does "Brouwer's continuity theorem"
hold in Sh([0,\infty))? The proof that I know for Sh(R) doesn't
work over [0,\infty), but that may be because it's not the best
proof.

Peter Johnstone

On Thu, 5 Mar 2009, Thomas Streicher wrote:

> Bob Lubarsky has recently asked me a question I could answer only partially.
> He is not reading this mailing list and so I forward his question (since I am
> also interested in it).
> The question is whether for nonisomorphic spaces X and Y one can always find
> a formula in higher order arithmetic or in the language of set theory which
> holds in one of the toposes Sh(X), Sh(Y) but not in the other.
> More concretely he asked about the folowing 4 spaces
>
>  R (reals)        R_{\geq 0} (nonnegative reals)
>
>  Q (rationals)    Q_{\geq 0} (nonnegative rationals)
>
> AC_N holds for sheaves over spaces in the second line but not for sheaves
> over the spaces in the first line.
> But I couldn't tell him how to logically separate R and R_{\geq 0} or
> Q and Q_{\geq 0}.
>
> The background of Bob's question is his work on "forcing with settling down"
> (http://www.math.fau.edu/lubarsky/forcing with settling.pdf) providing a model
> for CZF without Fullness but Exponentiation where, moreover, the Dedekind
> reals are not a set but a proper class.
>
> Thomas
>
>
>