带绑定子的混合逻辑之 Sahlqvist 型完备性理论

在本文中，我们延续 \cite{Zh21c} 中的研究，发展带满足算子与 downarrow 绑定子 $\mathcal{L}(@, \downarrow)$ 的混合逻辑的 Sahlqvist 型完备性理论。我们遵循 \cite{ConRob} 中的思想定义了 $\mathcal{L}(@, \downarrow)$ 的骨架 Sahlqvist 公式类，但采用不同的证明策略，即纯证明论的策略：对每一条骨架 Sahlqvist 公式 $\phi$ 及其混合纯对应 $\pi$，证明 $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+\phi$ 推出 $\pi$，从而 $\mathbf{K}_{\mathcal{H}(@, \downarrow)}+\phi$ 相对于由 $\pi$ 定义的框架类完备，使用的是 \cite{Zh21c} 中定义的算法 $\mathsf{ALBA}^{\downarrow}$ 的一个受限版本。