LOMay 15
Cut-Elimination for the Bimodal Logic GR
arXiv:2605.1573257.0
AI Analysis
This work provides a proof-theoretic foundation for a logic that combines two important provability predicates, but the result is incremental as it extends existing techniques to a specific bimodal setting.
The paper presents a hypersequent calculus for the bimodal logic GR, which captures the arithmetic provability predicates of Goedel and Rosser, and proves the cut-elimination theorem for this calculus.
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.