Re: Logic preserved in double negation subtopos?

Re: Logic preserved in double negation subtopos?

[Prof. Peter Johnstone]

The inclusion of double-negation sheaves is an example of what I
called a sub-open map in my paper "Open maps of toposes"
(Manuscripta Math. 31 (1980), 217-247). Sub-open maps have the
property that their inverse image functors commute with implication
-- indeed, one could take that as a definition, although it
wasn't how I defined them in the paper.

Peter Johnstone
----------
On Tue, 2 Sep 2003, Jonas Eliasson wrote:

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

Logic preserved in double negation subtopos?

[Jonas Eliasson]

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