  As an attractive alternative, one could make definite descriptions into first-class things. Enlarge the language so that if \(\phi (y)\) is a formula where \(y\) is an object variable, then  \(\atoi y\phi (y)\)  is an intension term whose free variables are those of \(\phi (y)\) except for \(y\). Then modify the definition of formula, to allow these new intension terms to appear in places we previously allowed intension variables to appear. That leads to a complication, since intension terms involve formulas, and formulas can contain intension terms. In fact, formula and term must be defined simultaneously, but this is no real problem.