Metacat: a categorical framework for formal systems

Abstract

We present a categorical framework for formal systems in which inference rules with $m$ metavariables over a category of syntax $\mathcal{S}$, taken to be a cartesian PROP, are represented by operations of arity $k\to n$ equipped with spans $k\leftarrow m\to n$ in $\mathcal{S}$, encoding the hypotheses and conclusions in a common metavariable context. Composition is by substitution of metavariables, which is the sole primitive operation, as in Metamath. Proofs in this setting form a symmetric monoidal category whose monoidal structure encodes the combination and reuse of hypotheses. This structure admits a proof-checking algorithm; we provide an open-source implementation together with a surface syntax for defining formal systems. As a demonstration, we encode the formulae and inference rules of first-order logic in Metacat, and give axioms and representative derivations as examples.