Interpolation Properties for the Bimodal Provability Logic $$\textbf{GR}$$

Abstract We study interpolation properties for Shavrukov’s bimodal logic $$\textbf{GR}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>GR</mml:mi> </mml:math> of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic $$\textbf{GR}^\circ $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GR</mml:mi> <mml:mo>∘</mml:mo> </mml:msup> </mml:math> of $$\textbf{GR}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>GR</mml:mi> </mml:math> and its relational semantics. Based on our new semantics, we prove that $$\textbf{GR}^\circ $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GR</mml:mi> <mml:mo>∘</mml:mo> </mml:msup> </mml:math> and $$\textbf{GR}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>GR</mml:mi> </mml:math> 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 $$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:msup> <mml:mi>GR</mml:mi> <mml:mo>∘</mml:mo> </mml:msup> </mml:math> and $$\textbf{GR}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mi>GR</mml:mi> </mml:math> with respect to our new semantics.