We define game semantics for the constructive $\mu$-calculus and prove its equivalence to bi-relational semantics. As an application, we use the game semantics to prove that the $\mu$-calculus collapses to modal logic over the modal logic $\mathsf{IS5}$. We then show the completeness of $\mathsf{IS5}$ extended with fixed-point operators.

翻译：我们为构造性μ-演算定义了游戏语义，并证明了其与双关系语义的等价性。作为应用，我们利用该游戏语义证明了μ-演算在模态逻辑𝖨𝖲𝟧上可归约为模态逻辑。随后，我们证明了带有不动点算子的𝖨𝖲𝟧扩展系统的完备性。