{"id":"arxiv/2604.08331","url":"https://arxiv.org/abs/2604.08331","tags":["math.CT","cs.LO"],"score":0,"title":"Metacat: a categorical framework for formal systems","domain":"math.CT","source":"arxiv","authors":["Paul Wilson"],"reviews":0,"subject":"math.CT","summary":"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…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"discussed":0,"published":"2026-04-09","reactions":{}}