  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.
