Fibered Universal Algebra for First-Order Logics

Colin Bloomfield, Yoshihiro Maruyama

Published 2022-05-11Version 1

We apply Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a general framework for providing "algebraic" semantics for nonclassical first-order logics. To do so, we extend Lawvere-Pitts prop-categories for a broad variety of algebraic logical structures. We then establish an analogue of the homomorphism theorem from universal algebra for generalized prop-categories, and characterize two natural closure operators on the prop-categorical semantics. The first closes a class of structures (which are interpreted as morphisms of prop-categories) under satisfaction of their common first-order theory and the second closes a class of prop-categories under their associated first-order consequence. It turns out these closure operators have characterizations which closely mirror Birkhoff's characterization of closure under the satisfaction of an equational theory and Blok and J\'onsson's characterization of closure under equational consequence, respectively. These "algebraic" characterizations of the closure operators are unique to the prop-categorical semantics and do not have analogues, for example, in the classical Tarskian semantics of first-order logic. The prop-categories we consider are much more general than traditional intuitionistic prop-categories or triposes (i.e., topos representing indexed partially ordered sets). Nonetheless, to our knowledge, our results are still new even when restricted to these special classes of prop-categories.