  Sentences containing definite descriptions, expressions of the form `The
$F$', can be formalised using a binary quantifier $\iota$ that forms a formula
out of two predicates, where $\iota x[F, G]$ is read as `The $F$ is $G$'. This
is an innovation over the usual formalisation of definite descriptions with a
term forming operator. The present paper compares the two approaches. After a
brief overview of the system $\mathbf{INF}^\iota$ of intuitionist negative free
logic extended by such a quantifier, which was presented in
\citep{kurbisiotaI}, $\mathbf{INF}^\iota$ is first compared to a system of
Tennant's and an axiomatic treatment of a term forming $\iota$ operator within
intuitionist negative free logic. Both systems are shown to be equivalent to
the subsystem of $\mathbf{INF}^\iota$ in which the $G$ of $\iota x[F, G]$ is
restricted to identity. $\mathbf{INF}^\iota$ is then compared to an
intuitionist version of a system of Lambert's which in addition to the term
forming operator has an operator for predicate abstraction for indicating scope
distinctions. The two systems will be shown to be equivalent through a
translation between their respective languages. Advantages of the present
approach over the alternatives are indicated in the discussion.

Logic in Computer Science;Logic