A Binary Quantifier for Definite Descriptions for Cut Free Free Logics

This paper presents rules in sequent calculus for a binary quantifier $I$ to formalise definite descriptions: $Ix[F, G]$ means `The $F$ is $G$'. The rules are suitable to be added to a system of positive free logic. The paper extends the proof of a cut elimination theorem for this system by Indrzejczak by proving the cases for the rules of $I$. There are also brief comparisons of the present approach to the more common one that formalises definite descriptions with a term forming operator. In the final section rules for $I$ for negative free and classical logic are also mentioned.