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

This paper introduces a G3 G 3 -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 G3 G 3 -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.