Interpolation Properties for the Bimodal Provability Logic $$\textbf{GR}$$
Haruka Kogure, Taishi Kurahashi · Studia Logica · 2025
Abstract We study interpolation properties for Shavrukov’s bimodal logic $$\textbf{GR}$$ GR of usual and Rosser provability predicates. For this purpose, we introduce a new sublogic $$\textbf{GR}^\circ $$ GR ∘ of $$\textbf{GR}$$ GR and its relational semantics. Based on our new semantics, we prove that $$\textbf{GR}^\circ $$ GR ∘ and $$\textbf{GR}$$ 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 $$ GR ∘ and $$\textbf{GR}$$ GR with respect to our new semantics.