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

This paper introduces a G3-style sound and complete sequent calculus for the Russellian approach to definite description presented by Indrzejczak and some coauthors in previous works. We show that the calculi introduced have the good structural properties that are distinctive of G3-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.