一句话：证明模态逻辑T中消去双蕴涵会使公式指数增大，完备布尔基仅分两类；S5则与命题逻辑一致。
该文研究布尔算子基的选择是否影响模态公式的简洁性。命题逻辑中 Pratt 已证明，任一等价完备基之间可多项式翻译；但本文发现模态逻辑 T（因而 K）不同：消去双蕴涵需要指数多个模态算子 ◇，导致公式大小指数增长，因此 De Morgan 基与其加入双蕴涵的扩展在简洁性上不同。作者进一步证明，任何完备布尔算子集在简洁性上都与这两种基之一一致。作为补充，S5 中布尔算子选择不显著影响公式大小，行为类似命题逻辑。结果基于翻译复杂度与指数下界的理论分析。
Is it possible to write significantly smaller formulae when using Boolean operators other than those of the De Morgan basis (and, or, not, and the constants)? For propositional logic, a negative answer was given by Pratt: formulae over one set of operators can always be translated into an equivalent formula over any other complete set of operators with only polynomial increase in size. Surprisingly, for modal logic the picture is different: we show that elimination of bi-implication is only possible at the cost of an exponential number of occurrences of the modal operator $\lozenge$ and therefore of an exponential increase in formula size, i.e., the De Morgan basis and its extension by bi-implication differ in succinctness. Moreover, we prove that any complete set of Boolean operators agrees in succinctness with the De Morgan basis or with its extension by bi-implication. More precisely, these results are shown for the modal logic $\mathrm{T}$ (and therefore for $\mathrm{K}$). We complement them showing that the modal logic $\mathrm{S5}$ behaves as propositional logic: the choice of Boolean operators has no significant impact on the size of formulae.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2408-11651,
title = {Boolean basis, formula size, and number of modal operators},
author = {Christoph Berkholz and Dietrich Kuske and Christian Schwarz},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 3},
year = {2025},
doi = {10.46298/lmcs-21(3:10)2025}
}