Metacat: a categorical framework for formal systems

TL;DR

Metacat introduces a categorical framework for formal systems that models inference rules and proofs using spans and monoidal categories, enabling proof checking and implementation.

Contribution

It provides a novel categorical formalism for representing inference rules and proofs, with an implementation and application to first-order logic.

Findings

Proof-checking algorithm implemented and demonstrated.

Categorical encoding of first-order logic inference rules.

Open-source tool for defining and verifying formal systems.

Abstract

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.