可证性逻辑在序数空间上的强完备性

Abashidze 和 Blass 独立证明了模态逻辑 $\sf{GL}$ 在任何配备区间拓扑且大于等于 $\omega^\omega$ 的序数上的拓扑解释是完备的。Icard 随后引入了一族拓扑 $\mathcal I_\lambda$（$\lambda < \omega$），旨在为 Japaridze 的多模态逻辑 $\sf{GLP}$ $_{\omega}$ 提供语义。Icard 的构造随后被 Joosten 和本文第二作者推广至任意序数 $\lambda \geq \omega$。在本文中，我们进一步推广 Icard 拓扑。给定一个分散空间 $\mathfrak X = (X, \tau)$ 和一个序数 $\lambda$，我们定义一个拓扑 $\tau_{+\lambda}$，使得当 $\mathfrak X$ 是赋予左拓扑的序数时，$\tau_{+0}$ 为原始拓扑 $\tau$，且 $\tau_{+\lambda}$ 与 $\mathcal I_\lambda$ 一致。然后我们证明，给定任何分散空间 $\mathfrak X$ 和任何序数 $\lambda>0$，只要 $(X, \tau)$ 的秩足够大，$\sf{GL}$ 对于 $\tau_{+\lambda}$ 就是强完备的。作为 $\mathfrak X=\omega^\omega$ 且 $\lambda=1$ 这一特殊情形的推论，即可得到原始的 Abashidze-Blass 定理。