不使用尖括号的直觉主义哥德尔-勒布理论

《ACM Transactions on Computational Logic》：Intuitionistic G?del-L?b without Sharps

直觉主义G?del-L?b逻辑的循环证明系统及完全性定理研究，采用非well-founded证明并满足进步性条件，通过ZFC无法证实的Σ1?-决定性原理实现原系统完全性证明。

　　

摘要

Das、van der Giessen 和 Marin 最近提出了一个直观主义的 G?del-L?b 逻辑版本，称为 $\mathrm{IGL}$。他们的证明系统包含了带有渐进性条件的不完备证明。他们的完备性证明利用了 ${\Sigma }_1^1$-确定性原理；而这一原理在 $\mathrm{ZFC}$ 中是无法证明的。我们为 $\mathrm{IGL}$ 定义了一个循环证明系统，并给出了一个避免使用 ${\Sigma }_1^1$-确定性的完备性定理证明。