Quantified Reflection Calculus with one modality

TL;DR

This paper introduces the logic QRC$_1$, a positive fragment of quantified modal logic interpreting the diamond modality as theory consistency, and establishes its arithmetical soundness, relational semantics, and decidability.

Contribution

It provides the first relational semantics and completeness proof for QRC$_1$, a new fragment of quantified modal logic, and demonstrates its finite model property.

Findings

QRC$_1$ is arithmetically sound.

QRC$_1$ has relational semantics and is complete.

QRC$_1$ is decidable due to the finite model property.

Abstract

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 first steps towards arithmetical completeness by providing relational semantics for QRC$_1$ with a corresponding completeness proof. We also show the finite model property, which implies decidability.