对Vardanyan定理的一种突破
An Escape from Vardanyan's Theorem
AI总结：
针对Vardanyan定理关于皮亚诺算术量化可证性逻辑不可计算公理化的结论在严格正签名下无法证明的问题，研究推广Kripke可靠性与完全性证明得常域完全性，通过Solovay型构造证明QRC₁系统的算术语义完全性，明确其为QGL严格正片段及QPL(PA)的片段。
摘要：
Vardanyan定理指出，$\u276aQPL\u276b(\u276aPA\u276b)$——即Peano算术的量化可证性逻辑——是$Π^0_2$完全的，且即便将语言限制为仅含一个一元谓词，该结论依然成立。此外，Visser和de Jonge推广了这一结果，得出结论：对于一大类理论，其量化可证性逻辑无法被可计算公理化。然而，这一结论的证明无法在严格正的签名中完成。$\u276aQRC_1\u276b$系统是作者此前提出的一阶可证性逻辑候选。本文中，我们推广了已有的Kripke可靠性与完全性证明，得到常域完全性。随后我们证明，$\u276aQRC_1\u276b$相对于算术语义确实是完全的，这一结果通过将Solovay型构造应用于常域Kripke模型实现。作为推论，我们得出$\u276aQRC_1\u276b$是$\u276aQGL\u276b$的严格正片段，同时也是$\u276aQPL\u276b(\u276aPA\u276b)$的一个片段。
英文摘要：
Vardanyan's Theorems state that $\mathsf{QPL}(\mathsf{PA})$ - the quantified provability logic of Peano Arithmetic - is $Π^0_2$ complete, and in particular that this already holds when the language is restricted to a single unary predicate. Moreover, Visser and de Jonge generalized this result to conclude that it is impossible to computably axiomatize the quantified provability logic of a wide class of theories. However, the proof of this fact cannot be performed in a strictly positive signature. The system $\mathsf{QRC}_1$ was previously introduced by the authors as a candidate first-order provability logic. Here we generalize the previously available Kripke soundness and completeness proofs, obtaining constant domain completeness. Then we show that $\mathsf{QRC}_1$ is indeed complete with respect to arithmetical semantics. This is achieved via a Solovay-type construction applied to constant domain Kripke models. As corollaries, we see that $\mathsf{QRC}_1$ is the strictly positive fragment of $\mathsf{QGL}$ and a fragment of $\mathsf{QPL}(\mathsf{PA})$.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
