This chapter describes the categorical proof theory of the cut rule, a very basic component of any sequent-style presentation of a logic, assuming a minimum of structural rules and connectives, in fact, starting with none. It is shown how logical features can be added to this basic logic in a modular fashion, at each stage showing the appropriate corresponding categorical semantics of the proof theory, starting with multicategories, and moving to linearly distributive categories and *-autonomous categories. A key tool is the use of graphical representations of proofs (“proof circuits”) to represent formal derivations in these logics. This is a powerful symbolism, which on the one hand is a formal mathematical language, but crucially, at the same time, has an intuitive graphical representation.
Trade-offs for fully dynamic transitive closure on DAGs: breaking through the
O
(
n
2
barrier