Non-Well-Founded Proofs for the Grzegorczyk Modal Logic

TL;DR

This paper introduces a sequent calculus for the Grzegorczyk modal logic that supports cyclic proofs and proves cut-elimination, enabling proof-theoretic analysis and interpolation results.

Contribution

It develops a novel non-well-founded proof system for Grz logic with a cut-elimination theorem and establishes Lyndon interpolation proof-theoretically.

Findings

Cut-elimination for cyclic proofs in Grz logic

Proof-theoretic Lyndon interpolation property established

Supports non-well-founded proof structures

Abstract

We present a sequent calculus for the Grzegorczyk modal logic Grz allowing cyclic and other non-well-founded proofs and obtain the cut-elimination theorem for it by constructing a continuous cut-elimination mapping acting on these proofs. As an application, we establish the Lyndon interpolation property for the logic Grz proof-theoretically.