# Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs

## TL;DR

This paper introduces a sequent calculus for the modal Grzegorczyk logic that permits non-well-founded proofs and establishes a cut-elimination theorem through a continuous transformation of these proofs.

## Contribution

It develops a novel sequent calculus with non-well-founded proofs for Grz logic and proves cut-elimination using a continuous proof transformation.

## Key findings

- Cut-elimination theorem established for the calculus
- Continuous cut-elimination mapping constructed
- Non-well-founded proofs enabled for Grz logic

## Abstract

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