  So far we have been speaking informally, but there are two equivalent ways of developing definite descriptions ideas formally. The approach introduced by Bertrand Russell (Russell 1905, Whitehead and Russell 1925) is widely familiar and probably needs little explication here. Suffice it to say, it extends to the intensional setting without difficulty. In this approach, a term-like expression, \(\atoi y\phi (y)\),  is introduced, where \(\phi (y)\) is a formula and \(y\) is an object variable. It is read, “the \(y\) such that \(\phi (y)\).” This expression is given no independent meaning, but there is a device to translate it away in an appropriate context. Thus,  \([\lambda x\,\psi (x)] \atoi y\phi (y))\)  is taken to abbreviate the formula \(\exists y[\forall z(\phi (z) \equiv z = y)  \wedge \psi (y)]\).   (The standard device has been used of writing \(\phi (z)\) to represent the substitution instance of \(\phi (y)\) resulting from replacing free occurrences of \(y\) with occurrences of \(z\), and modifying bound variables if necessary to avoid incidental capture of \(z\).) The present abstraction notation, using \(\lambda\), is not that of Russell, but he used an equivalent scoping device. As he famously pointed out, Russell’s method allows us to distinguish between “The present King of France is not bald,” which is false because there is no present King of France, and “It is not the case that the present King of France is bald,” which is true because “The present King of France is bald” is false. It becomes the distinction between  \([\lambda x\,\neg\textit{Bald}(x)](\atoi y\textit{King}(y))\)  and  \(\neg [\lambda x\textit{Bald}(x)](\atoi y\textit{King}(y))\).