Cut elimination for a non-wellfounded system for the master modality

TL;DR

This paper extends a cut elimination method to non-wellfounded proofs with trace conditions, enabling syntactic cut elimination for a modal logic system with the master modality using structural proof theory and corecursion.

Contribution

It introduces a novel approach to cut elimination for non-wellfounded proofs based on trace conditions, applicable to modal logic systems.

Findings

Successfully extended cut elimination to trace-based non-wellfounded proofs.

Provided a syntactic cut elimination method for the $K^+$ modal logic system.

Demonstrated the method's reliance on structural proof theory and corecursion.

Abstract

In previous work we provided a method for eliminating cuts in non-wellfounded proofs with a local-progress condition, these being the simplest kind of non-wellfounded proofs. The method consisted of splitting the proof into nicely behaved fragments. This paper extends our method to proofs based on simple trace conditions. The main idea is to split the system with the trace condition into infinitely many local-progress calculi that together are equivalent to the original trace-based system. This provides a cut elimination method using only basic tools of structural proof theory and corecursion, which is needed due to the non-wellfounded character of proofs. We will employ the method to obtain syntactic cut elimination for $K^+$, a system of modal logic with the master modality.