A note on the incompleteness of Afshari & Leigh's system Clo
Johannes Kloibhofer · arXiv (Cornell University) · 2023
The system $\mathsf{Clo}$ is a cyclic, cut-free proof system for the modal $μ$-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 $μ$-calculus. We prove that $\mathsf{Clo}$ is incomplete by giving a valid sequent that is not provable in $\mathsf{Clo}$.