First-Order Logic into Set Theory?

Question

It may sound silly, but I just came to wonder whether you can "translate" all well-formed formulas in FOL (without individual constants such as $a,b,\ldots$) into equivalent formulas in set theory (plus Boolean operators) given a first-order model.

NOT the other way around, which is to reduce set-theory into first-order logic.

For example, it seems like the following equivalences trivially hold (I will assume that first-order predicates are no more than sets):

$$\exists x \, Fx \text{ iff }\neg(F = \emptyset)$$ $$\exists x (Px \wedge \exists y (Rxy)) \text{ iff } \neg(P= \emptyset)\wedge \neg\{(P \cap X)=\emptyset\}\wedge \neg (Y=\emptyset) \text{ where }R=X\times Y$$

Can every well-formed formula be translated into an equivalent set-theoretic formula in a similar vein? Or to put it another way, can logic formulas with first-order quantifiers ($\exists, \forall$) be suitably translated into set-theoretic formulas without first-order quantifiers?

If that is the case, will extending the first-order logic (e.g. into infinitary logic) compromise such set-theoretic translatablity?

Answer 1

Step 1

Take any first-order structure $M$ over any language $L$.

Then $M$ already interprets formulae over $L$, and we can use the interpretation. For example:

$\forall x,y\ \exists z\ ( z \ne x \land P(x,f(y,z)))$

simply becomes:

$\forall x,y \in D\ \exists z \in D\ ( z \ne x \land P_M(x,f_M(y,z)))$

where $D$ is the domain of $M$ and $P_M,f_M$ are the interpretations of $P,f$ in $M$.

It is trivial to translate the function application and ordered pairs to pure ZFC, but I won't do it since it is not worth the trouble.

Step 2

Now it seems you also want to get rid of even quantifiers.

Take any $1$-parameter sentence $φ$ over ZFC.

Then: $ \def\none{\varnothing} $

$\forall x \in D\ ( φ(x) )$ iff $\{ x : x \in D \land φ(x) \} = D$.

$\exists x \in D\ ( φ(x) )$ iff $\{ x : x \in D \land φ(x) \} \ne \none$.

Thus you can recursively get rid of quantifiers, if you allow the use of set constructors, which pure ZFC does not have.

Notes

If you forbid set constructors, then "$\forall x,y \in D\ ( R_M(x,y) \to R_M(y,x) )$" cannot be translated to a sentence without quantifiers, because any translation must assert that $R$ is symmetric, and there is no way to do that without quantifiers. Notice that set equality itself has a quantifier hiding inside, which is crucial in allowing equality between constructed sets to capture quantified assertions.