Fibred Algebraic Semantics for a Variety of Non-Classical First-Order Logics and Topological Logical Translation

Abstract

Lawvere hyperdoctrines give categorical algebraic semantics for intu- itionistic predicate logic. Here we extend the hyperdoctrinal semantics to a broad variety of substructural predicate logics over the Typed Full Lam- bek Calculus, verifying their completeness with respect to the extended hyperdoctrinal semantics. This yields uniform hyperdoctrinal complete- ness results for numerous logics such as different types of relevant predicate logics and beyond, which are new results on their own; i.e., we give uni- form categorical semantics for a broad variety of non-classical predicate logics. And we introduce an analogue of Lawvere-Tierney topology and cotopology in the hyperdoctrinal setting, which gives a unifying perspec- tive on different logical translations, in particular allowing for a uniform treatment of Girard's exponential translation between linear and intu- itionistic logics and of Kolmogorov's double negation translation between intuitionistic and classical logics. In the hyerdoctrinal conception, type theories are categories, logics over type theories are functors, and logical translations between them, then, are natural transformations, in particu- lar Lawvere-Tierney topologies and cotopologies on hyperdoctrines. The view of logical translations as hyperdoctrinal Lawvere-Tierney topologies and cotopologies have not been elucidated before, and may be seen as a novel contribution of the present work. From a broader perspective, this work may be regarded as taking first steps towards interplay between al- gebraic and categorical logic; it is, technically, a combination of substruc- tural (or Lambekian) algebraic logic and hyperdoctrinal (or Lawverian) categorical logic, as the hyperdoctrinal completeness theorem is shown via the integration of the Lindenbaum-Tarski algebra construction with the syntactic category construction. As such this work lays a foundation for further interactions between algebraic and categorical logic. Show more