Cut-Elimination for the Bimodal Logic GR
Logic in Computer Science
2026-05-18 v1
Abstract
In this paper, we present a hypersequent calculus for bimodal logic GR, where the two modalities represent the arithmetic provability predicates of Goedel and Rosser, respectively. We prove the cut-elimination theorem for the calculus.
Keywords
Cite
@article{arxiv.2605.15732,
title = {Cut-Elimination for the Bimodal Logic GR},
author = {Hirohiko Kushida},
journal= {arXiv preprint arXiv:2605.15732},
year = {2026}
}