zbMATH — the first resource for mathematics

Cut elimination for the weak modal Grzegorczyk logic via non-well-founded proofs. (English) Zbl 07176948
Iemhoff, Rosalie (ed.) et al., Logic, language, information, and computation. 26th international workshop, WoLLIC 2019, Utrecht, The Netherlands, July 2–5, 2019. Proceedings. Berlin: Springer (ISBN 978-3-662-59532-9/pbk; 978-3-662-59533-6/ebook). Lecture Notes in Computer Science 11541, 569-583 (2019).
Summary: We present a sequent calculus for the weak Grzegorczyk logic $$\mathsf{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.
For the entire collection see [Zbl 1418.03008].
MSC:
 03B70 Logic in computer science
Full Text: