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

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?

• It is $\exists x(\phi^A(x)\land Q(x))$, not $\to.$ The sentence $\lor_{x\in A}Q(x)$ is correct semantically, the usual FOL does not have indexed disjunctions like this. Commented Nov 17, 2018 at 4:23
• speaking of which, recall our exchange here math.stackexchange.com/questions/2992901/… Commented Nov 17, 2018 at 4:34
• See Restricted quantifier : $\exists x (x \in A \land Qx)$. Commented Nov 17, 2018 at 9:28
• If we stay at the "standard" version of FOL, we have no $\in$ symbol; thus we have to use a predicaet $A(x)$ and thus : $\exists x (A(x) \land Q(x))$. Commented Nov 17, 2018 at 9:38
• @spaceisdarkgreen I didn't realize it was the same as that exchange we had! Thats really useful thanks for that :) . I think then what still seems unclear to me is the dissymmetry of how we interpret $\forall x \in A: Qx$ formally with an implication but $\exists x \in A: Qx$ with a conjunction. I feel if I understand that then things should make a lot more sense to me. The dissymmetry is what confuses me. Commented Nov 17, 2018 at 18:02

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.1 There is no need to require a predicate corresponding to $$x\in A$$. On the other hand, using an $$A$$-indexed disjunction2 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.

1 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)$$.

2 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.

• note I never said $x \in A$ was a formal FOL L-sentence/L-formula/L-term. It's not. I instead defined it via a definable set though for some reason you don't like that but thats the only way I know how to do this. Thanks for the help! Commented Nov 17, 2018 at 20:01
• $x\in A$ is a formal formula in (typical) first-order theories of sets. It's $\exists x\in A.Q(x)$ that I was saying wasn't a formula of FOL itself, though you could easily make a slight extension of FOL to make it formal given a binary predicate symbol $\in$. It's not clear from your question what kind of thing you want $A$ to be. If you want $A$ to be a subset of some semantic domain, then that corresponds to the class case and using definable "sets". In this case, it really wouldn't make sense to have a formal notation $\exists x\in A.Q(x)$, though it's fine informally as you describe. Commented Nov 17, 2018 at 20:38
• I don't know first-order theories of sets. Thats why I said $\exists x \in A: Qx$ was informal. What I had in mind as "formal" was FOL as described in these notes: faculty.math.illinois.edu/~vddries/main.pdf. So for me $x \in A$ is short hand for "definable sets" i.e. set of elements that have $\mathcal A \models \varphi^A(x)$ in some L-structure $\mathcal A = (A;L)$. Commented Nov 17, 2018 at 20:41