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