Call a set-theoretical formula $\phi(x,X)$ a **set-builder formula** (with parameter $X$) iff $\lbrace x\ |\ \phi(x,X) \rbrace$ is a set for every set $X$.

Call a set-builder formula $\phi(x,X)$ **invertible** iff there is a set-builder formula $\phi^{-1}(y,Y)$ such that

$$X = \lbrace y\ |\ \phi^{-1}(y,\lbrace x\ |\ \phi(x,X)\rbrace)\rbrace$$

for every set $X$.

**Example 1**:

$$\phi(\mathbf{x},\mathbf{X}) = \mathbf{x} \in \mathbf{X}$$

Note, that $X = \lbrace x \ |\ \phi(x,X) \rbrace$. Thus $\phi$ can be inverted by

$$\phi^{-1}(\mathbf{y},\mathbf{Y}) = \mathbf{y} \in \mathbf{Y}$$

**Example 2**:

$$\phi(\mathbf{x},\mathbf{X}) = (\exists z,z')\ \mathbf{x} = (z,z') \wedge z,z' \in \mathbf{X}$$

$Y := \lbrace x \ |\ \phi(x,X) \rbrace$ is the set $X \times X$ of ordered pairs over a given set $X$. $\phi$ can be inverted by

$$\phi^{-1}(\mathbf{y},\mathbf{Y}) = (\exists z,z')\ z =(\mathbf{y},z') \wedge z \in \mathbf{Y}$$

since $X = \lbrace y\ |\ \phi^{-1}(y,Y)\rbrace$ is the underlying set for a given set of ordered pairs $Y$.

**Example 3:**

$$\phi(\mathbf{x},\mathbf{X}) = (\forall z)\ z \in \mathbf{x} \rightarrow z \in \mathbf{X} $$

$Y := \lbrace x \ |\ \phi(x,X) \rbrace$ is the powerset $P(X)$ of a given set $X$. $\phi$ can be inverted by

$$\phi^{-1}(\mathbf{y},\mathbf{Y}) = (\exists z)\ \mathbf{y} \in z \wedge z \in \mathbf{Y}$$

since $X = \lbrace y\ |\ \phi^{-1}(y,Y)\rbrace$ is the underlying set for a given powerset $Y$.

**Counterexample:**

$$\phi(\mathbf{x},\mathbf{X}) = (\exists z,z')\ z =(\mathbf{x},z') \wedge z \in \mathbf{X}$$

For arbitrary sets of pairs $X = X_1 \times X_2$ the set $\lbrace x \ |\ \phi(x,X) \rbrace$ equals $X_1$, i.e. is the projection on the first component. Thus $\phi$ cannot be inverted.

**Questions**

Is the property of being invertible (semi-)decidable for set-builder formulas?

That means, is there a systematic way to tell whether an (invertible) set-builder formula is invertible?

Is a formula $\phi^{-1}$ computable for invertible set-builder formulas $\phi$?

That means, can a formula $\phi^{-1}$ be construed in a systematic way for a given invertible set-builder formula $\phi$?

To ask the first question more softly:

Are there (semi-)obvious necessary and/or sufficient conditions for a set-builder formula to be invertible?