Quantified Reflection Calculus with one modality

From MaRDI portal
Publication:6337696

arXiv2003.13651MaRDI QIDQ6337696FDOQ6337696


Authors: Ana de Almeida Borges, Joost J. Joosten Edit this on Wikidata


Publication date: 30 March 2020

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 also show the finite model property, which implies decidability.




Has companion code repository: https://gitlab.com/ana-borges/QRC1-Coq









This page was built for publication: Quantified Reflection Calculus with one modality

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6337696)