# What is the symmetry between the definitions of the bounded universal/existential quantifiers?

What is the symmetry between the definitions of the bounded universal/existential quantifiers?

$\forall x \in A, B(x)$ means $\forall x (x \in A \rightarrow B(x))$

$\exists x \in A, B(x)$ means $\exists x (x \in A \land B(x))$

These make intuitive sense, but I would expect there to be some kind of symmetry between how the definitions of the bounded quantifiers work, and I can't see one. $A \rightarrow B$ means $\lnot A \lor B$ which doesn't seem to have a direct relationship with $A \land B$. What am I missing?

-
I am not sure what you mean by symmetry, but the existencial and universal quantifiers are respectively, the left and right adjoints of the inverse image functor. – G. Rodrigues May 23 '11 at 17:29
It has been quite some time since you have asked the question, is there anything missing from the answers? If so, please update the question accordingly; otherwise please accept one of the answers. – Asaf Karagila Jul 13 '11 at 9:41
I haven't been able to clarify this for myself. I will review the answers and see if I can understand what I still don't get tomorrow. – John Salvatier Jul 15 '11 at 16:14

Consider $\forall x\in A, B(x)$. That is if $x$ is a member of $A$ then $B(x)$ is true.

This translates, as you well put to $\forall x(x\in A\rightarrow B(x))$, which again translates to $\forall x(x\notin A\lor B(x))$.

Denote $B=\{x\mid B(x)\}$, that is all the elements which satisfy $B(x)$. Now you have that $x\in B \iff B(x)$ is true.

We re-evaluate the previous sentence: $\forall x(x\in A\rightarrow x\in B)$, that is to say $A\subseteq B$, or to say $\forall x(x\notin A\lor x\in B)$.

Now consider the existential version: $\exists x(x\in A\land B(x))$ that is $\exists x(x\in A\land x\in B)$, or in simpler words $A\cap B\neq\emptyset$.

Lastly we recall that $\lnot\forall x\varphi(x) \iff \exists x\lnot\varphi(x)$. This translates well over bounded quantifiers:

\begin{align} \lnot(\forall x\in A, B(x)) &\iff \lnot\forall x(x\in A\rightarrow x\in B)\\ &\iff \exists x\lnot(x\in A\rightarrow x\in B)\\ &\iff \exists x(x\in A\land x\notin B)\\ &\iff \exists x\in A,\lnot B(x) \end{align}

-
I think this shows that Exists and Forall are simply less symmetric than I was expecting. – John Salvatier Jul 17 '11 at 1:28
@John: Could you elaborate? – Asaf Karagila Jul 17 '11 at 5:21

You might think of universal as a mega-intersection, and existential as a mega-union. E.g., if $A=\lbrace x_1,x_2,\dots\rbrace$ then your first formula is $B(x_1)$ and $B(x_2)$ and ..., while the second is $B(x_1)$ or $B(x_2)$ or ....

There is also some sort of symmetry in noting that "not for all" is the same as "there exists ... not," and "not there exists" is the same as "for all ... not."

-
I don't think this answers the question but +1 for the notion of forall being an extended conjunction and exists being an extended disjunction. I hadn't heard that notion before. Do you know of something that explores this notion? – John Salvatier May 22 '11 at 6:52
@John: It is a standard argument, in fact if you look closely you realize that it is actually the definition. In older papers $\forall$ was denoted by $\bigwedge$ and $\exists$ was denoted by $\bigvee$. – Asaf Karagila May 22 '11 at 8:39

As Asaf Karagila says, those two connectives, $\forall x \in A, \ldots$ and $\exists x \in A, \ldots$ are dual of each other.

Just like the conjunction / disjunction pair or the universal / existential pair, we have that $\lnot (\forall x \in A, \phi(x)) \Leftrightarrow \exists x \in A, \lnot \phi(x)$.

Also, if $A$ is a singleton $\{a\}$, those two connective are logically equivalent, and $\forall x \in A, \phi(x) \Leftrightarrow \exists x \in A, \phi(x) \Leftrightarrow \phi(a)$

-

Is this more symmetrical?

$\forall x \in A, B(x)$ means $\forall x (x \notin A \lor B(x))$

$\exists x \in A, B(x)$ means $\exists x (x \in A \land B(x))$

-
How is that different from what I wrote? – Asaf Karagila May 22 '11 at 10:37
You mention the above formula in only in passing. – Dietrich Epp May 22 '11 at 10:45