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

2018/04/03 by Yury Savateev, Savateev, Yury, Daniyar Shamkanov +1 · 2 citations
Computer Science · #Advanced Algebra and Logic #FOS: Mathematics #Logic (math.LO) #Logic, Reasoning, and Knowledge #Logic, programming, and type systems

paper · pdf · doi:10.48550/arxiv.1804.01432

openalex publication_date 2018/04/03 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28

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.

Cited by

• Coalgebraic proof translations for non-wellfounded proofs
• Cut elimination for a non-wellfounded system for the master modality

Related

• Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
• Non-Well-Founded Proofs for the Grzegorczyk Modal Logic
• Cut elimination for a non-wellfounded system for the master modality
• Cut-restriction: from cuts to analytic cuts
• Cut-elimination for the alternation-free modal mu-calculus