Game semantics for the constructive $\hat{I}¼$-calculus

Abstract

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