Cut-elimination for the mu-calculus with one variable

TL;DR

This paper proves a syntactic cut-elimination result for the one-variable fragment of the modal mu-calculus using a novel technique involving Buchholz's Omega-rule, advancing proof theory in modal logic.

Contribution

It introduces a new cut-elimination method for the one-variable mu-calculus fragment based on Mints' technique and Buchholz's Omega-rule.

Findings

Successful cut-elimination for the one-variable mu-calculus fragment

Development of a novel proof technique using Buchholz's Omega-rule

Enhanced understanding of proof transformations in modal mu-calculus

Abstract

We establish syntactic cut-elimination for the one-variable fragment of the modal mu-calculus. Our method is based on a recent cut-elimination technique by Mints that makes use of Buchholz' Omega-rule.