In the context of type free set theories with set abstracts, as e.g. investigated by Andrea Cantini, Logical Frameworks for Truth and Abstraction, Elsevier 1996, one has the following construction (Cantini, p. 76):
For any formula $\alpha(x,y)$ with the free variables shown, there is a set $\textbf{v}$ such that $\forall x(x\in \textbf{v}\leftrightarrow \alpha(x,\textbf{v}))$.
Proof:
Let $$D^A=\{(x,f)|\alpha(x,\{u|(u,f)\in f\})\}$$
and $$\textbf{v}=\{x|(x,D^A)\in D^A\}$$
By spelling out:
$$x\in\textbf{v}\leftrightarrow (x,D^A)\in D^A\leftrightarrow\alpha(x,\textbf{v})$$
(Cantini credits Albert Visser with the definition of $\textbf{v}$, "though in semantical context ($\in$ replaced by a satisfaction predicate)", in Semantics and the Liar Paradox, in D. Gabbay and F. Guenthner (eds.), Handbook of Philosophical Logic IV (Reidel, Dordrecht), 1989, 695-696.)
Question:
Is this construction reminiscent of transfinite recursion, some other fixed point construction, or sui generis?
