  This paper presents rules of inference for a binary quantifier $I$ for the
formalisation of sentences containing definite descriptions within intuitionist
positive free logic. $I$ binds one variable and forms a formula from two
formulas. $Ix[F, G]$ means `The $F$ is $G$'. The system is shown to have
desirable proof-theoretic properties: it is proved that deductions in it can be
brought into normal form. The discussion is rounded up by comparisons between
the approach to the formalisation of definite descriptions recommended here and
the more usual approach that uses a term-forming operator $\iota$, where $\iota
xF$ means `the F'.

Logic in Computer Science;Logic