Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs
Logic
2017-04-12 v1
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.
Cite
@article{arxiv.1704.03258,
title = {Cut-elimination for the modal Grzegorczyk logic via non-well-founded proofs},
author = {Yury Savateev and Daniyar Shamkanov},
journal= {arXiv preprint arXiv:1704.03258},
year = {2017}
}
Comments
WOLLIC'17, 12 pages, 1 appendix