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

2023/07/13 by Kloibhofer, Johannes · 1 citation
#FOS: Mathematics #Logic (math.LO)

paper · doi:10.48550/arxiv.2307.06846

Abstract

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

Cited by

• Unravelling Cyclic First-Order Arithmetic

Related

• Completeness of Kozen's Axiomatization for the Modal mu-Calculus: A Simple Proof
• On the cut-elimination of the modal μ-calculus: Linear Logic to the rescue
• Demystifying μ
• Focus-style proof systems and interpolation for the alternation-free μ-calculus
• Cut-elimination for the alternation-free modal mu-calculus