A logic has uniform interpolation if its formulas can be projected down to given subsignatures, preserving all logical consequences that do not mention the removed symbols; the weaker property of (Craig) interpolation allows the projected formula -- the interpolant -- to be different for each logical consequence of the original formula. These properties are of importance, e.g., in the modularization of logical theories. We study interpolation in the context of coalgebraic modal logics, i.e. modal logics axiomatized in rank 1, restricting for clarity to the case with finitely many modalities. Examples of such logics include the modal logics K and KD, neighbourhood logic and its monotone variant, finite-monoid-weighted logics, and coalition logic. We introduce a notion of one-step (uniform) interpolation, which refers only to a restricted logic without nesting of modalities, and show that a coalgebraic modal logic has uniform interpolation if it has one-step interpolation. Moreover, we identify preservation of finite surjective weak pullbacks as a sufficient, and in the monotone case necessary, condition for one-step interpolation. We thus prove or reprove uniform interpolation for most of the examples listed above.
翻译:如果其公式可以投向给定的子符号,逻辑就具有统一的内推法,如果其公式可以投向给定的子符号,则逻辑的内推法具有统一的内推法,保留所有不提及被删除符号的逻辑后果;(Craig)内推法的较弱属性使得预测的公式 -- -- 中间推法 -- -- 与原始公式的每个逻辑后果不同。这些属性很重要,例如在逻辑理论的模块化方面。我们研究在煤热模型逻辑背景下的内推法,即模型逻辑在1级中分解,限制对案件的清晰度,采用有限的多种模式。这些逻辑的例子包括模型逻辑K和KD、邻接逻辑及其单元变式、定式加权逻辑和联合逻辑。我们引入了一步(单调)的内推法概念,它仅指一种不固定模式的限制性逻辑,并且表明,如果有一步骤的内推法,那么煤化模型的内推法就具有统一的内推法性。此外,我们确定在单项上保留有限的可辨微弱拉动的后推法,从而能够将单列一个中间进行。