Fibered universal algebra for first-order logics

DOI10.1016/J.JPAA.2023.107415MaRDI QIDQ6051097zbMATH OpenOpenAlexFDO

Authors Colin Bloomfield, Yoshihiro Maruyama

Publication date 19 September 2023

Published in Journal of Pure and Applied Algebra (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/2205.05657

abstract algebraic logic Birkoff theorem Blok-Jónsson theorem categorical logic fibred universal algebra general predicate logic generalized quantifiers hyperdoctrine prop-category

Mathematics Subject Classification ID

Other nonclassical logic (03B60) Abstract algebraic logic (03G27) Categorical logic, topoi (03G30) Categorical semantics of formal languages (18C50)

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.

Cites work

This page was built for publication: Fibered universal algebra for first-order logics

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6051097)