发表机构
School of Mathematics, Institute for Research in Fundamental Sciences (IPM)（基础科学研究所数学学院）
机构由 AI 辅助整理，请以论文原文为准。AI 中文总结
本文通过力迫法为模态逻辑的扩张理论建立集合论翻译，证明其可靠性与完备性，并构建相应的Kripke模型。
AI 中文摘要
我们发展了一种对递归可公理化的一阶理论 $T$ 的正规模态扩张 $T_m$ 的集合论翻译。我们首先通过添加见证常量过渡到基础语言的 Henkin 扩张，并研究该扩张的句子代数。该翻译是利用相应的 Lindenbaum-Tarski 代数、其超滤子的 Stone 空间，以及通过 Borel 集的 $\sigma$-理想进行的商力迫构造的；特别地，贫集理想产生 Cohen 力迫，而零集理想产生随机力迫。在布尔值宇宙中，我们通过翻译公式的布尔值在合适的滤子名中的成员关系来解释模态算子 $\Box$。我们证明该翻译是可靠且完备的：一个模态公式在 $T_m$ 中可证明当且仅当它的集合论翻译在每一个相关的解释中都被力迫。然后我们从泛型扩张构建 Kripke 框架和模型，并表明 $\Box$ 的力迫解释与在相应可达关系上的量化一致。作为结果，我们获得了相对于所得 Kripke 模型的完备性。
英文摘要
We develop a set-theoretic translation of a normal modal extension $T_m$ of a recursively axiomatizable first-order theory $T$. We first pass to the Henkin expansion of the underlying language by adding witness constants and work with the sentence algebra of this expansion. The translation is constructed using the corresponding Lindenbaum-Tarski algebra, the Stone space of its ultrafilters, and quotient forcing by a $σ$-ideal of Borel sets; in particular, the meager ideal yields Cohen forcing and the null ideal yields the random forcing. In a Boolean-valued universe, we interpret the modal operator $\Box$ by membership of the Boolean value of the translated formula in a suitable filter name. We prove that this translation is sound and complete: a modal formula is provable in $T_m$ if and only if its set-theoretic translation is forced in every associated interpretation. We then build Kripke frames and models from generic extensions and show that the forcing interpretation of $\Box$ agrees with quantification over the corresponding accessibility relation. As a consequence, we obtain completeness with respect to the resulting Kripke models.
