Abstract

We study interpolation properties for Shavrukov’s bimodal logic $$\textbf{GR}$$ of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic $$\textbf{GR}^\circ$$ of $$\textbf{GR}$$ and its relational semantics. Based on our new semantics, we prove that $$\textbf{GR}^\circ$$ and $$\textbf{GR}$$ enjoy Lyndon interpolation property and uniform interpolation property. As a consequence of our proofs, we obtain the completeness and the finite frame property of $$\textbf{GR}^\circ$$ and $$\textbf{GR}$$ with respect to our new semantics.