We define game semantics for the constructive $\mu$-calculus and prove its correctness. We use these game semantics to prove that the $\mu$-calculus collapses to modal logic over $\mathsf{CS5}$ frames. Finally, we prove the completeness of $\mathsf{\mu CS5}$ over $\mathsf{CS5}$ frames.

翻译：我们为构造性μ-演算定义了游戏语义并证明其正确性。利用这些游戏语义，我们证明了在$\mathsf{CS5}$框架上μ-演算可坍缩为模态逻辑。最后，我们证明了$\mathsf{\mu CS5}$在$\mathsf{CS5}$框架上的完全性。