Metacat: a categorical framework for formal systems
Fuente:
arXiv
Guardado en:
| Autor principal: | |
|---|---|
| Formato: | Preprint |
| Publicado: |
2026
|
| Materias: | |
| Acceso en línea: | |
| Etiquetas: |
Agregar Etiqueta
Sin Etiquetas, Sea el primero en etiquetar este registro!
|
| _version_ | 1866910116797743104 |
|---|---|
| author | Wilson, Paul |
| author_facet | Wilson, Paul |
| contents | 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. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2604_08331 |
| institution | arXiv |
| publishDate | 2026 |
| record_format | arxiv |
| spellingShingle | Metacat: a categorical framework for formal systems Wilson, Paul Category Theory Logic in Computer Science 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. |
| title | Metacat: a categorical framework for formal systems |
| topic | Category Theory Logic in Computer Science |
| url | https://arxiv.org/abs/2604.08331 |