Graphical Regular Logic

Understand

Regular logic can be regarded as the internal language of regular categories, but the logic itself is generally not given a categorical treatment.

• In this paper, we understand the syntax and proof rules of regular logic in terms of the free regular category $\mathsf{FRg}(\mathrm{T})$ on a set $\mathrm{T}$.
• From this point of view, regular theories are certain monoidal 2-functors from a suitable 2-category of contexts---the 2-category of relations in $\mathsf{FRg}(\mathrm{T})$---to the 2-category of posets.
• Such functors assign to each context the set of formulas in that context, ordered by entailment.