Suppose we in an impredicative framework isolate the fixed point

$$Gx\leftrightarrow A(G,x)$$

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?

`\\\\(\\\\)`

works, but`\(\)`

and even`\\(\\)`

don't, for technical reasons. (Just for fun, for`\[\]`

it's`\\[\\]`

, not`\\\\[\\\\]`

.) $\endgroup$