We define game semantics for the constructive $\mu$-calculus and prove its equivalence to bi-relational semantics. We use the game semantics to prove that the $\mu$-calculus collapses to modal logic over constructive variants of $\mathsf{S5}$. Finally, we use the collapse to prove the completeness of constructive variants of $\mathsf{S5}$ with fixed-point operators.

翻译：我们为构造性 μ-演算定义了游戏语义，并证明其与双关系语义的等价性。利用该游戏语义，我们证明了在构造性 S5 变体上 μ-演算退化为模态逻辑。最后，我们利用这一退化结果证明了带不动点算子的构造性 S5 变体的完备性。