AI 中文总结
本文给出S4嵌入BBI的全新句法证明，证明其在S4任意公理扩张下稳定，可扩展至BBI的多种语言扩张，还给出BBI演绎定理的首个完整证明。
AI 中文摘要
我们给出了经典模态逻辑S4嵌入到布尔分组蕴含逻辑（BBI）的新证明。原始证明是语义性的，而本证明完全是句法性的，通过希尔伯特式演算进行，且借鉴了哥德尔新近发现的直觉主义命题逻辑嵌入S4的证明思路。我们给出了BBI演绎定理的首个完整证明，用于证明该嵌入在假设推理中保持成立，包括假设被组织成分组的情况。与现有证明不同，我们的证明在S4的任意公理扩张下保持稳定，适用于文献中所有已知的BBI公理扩张。我们阐明了该嵌入与两种逻辑语义性质的关联，且该证明可自然扩展到BBI的语言扩张，如混合BBI、经典BI和亚经典BBI。
英文摘要
We present a new proof of the embedding of the classical modal logic S4 into the logic of Boolean Bunched Implications (BBI). While the original proof is semantical, this proof is entirely syntactical. It proceeds via Hilbert-style calculi, and is built by analogy with a recently discovered proof by Godel of the embedding of intuitionistic propositional logic into S4. We present the first full proofs of deduction theorems for BBI, which are used to show that the embedding is preserved by reasoning with assumptions, including where those assumptions are organised into bunches. Unlike the existing proof, our proof is stable under arbitrary axiomatic extensions of S4, and applies to all known axiomatic extensions of BBI in the literature. We observe how this embedding is related to semantical properties of both logics. Moreover, the proof extends gracefully to language extensions of BBI, as we show with hybrid BBI, classical BI, and sub-classical BBI.
