Fibered Universal Algebra for First-Order Logics

TL;DR

This paper develops a new algebraic framework for nonclassical first-order logics using extended prop-categories, establishing novel closure operators that generalize classical algebraic semantics.

Contribution

It introduces a generalized prop-categorical semantics for first-order logics, including algebraic closure operators analogous to classical results, extending the scope beyond traditional Tarskian semantics.

Findings

Established a homomorphism theorem extension for prop-categories.

Characterized two natural closure operators mirroring classical algebraic theorems.

Demonstrated the novelty of these operators in the prop-categorical setting.

Abstract

We extend Lawvere-Pitts prop-categories (aka. hyperdoctrines) to develop a general framework for providing "algebraic" semantics for nonclassical first-order logics. This framework includes a natural notion of substitution, which allows first-order logics to be considered as structural closure operators just as propositional logics are in abstract algebraic logic. We then establish an extension 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 the 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 that closely mirror Birkhoff's characterization of the closure of a class of algebras under the satisfaction of their common equational theory and Blok and J\'onsson's characterization of closure under equational consequence, respectively. These "algebraic" characterizations of the first-order closure operators are unique to the prop-categorical semantics and do not have analogs, for example, in the Tarskian semantics for classical 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.