A note on the incompleteness of Afshari & Leigh's system Clo

TL;DR

This paper demonstrates that the proof system Clo for the modal μ-calculus is incomplete by providing a valid sequent that it cannot prove, challenging its proposed completeness.

Contribution

It reveals the incompleteness of Afshari & Leigh's system Clo, showing it cannot prove all valid sequents in the modal μ-calculus.

Findings

Clo is incomplete for the modal μ-calculus

A specific valid sequent is not provable in Clo

Challenges the claimed completeness of Clo

Abstract

The system $\mathsf{Clo}$ is a cyclic, cut-free proof system for the modal $\mu$-calculus. It was introduced by Afshari & Leigh as an intermediate system in their intent to show the completeness of Kozen's axiomatisation for the modal $\mu$-calculus. We prove that $\mathsf{Clo}$ is incomplete by giving a valid sequent that is not provable in $\mathsf{Clo}$.