The Constructive $\mu$-calculus: Game Semantics and Non-Wellfounded Proof Systems

TL;DR

This paper introduces a constructive variant of the modal $alculus$, establishing game semantics, proving soundness and completeness of a non-wellfounded proof system, and extending to other non-classical modal logics.

Contribution

It develops a game semantics and a non-wellfounded proof system for the constructive modal $alculus$, with extensions to other non-classical modal logics.

Findings

Game semantics equivalent to birelational Kripke semantics

Proof system is sound and complete

Framework adaptable to other non-classical modal logics

Abstract

We study a variant of the modal $\mu$-calculus based on the constructive modal logic $\mathsf{CK}$. We define game semantics for the constructive $\mu$-calculus and prove its equivalence to the birelational Kripke semantics. We then use the game semantics to prove the soundness and completeness of a fully-labeled non-wellfounded proof system for it. At last, we briefly describe how to adapt the game semantics and proof system to the $\mu$-calculus over other non-classical modal logics.