Invertible set-theoretical formulas

Question

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?

Answer 1

There is no algorithm for this.

The first thing to say, however, is that there is a metamathematical problem with your question. Your question makes reference to the truth of formulas of arbitrary complexity, and we have no way of formalizing this in mathematics, because of Tarski's theorem on the non-definability of truth. In this sense, the question is not really sensible. It is not meaningful to ask about algorithms ranging over all formulas, if part of the criteria of the problem to be solved has to do with the truth of those formulas. You could fix this issue by asking about formulas of restricted complexity, or by asking for provability in a formal system rather than truth, for the inversion criterion.

Meanwhile, one can make examples of formulas such that the question of whether they are invertible or not is independent of ZFC. For example, consider a formula $\phi(x,X)$ that splits into cases depending on the fact of the matter for some undecidable question, and then acts like one formula if that fact is true, and like another if the fact is false. For instance, let $\phi(x,X)$ be the formula that asserts: if the CH holds, then $x\in X$, and if it doesn't hold, then $x$ is the first element of an ordered pair in $X$. This formula is like your first example and hence invertible, if CH holds, and it is like your counterexample and hence not invertible, if CH fails. Thus, the question of whether it is invertible or not is independent of ZFC.

Similarly, one can make examples using a parameter and the halting problem to violate the decidibility question, if one asks about restricting the complexity of the formulas. For example, let $\phi_n(x,X)$ be the formula that asserts: if the $n^{th}$ program halts, then $x\in X$, and if it doesn't halt, then $x$ is the first element of an ordered pair in $X$. These assertions have bounded complexity, and so they avoid the objection of Tarski's theorem. But in order to decide if this formula is invertible in your sense, we have to be able to determine whether the $n^{th}$ program halts. Since the halting problem is not decidable, there is no algorithm for deciding whether or not a given formula (of this complexity) is invertible.

Answer 2

Let me offer an affirmative answer based on a different reading of the question than Joel’s. Since there is no truth predicate for all formulas in ZFC, I would interpret the definitions metamathematically so that a formula is a set-builder formula if ZFC proves that for every $X$, $\{x:\phi(x,X)\}$ is a set, and similarly for invertibility.

Then the properties of being a set-builder formula and of being invertible are both recursively enumerable (since provability in ZFC is). They are not decidable: for example, if $\phi$ is a sentence, then $\phi$ is a set builder iff it is refutable in ZFC. Similarly, if $\phi_0$ and $\phi_1$ are fixed set-builder formulas such that one is invertible and the other one is not (provably), then for a sentence $\phi$, the set-builder formula $(\phi\land\phi_0)\lor(\neg\phi\land\phi_1)$ is invertible iff $\phi$ is provable. Nevertheless, given an invertible formula $\phi$, there is an algorithm to find a $\phi^{-1}$: namely, search all possible strings until you find one which is a ZFC proof that a formula $\psi$ is an inverse of $\phi$, and then output $\psi$ as $\phi^{-1}$.