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.

翻译：本文提出了双模态逻辑GR的超矢列演算，其中两个模态分别表示哥德尔和罗瑟的算术可证谓词。我们证明了该演算的切割消去定理。