A Natural Deduction style proof system for propositional $\mu$-calculus and its formalization in inductive type theories

TL;DR

This paper formalizes Kozen's propositional modal μ-calculus within the Calculus of Inductive Constructions, addressing key issues in encoding modal proof rules and enabling computer-aided proof development in Coq.

Contribution

It introduces a formal proof system for propositional μ-calculus in Coq, handling complex encoding challenges and facilitating error-free proof development.

Findings

Successful formalization of μ-calculus in Coq

Resolution of encoding issues with higher-order syntax

Provides a portable approach for similar proof systems

Abstract

In this paper, we present a formalization of Kozen's propositional modal $\mu$-calculus, in the Calculus of Inductive Constructions. We address several problematic issues, such as the use of higher-order abstract syntax in inductive sets in presence of recursive constructors, the encoding of modal (``proof'') rules and of context sensitive grammars. The encoding can be used in the \Coq system, providing an experimental computer-aided proof environment for the interactive development of error-free proofs in the $\mu$-calculus. The techniques we adopted can be readily ported to other languages and proof systems featuring similar problematic issues.