Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
classification
🧮 math.LO
keywords
cut-eliminationproofsgrzegorczyklogicmodalnon-well-foundedactingallowing
read the original 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.
This paper has not been read by Pith yet.
discussion (0)
Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.