What is the formal definition in first order logic of the informal statement $\exists x \in A : Qx$?

Question

tl;dr: Is the right translation of the informal statement $ \exists x \in A:Q(x)$ into formal FOL $\exists x (\varphi^A(x)\to Qx)$? Or $\lor_{x \in A} Qx$? Are they equivalent? Or perhaps something else?

---

My thoughts:

I was reading stuff about vacuous truths and noticed the bullet points:

1. $\forall x:P(x)\Rightarrow Q(x)$, where it is the case that ${\displaystyle \forall x:\neg P(x)} \forall x:\neg P(x)$.
2. ${\displaystyle \forall x\in A:Q(x)} \forall x\in A:Q(x)$, where the set {\displaystyle A} A is empty.
3. ${\displaystyle \forall \xi :Q(\xi )} \forall \xi :Q(\xi )$, where the symbol ${\displaystyle \xi } $ is restricted to a type that has no representatives.

from bullet point 2 I assume that statements of the form $\forall a \in A: Qx$ are translated to $\forall x (\varphi^A(x)\to Qx)$ where $\varphi^A$ is the L-formula that returns True for elements of $A$ (so we are assuming the set A is definable). These is the formal language of L-structures and FOL according to these notes. However I noticed that if we thought about this algorithmically we could also write the code for $\sigma_{\forall} = \forall x (\varphi^A(x)\to Qx)$ as follows:

def translation_of_informal_for_all_statement():
sigma_for_all = True //like this to make code elegant but I dont get it
for a in A:
    sigma_for_all = sigma_for_all && Qx
return sigma_for_all

this seems to return the right things for $\forall a \in A: Qx$ and seems identical to $\sigma_{\forall} = \forall x (\varphi^A(x)\to Qx)$ as far as I can tell (i.e. has the same truth table). Especially in the tricky edge case when the set $A$ is empty (which I'm not actually true why it should be true in that case except that if I do set it true it makes the code/algorithm more elegant and compact without weird edge case scenario conditionals in the code). Note the code just expresses the formula $\land_{x \in A} Qx$.

Thus, I wondered what would be the correct (sound, consistent?) translation for $\exists x \in A : Qx$. I thought it would be $\sigma_{\exists} = \exists x (\varphi^A(x)\to Qx)$ just from looking at how the forall statement was translated (just a guess). However it makes sense to me that the code for it should be easy to translate:

def translation_of_informal_exists_statement():
sigma_exists = False // like this because no element as of yet satisfies the existence statement
for a in A:
    sigma_exists = sigma_exists or Qx
return sigma_exists

The initialization to false does make sense to me. In that we have not found an element in the set $A$ that has property $Qx$ before we start the loop and if the loop is empty or we don't find $Qx$ then we know no element in $A$ has property $Qx$. That makes sense to me. Note that the code just implements $\lor_{x \in A} Qx$. However, what I am not sure is if the algorithm/pseudo-code I wrote is indeed equivalent to $\sigma_{\exists} = \exists x (\varphi^A(x)\to Qx)$ and if that is the right interpretation. Is it?

Answer 1

To start, $\exists x\in A.Q(x)$ is not a formula of FOL (unless you're viewing $A$ as a sort in which case I'd recommend against using $\in$). In particular, $\in$ is not part of the logical syntax of the framework of first-order logic. Instead, it is a binary predicate symbol in typical first-order theories of set theory.

Within the context of a suitable set theory, say ZFC, $\exists x\in A.Q(x)$ is often viewed as an abbreviation of $\exists x.x\in A\land Q(x)$ as suggested by spaceisdarkgreen.¹ There is no need to require a predicate corresponding to $x\in A$. On the other hand, using an $A$-indexed disjunction² isn't a valid FOL formula and just doesn't make sense. It mixes object-level and meta-leval notions. (There are infinitary logics which allow formulas roughly like this, but they tend to be poorly behaved and there is still a separation between object- and meta-level.)

Above, I was treating $A$ as a set (i.e. an individual) of the (set) theory. There are some other possibilities. Another possibility is that $A$ could be a class. In that case, $A$ is represented by some formula and $\exists x\in A.Q(x)$ would indeed mean $\exists x.\varphi^A(x)\land Q(x)$ where $\varphi^A$ is some formula that represents the class $A$. I, personally, don't like treating classes as set-like things and would rather talk only about representative formulas.

A third possibility, which I indicated in the first paragraph, is that $A$ is a sort. In that case, I'd prefer a notation like $\exists x\!:\!A.Q(x)$. There's typically no reason to do this unless you are working in a multi-sorted FOL. In this case, this is a primitive notion (or perhaps defined in terms of universal quantification over $A$), it is not an abbreviation for something else. In multi-sorted FOL, we simply have different quantifiers for each sort. Multi-sorted FOL won't have a predicate indicating "membership" in a sort, so there's nothing that corresponds to $x\in A$ or $\varphi^A$. (The [set-theoretic] semantics of multi-sorted FOL will assign a different "domain" set to each sort. In the semantics, $[\![\exists x:A.Q(x)]\!] = \boldsymbol{\exists} x\in [\![A]\!].[\![Q(x)]\!]$ where the brackets indicate the [overloaded] semantic mapping of sorts and formulas, and I use a slightly bolded $\boldsymbol{\exists}$ to distinguish between the object-level $\exists$ and the meta-level $\boldsymbol{\exists}$ in the semantics.)

As a final note, while you can (again) get some intuition by thinking about quantifiers as loops that check whether any/all "elements" satisfy the predicate in the body, there are a variety of ways where this view is inadequate. When you are not working in a set-theoretic context there may be no analogue to "elements", and even in a set-theoretic context it doesn't make sense to talk about "looping over" the elements of a set, e.g. the set of reals. You can, however, go the other way, and view certain loops as implementing some quantified formulas, but again this is a very special case that makes it harder to see the "essence" of quantification.

¹ Incidentally, you could derive this by using the definition of $\exists $ in terms of $\forall$, i.e. $\exists x\in A.Q(x)$ should be the same as $\neg\forall x\in A.\neg Q(x)$.

² While you can get some intuitions about $\forall$ and $\exists$ by viewing them (intuitively!) as (potentially infinite) conjunctions/disjunctions, I recommend care in doing so. While this intuition tends to be valid enough for classical logic, it doesn't generalize to non-classical logics. This means that there are aspects of the quantifiers that this intuition misses. It would be like considering quotients of groups but only considering commutative group examples; you lose the notion and significance of normality.