Re: a question of Lubarsky

Re: a question of Lubarsky

[Thomas Streicher]

Dear Peter,

> 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).

Thanks for that explict argument. I told Bob a cardinality axiom. In the
languages under consideration there are just countably many formulas but
there are class many non-homeomorphic sober spaces.

> 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.

I don't know which proof you have in mind. Until recently I was just aware
of the argument in the book by MacLane and Moerdijk using a gros topos.
But just now I have found that in Troelstra & van Dalen Ch.15 Thm.3.24 says
that for any completely regular, first countable space T without isolated
points Sh(T) validates Brouwer's Theorem. They attribute it to Grayson.
Thus Brouwer's theorem holds in any of the four spaces mentioned.

Bob tells me that with his forcing with settling he can distinguish R and
[0,\infty) but does not know how to distinguish Q and Q \cap [),\infty).

Thomas

Re: a question of Lubarsky

[Thomas Streicher]

> The cardinality argument also shows a bit more, I guess.  As you've point=
> ed out, the valid formulas in Sh(X) and Sh(Y) will agree if they have the=
>  same soberification / locale, or if Y is a product of X with some discre=
> te space.  However, even after identifying such spaces, there will still =
> be (certainly in classical metatheory, and I think in most weaker theorie=
> s) more than continuum-many classes of spaces; so these "trivial reasons"=
>  can't be the only cases when Sh(X) and Sh(Y) validate the same formulas.

Certainly, yust consider algebraic lattices with their Scott topology. They are
all sober and connected. P(\kappa) for all cardinals \kappa provides a class
of nonisomorphic such gadgets.

BTW Bob suggested to characterise when two sober spaces or locales are
logically indistinguishible. I find this a most difficult questions. Reminds me
a bit (admittedly somewhat vague analogy) of characterising elementary
equivalence of structures. There is an answer by Ehrenfeucht-Fraisse games.
But this can't be use for the question at issue.

Thomas

Re: a question of Lubarsky

[Peter LeFanu Lumsdaine]

> Dear Peter,
>=20
>> 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).
>=20
> Thanks for that explict argument. I told Bob a cardinality axiom. In th=
e=20
> languages under consideration there are just countably many formulas bu=
t=20
> there are class many non-homeomorphic sober spaces.

The cardinality argument also shows a bit more, I guess.  As you've point=
ed out, the valid formulas in Sh(X) and Sh(Y) will agree if they have the=
 same soberification / locale, or if Y is a product of X with some discre=
te space.  However, even after identifying such spaces, there will still =
be (certainly in classical metatheory, and I think in most weaker theorie=
s) more than continuum-many classes of spaces; so these "trivial reasons"=
 can't be the only cases when Sh(X) and Sh(Y) validate the same formulas.

-Peter.

>> Whether one can separate Sh(R) from Sh([0,\infty)) in this way is a mo=
re
>> 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.
>=20
> I don't know which proof you have in mind. Until recently I was just
> aware of the argument in the book by MacLane and Moerdijk using a gros
> topos. But just now I have found that in Troelstra & van Dalen Ch.15
> Thm.3.24 says that for any completely regular, first countable space T
> without isolated points Sh(T) validates Brouwer's Theorem. They attribu=
te
> it to Grayson. Thus Brouwer's theorem holds in any of the four spaces
> mentioned.
>=20
> Bob tells me that with his forcing with settling he can distinguish R a=
nd
>  [0,\infty) but does not know how to distinguish Q and Q \cap [),\infty=
).
>=20
>=20
> Thomas
>=20
>=20
>=20
>=20
>=20


--=20
Peter LeFanu Lumsdaine
Carnegie Mellon University

"I shall cast out Wisdom and reject Learning;
My thoughts shall wander in the silent Void."
        -Hsi K'ang

Re: a question of Lubarsky

[Prof. Peter Johnstone]

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
>
>
>

a question of Lubarsky

[Thomas Streicher]

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