Cut Elimination for Weak Modal Grzegorczyk Logic via Non-Well-Founded Proofs

TL;DR

This paper introduces a sequent calculus for the weak Grzegorczyk logic that incorporates non-well-founded proofs and proves cut-elimination through a continuous transformation, advancing proof theory techniques.

Contribution

It develops a novel sequent calculus with non-well-founded proofs for weak Grzegorczyk logic and establishes cut-elimination via a continuous mapping.

Findings

Cut-elimination theorem established for the calculus

Continuous cut-elimination mapping constructed

Proofs include non-well-founded structures

Abstract

We present a sequent calculus for the weak Grzegorczyk logic Go allowing non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs.