Towards a Coq formalization of a quantified modal logic

Abstract

We present a Coq formalization of the Quantified Reflection Calculus with one modality, or QRC1. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The highlights are a deep embedding of QRC1 in the Coq proof assistant, a mechanization of the notion of Kripke model with varying domains and a formalization of the soundness theorem. We focus on the design decisions inherent to the formalization and the insights that led to new and simplified proofs.

Keywords

Modal logic, strictly positive logic, Kripke semantics, feasible fragments, formalization, Coq

Citation

de Almeida Borges, A. (2022). Benzmüller, C. & Otten, J. (Eds.). Towards a Coq formalization of a quantified modal logic. Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022) (pp. 13–27). CEUR. URL: https://ceur-ws.org/Vol-3326/ARQNL2022_paper1.pdf

@InProceedings{AlmeidaBorges2022_QRC1Coq,
  author = "{de Almeida Borges}, Ana",
  editor = "Benzmüller, Christoph and Otten, Jens",
  title = "Towards a {C}oq formalization of a quantified modal logic",
  booktitle = "Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics ({ARQNL} 2022)",
  year = "2022",
  pages = "13--27",
  publisher = "CEUR",
  address = "Haifa, Israel",
  url = "https://ceur-ws.org/Vol-3326/ARQNL2022\_paper1.pdf",
  keywords = "Modal logic, strictly positive logic, Kripke semantics, feasible fragments, formalization, Coq",
  abstract = "We present a Coq formalization of the Quantified Reflection Calculus with one modality, or QRC1. This is a decidable, strictly positive, and quantified modal logic previously studied for its applications in proof theory. The highlights are a deep embedding of QRC1 in the Coq proof assistant, a mechanization of the notion of Kripke model with varying domains and a formalization of the soundness theorem. We focus on the design decisions inherent to the formalization and the insights that led to new and simplified proofs."
}