An Escape from Vardanyan's Theorem

Abstract

Vardanyan’s Theorems state that QPL(PA) - the quantified provability logic of Peano Arithmetic - is Π02 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 QRC1 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 QRC1 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 QRC1 is the strictly positive fragment of QGL and a fragment of QPL(PA).

Keywords

Modal logic, provability logic, strictly positive logics, quantified modal logic, arithmetic interpretations, feasible fragments

Citation

de Almeida Borges, A. & Joosten, J. J. (2023). An escape from Vardanyan's Theorem. The Journal of Symbolic Logic, 88(4), 1613–1638. URL: https://www.cambridge.org/core/services/aop-cambridge-core/content/view/03E13D4C282563F918AF77CF6E2830DA/S002248122200038Xa.pdf/an-escape-from-vardanyans-theorem.pdf, doi:10.1017/jsl.2022.38

@Article{AlmeidaBorges_Joosten2023_Escape,
  author = "{de Almeida Borges}, Ana and Joosten, Joost J.",
  title = "An Escape from {V}ardanyan's {T}heorem",
  journal = "The Journal of Symbolic Logic",
  year = "2023",
  volume = "88",
  number = "4",
  publisher = "Cambridge University Press",
  pages = "1613--1638",
  url = "https://www.cambridge.org/core/services/aop-cambridge-core/content/view/03E13D4C282563F918AF77CF6E2830DA/S002248122200038Xa.pdf/an-escape-from-vardanyans-theorem.pdf",
  doi = "10.1017/jsl.2022.38",
  keywords = "Modal logic, provability logic, strictly positive logics, quantified modal logic, arithmetic interpretations, feasible fragments",
  abstract = "Vardanyan’s Theorems state that QPL(PA) - the quantified provability logic of Peano Arithmetic - is Π02 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 QRC1 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 QRC1 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 QRC1 is the strictly positive fragment of QGL and a fragment of QPL(PA)."
}