Syntax and Consequence Relations -- A Categorical Perspective

TL;DR

This paper introduces a categorical framework to model syntax and inference in logics with algebraic signatures, enhancing understanding of algebraisation and invariance under substitution.

Contribution

It develops a functorial approach to structurality, offering a clearer, more conceptual framework for algebraic semantics and deriving new results.

Findings

Functorial modeling of structurality improves clarity

Provides new insights into algebraisation of logics

Unifies existing results with a categorical perspective

Abstract

In this paper, we use a categorical and functorial set up to model the syntax and inference of logics with algebraic signature, extending previous works on algebraisation of logics. The main feature of this work is that structurality, or invariance under substitution of variables, are modelled by functoriality, resulting in a much clearer framework for algebraic semantics and algebraisation. It also provides a very nice conceptual understanding of various existing results already established in the literatures, and derives several new results as well.