Cfrgtkky

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 xin A:Q(x)} forall xin 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?

To start, $exists xin 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 xin A.Q(x)$ is often viewed as an abbreviation of $exists x.xin Aland Q(x)$ as suggested by spaceisdarkgreen.¹ There is no need to require a predicate corresponding to $xin 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 xin 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 $xin 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} xin [![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 xin A.Q(x)$ should be the same as $negforall xin 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.