Logic preserved in double negation subtopos?

[Jonas Eliasson <jonase@math.uu.se>]

While writing a joint paper with Steve Awodey, we came to think about the
following question:

Given a Grothendieck topos Sh(C), what logic is preserved by the
associated sheaf functor from Sh(C) to the double negation subtopos of
Sh(C)?

We know that a: Sh(C) --> DNSh(C) preserves geometric logic. Since it is
double negation it also preserves 0 (falsehood), negation and implication.
>From this you can draw the conclusion that a preserves the validity of
formulas built up from double negation stable predicates without universal
quantifiers.

Presumably this has been studied in the literature, can something stronger
be said about what validities are preserved, could anyone provide a
reference for a general result of this kind?

Grateful for any help,
Jonas Eliasson




 ------------------------------------------
| Jonas Eliasson                           |
| Department of Mathematics                |
| Uppsala University                       |
| Sweden                                   |
| E-mail: jonase@math.uu.se                |
| Homepage: http://www.math.uu.se/~jonase/ |
 ------------------------------------------