Modal logic can be traced back to Lewis’ introduction of a modal connective for ‘strict implication’, also known as the Lewis arrow. Classically, the Lewis arrow is inter-definable with box, and so the connective has fallen into disuse over time. Over an intuitionistic base, however, the arrow is more expressive than the box.

With the aim of setting up a general framework for intuitionistic fixed point modal logics, we study an intuitionistic version of the mu-calculus with the Lewis arrow as modal connective. Formulas are interpreted over bi-relational Kripke models, which satisfy a confluence condition to ensure monotonicity with respect to the intuitionistic order.

In this talk, I will introduce both algebraic and game semantics for the logic, and provide a complete non-wellfounded proof system for guarded formulas. Moreover, I will show how Ruitenburg’s theorem can be used to prove that every formula is equivalent to a guarded one, thereby showing that this well-known result for the classical mu-calculus still holds in the intuitionistic case.

This is joint work with Bahareh Afshari.