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

Abstract

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

22 pages