Cut-elimination for the alternation-free modal mu-calculus

TL;DR

A syntactic cut-elimination procedure for the alternation-free fragment of the modal mu-calculus is presented, which is exploited to directly transform a cyclic proof with cuts into a cut-free one, without detouring through other logics or relying on intermediate machinery for regularisation.

Abstract

We present a syntactic cut-elimination procedure for the alternation-free fragment of the modal mu-calculus. Cut reduction is carried out within a cyclic proof system, where proofs are finitely branching but may be non-wellfounded. The structure of such proofs is exploited to directly transform a cyclic proof with cuts into a cut-free one, without detouring through other logics or relying on intermediate machinery for regularisation. Novel ingredients include the use of multicuts and results from the theory of well-quasi-orders, the later used in the termination argument.

Figures (1)

• Figure 1: Proof rules of the $\mathsf{Focus}$ system

Theorems & Definitions (65)

• Definition 1
• Definition 2
• Proposition 3
• proof
• Proposition 4
• Lemma 5: Dickson's Lemma
• proof
• Definition 6
• Definition 7
• Lemma 8