Topological representation of geometric theories

Abstract Using Butz and Moerdijk's topological groupoid representation of a topos with enough points, a ‘syntax‐semantics’ duality for geometric theories is constructed. The emphasis is on a logical presentation, starting with a description of the semantic topological groupoid of models and isomorphisms of a theory. It is then shown how to extract a theory from equivariant sheaves on a topological groupoid in such a way that the result is a contravariant adjunction between theories and groupoids, the restriction of which is a duality between theories with enough models and semantic groupoids. Technically a variant of the syntax‐semantics duality constructed in 1 for first‐order logic, the construction here works for arbitrary geometric theories and uses a slice construction on the side of groupoids—reflecting the use of ‘indexed’ models in the representation theorem—which in several respects simplifies the construction and the characterization of semantic groupoids.