Towards a Coq formalization of a quantified modal logic

The Quantified Reflection Calculus with one modality, denoted by $\mathsf{QRC}_1$, is a strictly positive quantified modal logic inspired by the unimodal fragment of the Reflection Calculus. The quantified strictly positive language consists of a verum constant and relation symbols as atomic formulas, with the only available connectives being the conjunction, the diamond, and the universal quantifier. $\mathsf{QRC}_1$ statements are assertions of the form $\varphi \leadsto \psi$ where $\varphi$ and $\psi$ are in this strictly positive language. $\mathsf{QRC}_1$ was born out of the wish for a nice quantified provability logic for theories of arithmetic such as Peano Arithmetic, even though Vardanyan showed in 1986 that this is impossible in general. However, restricting the language to the strictly positive fragment is a viable solution, as shown by the author and Joosten in 2022. $\mathsf{QRC}_1$ has been proved sound and complete with respect to constant domain Kripke models. Furthermore, it has the finite model property with respect to both the domain size and the number of worlds, implying its decidability. Coq is an interactive theorem prover with which one can write definitions, executable algorithms, statements, and machine-checked proofs. We describe a Coq formalization of $\mathsf{QRC}_1$ and of some relevant results, most noticeably the Kripke soundness theorem. In the future, we aim to formalize the full completeness proof and extract a decision procedure in order to mechanically check whether a given implication of strictly positive formulas is provable in $\mathsf{QRC}_1$ or not.