A formulation of D-institution using functor categories
For researchers in institution theory and logic, this provides a potentially simpler framework for handling variables, but the abstract lacks concrete performance numbers or comparisons, making it an incremental contribution.
The paper proposes a new formulation of D-institution using functor categories to directly introduce variable structures, simplifying the axiomatization of logic. It defines a category of predicate logics, formulates compound sentences as a functor, and proves a completeness theorem.
Variables are a crucial element in logic and are also addressed in institution theory, an effort to axiomatize logic. In institution theory, we typically use extensions (signature morphisms) obtained from variables instead of introducing variables directly. While this approach appears simple at first glance because it does not introduce new structures, it often requires numerous conditions to describe variable structures, which can actually complicate the discussion. In this paper, we propose introducing variable structures directly by utilizing a generalization of category of functors. We define a category of predicate logics and formulate the introduction of compound sentences as a functor. We also introduce a proof system and prove a completeness theorem.