A Categorical Integration of Logical Connectives via Higher Category Theory
Barreto Joaquim Reizi
TL;DR
The paper presents a systematic framework to integrate local categorical models of logical connectives into a unified 2-category setting, using natural isomorphisms to manage coherence. It defines local categories for negation, conjunction, disjunction, and implication via dualizing objects, products, coproducts, and exponentials, and then elevates them to a 2-category with 2-morphisms to capture coherence. The integration employs direct product, bifunctors, and pseudo-limits/pseudo-colimits to glue these local structures while preserving universal properties up to isomorphism. A strictification step then converts the resulting bicategorical structure into a strict 2-category, preserving universality via a biequivalence and enabling clearer reasoning through strict associativity and unit laws. The framework is validated through diagrammatic coherence arguments and concrete logical transformations such as Curryfication, demonstrating potential applications in type theory, programming language semantics, and formal verification.
Abstract
This paper develops a systematic framework for integrating local categories that model logical connectives using higher category theory. By extending these local categories into a unified two-category enriched with natural isomorphisms, the universal properties of logical operations such as negation, conjunction, disjunction, and implication are rigorously captured. Advanced techniques including pseudo-limits, pseudo-colimits, and strictification are employed to transform the resulting weak structure into a strict two-category, thereby simplifying composition rules and coherence verification without loss of semantic content. The framework is validated through detailed diagrammatic proofs and concrete examples, demonstrating its robustness and potential impact in areas such as type theory, programming language semantics, and formal verification.