Interpolation properties for the bimodal provability logic $\mathbf{G}\mathbf{R}$

We study interpolation properties for Shavrukov’s bimodal logic $\mathbf{G}\mathbf{R}$ of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic ${\mathbf{G}\mathbf{R}}^{\circ }$ of $\mathbf{G}\mathbf{R}$ and its relational semantics. Based on our new semantics, we prove that ${\mathbf{G}\mathbf{R}}^{\circ }$ and $\mathbf{G}\mathbf{R}$ enjoy Lyndon interpolation property and uniform interpolation property.