QRC₁ in Coq

This library defines the language, calculus and Kripke semantics of QRC₁. It further proves its Kripke soundness and completeness, as well as its decidability.

Related publications

• Quantified Reflection Calculus with one modality

• An Escape from Vardanyan’s Theorem

• Towards a Coq formalization of a quantified modal logic

• Suitable logics: provability, temporal laws, and formalization (Chapter 10)