Game semantics for the constructive $\mu$-calculus

TL;DR

This paper introduces game semantics for the constructive μ-calculus, demonstrating its equivalence to bi-relational semantics and applying it to show collapse to modal logic over IS5, with completeness results.

Contribution

It provides the first game semantics for the constructive μ-calculus and proves its equivalence to bi-relational semantics, advancing understanding of fixed-point logics.

Findings

Game semantics for the constructive μ-calculus established.

Equivalence between game semantics and bi-relational semantics proven.

Collapse of μ-calculus to modal logic over IS5 demonstrated.

Abstract

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.