On inclusions between quantified provability logics

有限克里普克模型与量化模态逻辑中的可证明性解释

Finite Kripke models and provability interpretations in quantified modal logic

本文研究了有限克里普克模型在量化模态逻辑中的算术完备性，通过Artemov和Japaridze的有限模型嵌入技术，构建了两种不同场景下的可证明性谓词和算术解释。

海廷算术可证性逻辑的严格正片段

Strictly Positive Fragments of the Provability Logic of Heyting Arithmetic

本文确定了海廷算术量词可证性逻辑的严格正片段，证明其可判定且与皮亚诺算术的对应片段一致，并给出了严格正片段的简单公理化，解决了先前猜想。

Quantified Reflection Calculus with one modality

This paper presents the logic QRC$_1$, which is a strictly positive fragment of quantified modal logic. The intended reading of the diamond modality is that of consistency of a formal theory. Predicate symbols are interpreted as parametrized axiomatizations. We prove arithmetical soundness of the logic QRC$_1$ with respect to this arithmetical interpretation. Quantified provability logic is known to be undecidable. However, the undecidability proof cannot be performed in our signature and arithmetical reading. We conjecture the logic QRC$_1$ to be arithmetically complete. This paper takes the …

对Vardanyan定理的一种突破

An Escape from Vardanyan's Theorem

针对Vardanyan定理关于皮亚诺算术量化可证性逻辑不可计算公理化的结论在严格正签名下无法证明的问题，研究推广Kripke可靠性与完全性证明得常域完全性，通过Solovay型构造证明QRC₁系统的算术语义完全性，明确其为QGL严格正片段及QPL(PA)的片段。