Cut-Elimination for the Bimodal Logic GR

TL;DR

This paper introduces a hypersequent calculus for bimodal logic GR, modeling arithmetic provability, and proves the cut-elimination theorem for this calculus.

Contribution

It provides a new hypersequent calculus framework for bimodal logic GR with a proven cut-elimination theorem, advancing proof theory for provability logic.

Findings

Established a hypersequent calculus for bimodal logic GR

Proved the cut-elimination theorem within this calculus

Enhanced proof-theoretic understanding of provability modalities

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.