Suppose we in an impredicative framework isolate the fixed point
from a $Gx$ obtained by $\Pi^1_1$-comprehension as equivalent to $\forall K((A(K,x)\to Kx)\to Kx)$, where $K$ only occurs positively in $A(K,x)$.
May we take $Gx\leftrightarrow A(G,x)$ to be a recursive definition of $Gx$ in terms of $A(G,x)$?
(1) If so, may that not conflict with the requirement that definitions should be conservative?
(2) If not, what else may/should we consider $Gx\leftrightarrow A(G,x)$ to be?