Modal Hyperdoctrine: Higher-Order and Non-normal Extensions

Lawvere hyperdoctrines give categorical semantics for intuitionistic predicate logic but are flexible enough to be applied to other logics and extended to higher-order systems. We return to Ghilardi’s hyperdoctrine semantics for first-order modal logic [3] and extend it in two directions—to weaker, non-normal modal logics and to higher-order modal logics. We also relate S4 modal hyperdoctrines to intuitionistic hyperdoctrines via a hyperdoctrinal version of the Gödel-McKinsey-Tarski translation. This work is intended to complement the other categorical semantics that have been developed for quantified modal logic, and may also be regarded as first steps to extend coalgebraic modal logic to first-order and higher-order settings via hyperdoctrines.