Natural deduction systems with indefinite and definite descriptions
(ε-terms and ℩-terms) are presented, and interpreted in
Martin-Löf's intensional type theory. The interpretations are
formalizations of ideas which are implicit in the literature of
constructive mathematics: if we have proved that an element with a
certain property exists, we speak of ‘the element such that the
property holds' and refer by that phrase to the element constructed
in the existence proof. In particular, we deviate from the practice
of interpreting descriptions by contextual definitions.