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

翻译：我们提出一个通用且语法定义的相继式演算族，称为半分析演算，用以形式化“优质”相继式演算的非正式概念。我们证明，任何具有半分析相继式演算的足够强的（多模态）子结构逻辑都享有克雷格插值性质（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种例外）都不具有半分析演算。关键词：克雷格插值，相继式演算，子结构逻辑，线性逻辑，子指数模态词