Quantified Reflection Calculus with one modality

Abstract

This paper presents the logic QRC1, 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 QRC1 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 QRC1 to be arithmetically complete. This paper takes the first steps towards arithmetical completeness by providing relational semantics for QRC1 with a corresponding completeness proof. We further show the finite model property with respect to domains and number of worlds, which implies decidability.

Keywords

Provability logic, strictly positive logics, quantified modal logic, arithmetic interpretations, feasible fragments, decidable logics, finite model property

Citation

de Almeida Borges, A. & Joosten, J. J. (2020). Olivetti, N., Verbrugge, R., Negri, S., & Sandu, G. (Eds.). Quantified Reflection Calculus with one modality. Advances in Modal Logic 13 (pp. 13–32). College Publications. URL: http://www.aiml.net/volumes/volume13/deAlmeidaBorges-Joosten.pdf

@InProceedings{AlmeidaBorges_Joosten2020_QRC1,
  author = "{de Almeida Borges}, Ana and Joosten, Joost J.",
  editor = "Olivetti, Nicola and Verbrugge, Rineke and Negri, Sara and Sandu, Gabriel",
  title = "{Q}uantified {R}eflection {C}alculus with one modality",
  year = "2020",
  booktitle = "Advances in Modal Logic 13",
  pages = "13--32",
  publisher = "College Publications",
  address = "Helsinki, Finland",
  url = "http://www.aiml.net/volumes/volume13/deAlmeidaBorges-Joosten.pdf",
  keywords = "Provability logic, strictly positive logics, quantified modal logic, arithmetic interpretations, feasible fragments, decidable logics, finite model property",
  abstract = "This paper presents the logic QRC1, 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 QRC1 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 QRC1 to be arithmetically complete. This paper takes the first steps towards arithmetical completeness by providing relational semantics for QRC1 with a corresponding completeness proof. We further show the finite model property with respect to domains and number of worlds, which implies decidability."
}