AI 中文总结
该文研究模态逻辑框架可定义性的反数学强度，证明估值扩张引理等相关原则与二阶算术子系统$\text{ACA}^{+}_0}$等价，还考察了CTL、LTL对应原则的强度。
AI 中文摘要
我们研究模态逻辑中框架可定义性的反数学强度，核心原则是估值扩张引理（VEL），其断言框架上的每个命题变量赋值都可扩张为完全估值。我们证明，在$\text{RCA}_0}$上，VEL等价于$\text{ACA}^{+}_0}$，Geach公理和$\text{GL}$的框架可定义性原则也与之等价；我们还得到模态谓词逻辑中Barcan公式和逆Barcan公式的类似$\text{ACA}^{+}_0}$等价关系；最后，我们考察$\text{CTL}$和$\text{LTL}$的VEL变体，并确定它们的强度处于二阶算术的熟悉子系统之间。
英文摘要
We study the reverse-mathematical strength of frame definability in modal logic. The central principle is the Valuation Extension Lemma (VEL), which asserts that every assignment of propositional variables on a frame extends to a full valuation. We show that, over $\mathrm{RCA}_0$, VEL is equivalent to $\mathrm{ACA}^{+}_0$, and as are frame-definability principles for Geach axioms and for $\mathbf{GL}$. We also obtain analogous $\mathrm{ACA}^{+}_0$-equivalences for the Barcan and Converse Barcan formulas in modal predicate logic. Finally, we examine variants of VEL for $\mathbf{CTL}$ and $\mathbf{LTL}$ and locate their strengths between familiar subsystems of second-order arithmetic.
