Yes, Cockett and Seely's comment about proof theory is a reference to the theory/category adjunction. Each kind of theory corresponds to a kind of category, for instance:
| Theory |
Category |
| simply typed lambda-calculus |
cartesian closed category |
| intuitionistic multiplicative linear logic |
closed symmetric monoidal category |
| classical multiplicative linear logic with $\otimes,⅋$, and negation |
$\ast$-autonomous category = linearly distributive category with duals |
| classical multiplicative linear logic with $\otimes$ and ⅋ only |
linearly distributive category |
In between the theories and the above "categories with structure", there are notions like multicategories and polycategories that represent the judgmental structure of a theory only, and in which connectives can be characterized by universal properties yielding a structure equivalent to the above categories with structure.
For instance, IMLL has sequents of the form $A_1,\dots,A_m \vdash B$, corresponding to the homsets of a multicategory, in which $\otimes,\multimap$ can be given universal properties yielding a CSMC. Similarly, CMLL has sequents of the form $A_1,\dots,A_m \vdash B_1,\dots,B_n$, corresponding to the homsets of a polycategory, and in which $\otimes,⅋,(-)^\perp$ can be given universal properties. A polycategory in which only $\otimes,⅋$ exist is equivalent to a linearly distributive category, while if it also has duals $(-)^\perp$ it is equivalent to a $\ast$-autonomous category. I think this adding of duals is what Cockett and Seely are referring to "build up" -- starting from a linearly distributive category you can add an assumption of duals to obtain the structure corresponding to full CMLL (namely, a $\ast$-autonomous category).
Your quote from Blute and Scott is, I believe, a reference to this connection between linearly distributive and $\ast$-autonomous categories. The usual definition of a $\ast$-autonomous category involves only $\otimes$ and duals, from which ⅋ can be constructed; so I think they are contrasting this with linearly distributive categories, which have $\otimes,⅋$, in terms of which duals can be characterized (though they may not always exist).
Finally, the sentence about the Gentzen cut rule is a reference to the equivalence between polycategories with $\otimes$,⅋ and linearly distributive categories. Given a linearly distributive category $\cal C$, we define the polycategorical morphisms $(A_1,\dots,A_m) \to (B_1,\dots,B_n)$ to be the morphisms $A_1 \otimes \cdots \otimes A_m \to B_1 ⅋ \cdots ⅋ B_n$ in $\cal C$. The linear distributivities are then used to construct the polycategorical composition on these morphisms.
The simplest nontrivial case is composing a morphism $A \to (B,C)$ with a morphism $(C,D) \to E$, which should yield a morphism $(A,D) \to (B,E)$. This is an instance of polycategorical composition, which is a categorical representation of the cut rule for CLL:
$$ \frac{A \vdash B,C \qquad C,D \vdash E}{A,D \vdash B,E}$$
To construct such a composition in a linearly distributive category, we have morphisms $A\to B⅋C$ and $C\otimes D\to E$, and we can form the composite
$$A\otimes D \to (B⅋C) \otimes D \to B ⅋(C\otimes D) \to B ⅋E$$
using the linear distributivity in the middle.
Best Answer
In general, a theory is called proper if every sort is nonempty (in every model) and there is a sort which has (in every model) at least two elements. Then we have the following theorem: if $\mathbb{T}$ is any proper theory, the syntactic category of $\mathbb{T}^{eq}$ is a pretopos. This is a consequence of the following (non trivial) theorem, which is a generalization of the result found in [1]: call a coherent category proper if every object is a subobject of a nonempty one and if there is a decidable object $D$ such that $D$ and $\neg D$ are nonempty, where $\neg D$ is the complement of the diagonal $\Delta: D \to D \times D$. Then the theorem says that any proper coherent exact category is a pretopos.
In the case of a classical first-order theory, whose models have at least two elements, the syntactic category of $\mathbb{T}^{eq}$ is an exact coherent category, and it will be proper, since $\mathbb{T}$ is. Hence, it is a pretopos and thus it has disjoint coproducts. In fact, for a proper coherent category, the exact completion and the coproduct completion are equivalent.
[1] Victor Harnik: "Model theory vs. categorical logic: two approaches to pretopos completion". In Bradd Hart et al., editor, Models, logics, and higher-dimensional categories: a tribute to the work of Mihaly Makkai, volume 53 of CRM Proceedings and Lecture Notes. American Mathematical Society, Providence, R.I., 2011.