English

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

Logic 2023-07-14 v1

Abstract

The system Clo\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 Clo\mathsf{Clo} is incomplete by giving a valid sequent that is not provable in Clo\mathsf{Clo}.

Keywords

Cite

@article{arxiv.2307.06846,
  title  = {A note on the incompleteness of Afshari & Leigh's system Clo},
  author = {Johannes Kloibhofer},
  journal= {arXiv preprint arXiv:2307.06846},
  year   = {2023}
}