Proof Identity and Categorical Models of BV

TL;DR

This paper introduces a proof identity concept for BV logic using atomic flows, strengthening BV-categories and establishing their soundness with respect to the logic.

Contribution

It defines a new proof identity notion for BV and enhances BV-categories to clarify their relation to BV logic.

Findings

Defined proof identity for BV based on atomic flows.

Strengthened BV-categories to align with the logic.

Proved the soundness of the enhanced BV-categories.

Abstract

BV-categories are a recent development that aims to give categorical semantics to proofs in the logic BV. However, due to the absence of a coherence theorem on one side and a well-defined notion of proof identity for BV on the other side, the precise relation between BV-categories and the logic BV is still not clear. To improve on this situation, we define in this paper a notion of proof identity for BV, based on the notion of atomic flows, which can be seen as a special form of string diagrams. Based on this notion of proof identity, we then strengthen the existing notion of BV-category and prove that it is sound with respect to the logic.