Metacat: a categorical framework for formal systems
This work provides a novel categorical approach for formalizing inference systems, which could benefit researchers in logic and proof theory, though it appears incremental in building on existing categorical methods.
The authors tackled the problem of representing formal systems and inference rules by introducing a categorical framework where rules with metavariables are modeled using spans in a cartesian PROP, enabling composition via substitution. They developed a proof-checking algorithm, implemented it open-source, and demonstrated its application by encoding first-order logic with examples.
We present a categorical framework for formal systems in which inference rules with $m$ metavariables over a category of syntax $\mathscr{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 $\mathscr{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.