  This paper presents a way of formalising definite descriptions with a binary
quantifier $\iota$, where $\iota x[F, G]$ is read as `The $F$ is $G$'.
Introduction and elimination rules for $\iota$ in a system of intuitionist
negative free logic are formulated. Procedures for removing maximal formulas of
the form $\iota x[F, G]$ are given, and it is shown that deductions in the
system can be brought into normal form.
