We provide a general and syntactically-defined family of sequent calculi, called \emph{semi-analytic}, to formalize the informal notion of a "nice" sequent calculus. We show that any sufficiently strong (multimodal) substructural logic with a semi-analytic sequent calculus enjoys the Craig Interpolation Property, CIP. As a positive application, our theorem provides a uniform and modular method to prove the CIP for several multimodal substructural logics, including many fragments and variants of linear logic. More interestingly, on the negative side, it employs the lack of the CIP in almost all substructural, superintuitionistic and modal logics to provide a formal proof for the well-known intuition that almost all logics do not have a "nice" sequent calculus. More precisely, we show that many substructural logics including $\mathsf{UL^-}$, $\mathsf{MTL}$, $\mathsf{R}$, $\mathsf{L}_n$ (for $n \geq 3$), $\mathsf{G}_n$ (for $n \geq 4$), and almost all extensions of $\mathsf{IMTL}$, $\mathsf{L}$, $\mathsf{BL}$, $\mathsf{RM^e}$, $\mathsf{IPC}$, $\mathsf{S4}$, and $\mathsf{Grz}$, (except for at most 1, 1, 3, 8, 7, 37, and 6 of them, respectively) do not have a semi-analytic calculus. Keywords. Craig interpolation, sequent calculi, substructural logics, linear logics, subexponential modalities

翻译：我们提出了一类通用且句法定义的相继式演算族，称为\emph{半解析}演算，用以形式化“良好”相继式演算这一非形式化概念。我们证明，任何具有半解析相继式演算的足够强（多模态）子结构逻辑都满足Craig插值性质（CIP）。在积极应用方面，我们的定理为证明多种多模态子结构逻辑（包括线性逻辑的诸多片段与变体）的CIP提供了一种统一且模块化的方法。更有趣的是，在消极方面，该定理利用几乎所有子结构逻辑、超直觉主义逻辑及模态逻辑中CIP的缺失，为“几乎所有逻辑都不具备‘良好’相继式演算”这一广为人知的直觉提供了形式化证明。更精确地说，我们证明许多子结构逻辑，包括 $\mathsf{UL^-}$、$\mathsf{MTL}$、$\mathsf{R}$、$\mathsf{L}_n$（对于 $n \geq 3$）、$\mathsf{G}_n$（对于 $n \geq 4$），以及几乎所有的 $\mathsf{IMTL}$、$\mathsf{L}$、$\mathsf{BL}$、$\mathsf{RM^e}$、$\mathsf{IPC}$、$\mathsf{S4}$ 和 $\mathsf{Grz}$ 的扩展（分别最多只有1、1、3、8、7、37和6个例外），都不具有半解析演算。关键词：Craig插值，相继式演算，子结构逻辑，线性逻辑，次指数模态