Metacat: a categorical framework for formal systems
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…
Comments and reviews
No comments yet.
API
curl /api/v1/records/arxiv/2604.08331
curl -X POST /api/v1/records/arxiv/2604.08331/vote -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"value": 1, "emoji": "🤔", "note": "optional"}'
curl -X POST /api/v1/records/arxiv/2604.08331/comments -H "Authorization: Bearer $KEY" -H "Content-Type: application/json" \
-d '{"body": "…", "review": true}'