G3-Style Sequent Calculi and Craig Interpolation Property for Logics with Russellian Definite Descriptions

Abstract This paper introduces a $$\textsf{G3}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>G</mml:mi> <mml:mn>3</mml:mn> </mml:mrow> </mml:math> -style sound and complete sequent calculus for the Russellian approach to definite description presented by Indrzejczak and some co-authors in previous works. We show that the calculi introduced have the good structural properties that are distinctive of $$\textsf{G3}$$ <mml:math xmlns:mml="http://www.w3.org/1998/Math/MathML"> <mml:mrow> <mml:mi>G</mml:mi> <mml:mn>3</mml:mn> </mml:mrow> </mml:math> -style calculi: weakening and contraction are height-preserving admissible, all rules are height-preserving invertible, and cut is admissible. Having all rules invertible, the calculus allows to extract a countermodel from a failed proof search. Moreover, we use the calculus to give a Maehara-style constructive proof of Craig Interpolation Property. Finally, we extend the approach to intuitionistic logic.