Applications of constructive logic to sheaf constructions in toposes

Abstract

The internal logic of a topos is exploited to give an easy proof of the fact that topologies in a topos form a locale and to give simple internal reformulations of two well-known variants of associated sheaf constructions. We have two applications: (i) we extend Gödel's negative translation to a large class of higher order logics, including HHA and IZF with help of the associated sheaf construction for the double negation topology, (ii) generalizations of our internal notions and constructions are useful to investigate the relations between locales of Lawvere-Tierney topologies, Gabriel-Grothendieck topologies, universal closure operations and locales of localisations of the subcategory of T-algebras in an elementary topos for an arbitrary theory T.