Has an equivalent of the set-theoretic hierarchies (arithmetical, hyperarithmetical, Levy etc.) that uses the uniqueness quantification, $\exists !$ (and its dual, $\neg\exists!\neg$) been studied somewhere? That is a hierarchy such that $\exists! x \, \phi(x)$ is $\widetilde\Sigma_{n+1}$ when $\phi$ is $\widetilde\Pi_n$ and $\neg\exists!x \, \neg\phi(x)$ is $\widetilde\Pi_{n+1}$ when $\phi$ is $\widetilde\Sigma_{n}$.
The uniqueness quantification would be defined as $\exists !x \varphi(x) := \exists x \varphi(x) \wedge \forall y (\varphi(y) \rightarrow y=x)$. So we can establish, for example in the Levy hierarchy, that $\widetilde\Sigma_{n} \subseteq \Delta_{n+1}$. From there we obtain that $\Delta_n \subseteq\widetilde\Sigma_{n+1} \subseteq \Delta_{n+2}$ and a few questions arise that are non-trivial to me: Are those inequalities strict? What is a predicate in $\Delta_{n+2} \backslash \widetilde\Sigma_{n+1}$? In $\widetilde\Sigma_{n+1}\backslash\Delta_{n}$? etc.
I'm interested in works with any such defined set-theoretic hierarchy or any results that show that this hierarchy is not so interesting, is somehow equivalent to the classical hierarchies etc. I'm also interested in such results in constructive models such as $L$, $L_{\omega_1}$, ….
