非标准模态逻辑的可证性解释及其邻域语义嵌入中的算术完备性

我们从模态逻辑的视角研究满足以下条件的可证性谓词 $\mathrm{Pr}_T(x)$：条件 $\mathbf{E}$：若 $T \vdash \varphi \leftrightarrow \psi$，则 $T \vdash \mathrm{Pr}_T(\ulcorner \varphi \urcorner) \leftrightarrow \mathrm{Pr}_T(\ulcorner \psi \urcorner)$。为此，我们发展了一种基于邻域语义将模型嵌入算术的新方法。该方法拓宽了算术完备性证明的适用范围。特别地，我们证明了非标准模态逻辑 $\mathsf{EN}$、$\mathsf{ECN}$、$\mathsf{ENP}$、$\mathsf{END}$ 和 $\mathsf{ECNP}$ 的算术完备性定理。