Japaridze 多态可证性逻辑的多种类变体

我们考虑 Japaridze 多态可证性逻辑 $\mathsf{GLP}$ 的一种多种类变体。在该记为 $\mathsf{GLP}^\ast$ 的变体中，命题变量被赋予排序 $\alpha \leq \omega$，其中有限排序 $n < \omega$ 的变量被解释为算术层级的 $\Pi_{n+1}$-句子，而排序 $\omega$ 的变量遍历任意句子。我们证明 $\mathsf{GLP}^\ast$ 关于此解释是算术完全的。此外，我们将 $\mathsf{GLP}^\ast$ 与其单种类对应物 $\mathsf{GLP}$ 相关联，并证明前者继承了后者的若干已知性质，如 Craig 插值和 PSpace 可判定性。我们还研究了 $\mathsf{GLP}^\ast$ 的一个正变体，它允许更丰富的算术解释——变量被允许遍历理论而非单个句子。这一解释进而允许引入对应于完全一致反射原理的模态。我们证明我们的 $\mathsf{GLP}^\ast$ 正变体是算术完全的。