Logical consequences of descent theory

[Bas Spitters <spitters@cs.ru.nl>]

A number of people have suggested that descent theory has been/ can be
used to obtain logical results.

I can sort of see the possible connections:
open surjective maps between toposes are effective descent morphisms.
Viewed logically, such a map is a conservative extension preserving
all first-order structure.

Proper surjective maps are also effective descent morphisms.
Consider an occupied locale X (in Paul Taylor's sense).
I.e. X->1 is a proper surjection.
Then we obtain a proper surjection Sh(X)->Sets.
I.e. we conservatively add a generic point of the occupied space.

The inverse image preserves geometric logic, but does it preserve
anything else in general?
This is probably well-known, but I couldn't find it.

Any suggestions or pointers about the logical interpretation of
descent theory would be appreciated.


Thanks,

Bas


[For admin and other information see: http://www.mta.ca/~cat-dist/ ]