1
$\begingroup$

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?

$\endgroup$
  • $\begingroup$ 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? $\endgroup$ – Malice Vidrine Aug 26 '16 at 17:10
  • $\begingroup$ @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. $\endgroup$ – Leca Aug 26 '16 at 18:12
  • $\begingroup$ @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. $\endgroup$ – Leca Aug 26 '16 at 18:24
  • $\begingroup$ Can you precisely define what you mean by a "set-theoretic formula"? $\endgroup$ – Eric Wofsey Aug 26 '16 at 18:40
  • $\begingroup$ @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. $\endgroup$ – Leca Aug 26 '16 at 18:52
0
$\begingroup$

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.

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

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.