关于 GL 正向片段的一个证明系统

本文提出了一种证明系统 $\mathsf{GL}_{+}^{\top\bot}$，其基于 Dunn 提供的 sequent 系统 $\mathsf{K}_{+}^{\top\bot}$，用于 $\mathsf{GL}$ 的正向片段。正向模态公式是指不包含否定符号或蕴含符号的模态公式。更 precisely 定义为由连接词 $\lor$、$\land$、$\Diamond$、$\Box$、$\bot$、$\top$ 以及命题变量构成的模态公式。逻辑 $\mathsf{GL}$ 是包含 $\mathsf{K}$ 以及 Löb 公式 $\Box(\Box p\supset p)\supset\Box p$ 的最小正规模态逻辑。遵循 Dunn 的定义，sequent 是形式为 $\phi\vdash\psi$ 的表达式，其中 $\phi$ 和 $\psi$ 为正向模态公式。我们提出的证明系统 $\mathsf{GL}_{+}^{\top\bot}$ 具有如下性质：当且仅当 $\phi\supset\psi$ 在 $\mathsf{GL}$ 中可证时，$\phi\vdash\psi$ 才在 $\mathsf{GL}_{+}^{\top\bot}$ 中可证。