First-Order Logic into Set Theory?

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?

• The first thing it occurs to me that you might be asking is whether every consistent theory has a model in which the extensions of each of the predicates is set-theoretically definable. Is this in the neighborhood of what you mean? – Malice Vidrine Aug 26 '16 at 17:10
• @MaliceVidrine I am afraid that I have not fully understood what you meant. Still, it seems like your paraphrase of my question is slightly off, because I assumed above that a predicate is nothing more than the set, which is its extension, for the sake of brevity. My question has more to do with whether a set-theoretic "translation" of a FOL wff can be made while preserving the truth-value. – Leca Aug 26 '16 at 18:12
• @MaliceVidrine Thank you so much for your kind attention, and it seems that the problem lies in my question that is far from being lucid. – Leca Aug 26 '16 at 18:24
• Can you precisely define what you mean by a "set-theoretic formula"? – Eric Wofsey Aug 26 '16 at 18:40
• @EricWofsey Thank you for your comment. If I have not missed anything, what I think of is a formula that solely consists of set symbols (including the emptyset), various set-theoretic operators (e.g. $\subseteq, \cap$) except those which take an element as its operand (e.g. $\in$), and Boolean operators. – Leca Aug 26 '16 at 18:52

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.

• Thank you four your illuminating answer. – Leca Aug 27 '16 at 6:44
• @Leca: You're welcome two! – user21820 Aug 27 '16 at 6:45