The Geometric Completion of a Doctrine

Abstract

As several different formal systems with inequivalent syntax may describe equivalent semantics, it is possible to find `completions' to more expressive syntaxes that are semantically invariant. Doctrine theory, in the sense of Lawvere, is the natural categorical framework in which to express completions for first-order logic. We study the suitability of a fibred generalisation of the ideal completion of a preorder to act as a completion for doctrines to the syntax of geometric logic. In contrast to other completions of doctrines considered in the literature, our completion takes a Grothendieck topology as a second argument. As a result, the geometric completion is idempotent, as well as being `semantically invariant' for any doctrine whose models can be expressed as a category of continuous flat functors, encompassing a wide class of the most commonly considered doctrines. We also relate the geometric completion to other completions of doctrines considered in the literature: first, by studying the behaviour of the geometric completion when the second argument is omitted, and then by studying the interaction with those completions of doctrines that complete to a fragment of geometric logic. Throughout, we reference how these completions of doctrines yield completions of categories via the syntactic category construction. We demonstrate that it is equivalent to represent logical theories by either doctrines or syntactic categories, in so far as they have equivalent classifying toposes.