A formulation of D-institution using functor categories

TL;DR

This paper proposes a new way to incorporate variables directly into institution theory using functor categories, simplifying the description of variable structures and establishing a proof system with completeness.

Contribution

It introduces a novel categorical formulation of variables in institution theory through functor categories, providing a more direct and simplified approach.

Findings

Defined a category of predicate logics

Formulated compound sentences as a functor

Proved a completeness theorem for the proof system

Abstract

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.