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
Dear Peter, =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