$\iota x.\phi(x)$ means 'The unique $x$ that satisfies $\phi$', and is usually defined contextually/implicitly by replacing $\psi(\iota x.\phi(x))$ with $\exists!.x\phi(x)\wedge\psi(x)$. I wonder whether there is a way to import $\iota x.\phi(x)$ into the object language as a term and to define its semantics. I know this is different from ordinary math logic because the construction of terms now involves formulas and the denotational semantics of terms now seems to be intertwined with formulas'.
Thanks in advance.
This notion and generalizations is fairly deeply studied by Paul Taylor in the context of Abstract Stone Duality, particularly the notion of sobriety. In these papers, Paul Taylor solves the "problem" you bring up in the opposite way. He defines formulas as $\Sigma$-valued terms where $\Sigma$ is the Sierpiński space, the open set classifier, which means each formula, in this sense, picks out an open subset of its domain. Corresponding to equality of arrows in a category, the only actual formulas he uses are equalities of terms. Since $\mathbb{N}$ is discrete (with the usual topology), $=\ \!\!\! : \mathbb{N}\times\mathbb{N}\to\Sigma$ is a continuous function (i.e. the diagonal is an open subset of $\mathbb{N}\times\mathbb{N}$) and so definite description for discrete types is not problematic. For $\mathbb{R}$ with the standard topology, the diagonal is not open. Instead he defines a $\mathtt{cut}$ operation which takes two formulas ($\Sigma$-valued terms) satisfying properties that make the pair specify a Dedekind cut and produces a real number. The pattern of both of these constructs can be captured with the notion of (abstract) sobriety in an operation he calls $\mathtt{force}$ which generalizes definite description and $\mathtt{cut}$.
Moving back from the specific problem of definite description and abstract Stone duality, identifying formulas with certain terms is probably the technically simplest way to formulate your logical system. It is, however, certainly not the most minimal way (i.e. the way that requires the least structure for your semantics). It's actually a bit subtle to articulate why things are a bit complex in this case. Having terms depend on formulas isn't, by itself, too much of an issue. The axiom schema of separation does this without much issue. A denotational semantics for it would be an interpretation of formulas into subobjects and then a function from (at least the expressible subset of) subobjects to values in the semantic domain for terms. In this case though, for $\iota x.\varphi(x)$ to be well-formed requires some propositions to hold. For example, let's say $\varphi(x)$ uniquely characterizes $x$ if it exists, then given $\varphi(x)$ we can establish, say, $\psi(\iota x.\varphi(x))$, i.e. $x:X;\varphi(x)\vdash\psi(\iota x.\varphi(x))$ is a well-formed formula-in-context. The issue comes when we want to write $x:X;\varphi(x),\psi(\iota x.\varphi(x)) \vdash \chi(x)$. We can no longer treat the assumptions independently. Note, this is not because $\psi(\iota x.\varphi(x))$ contains $\varphi$ as a subformula, but because the well-formedness of $\iota x.\varphi(x)$ depends on the assumption of $\varphi(x)$. At any rate, the problems are essentially a simplified form of the exact same problems dependent type theories face. Instead of a sequence or conjunction of assumptions being the context, you need a telescope, i.e. a sequence where each entry (potentially) depends on all previous entries. To underscore this, writing the above formula-in-context with (irrelevant) proof terms would look something like: $$x:X;p:\varphi(x),q:\psi(\iota(p, x.\varphi(x)))\vdash \_:\chi(x)$$
The upshot is if you want to go this route, looking at the semantics of dependent type theory should provide you the tools you'd need. In fact, they'll be a bit over-powered, but you can simplify them to the proof-irrelevant case. For categorical semantics, this nlab page is an okay overview. Bart Jacobs' thesis and book are a bit technical but fairly authoritative.