# Can $\exists$ be transformed into enumeration in the case of a finite domain?

For example, according to the union axiom,$$a\in \bigcup\{u,v\}\Leftrightarrow \exists w\in \{u,v\}\,(a\in w)$$ Since $$\{u,v\}$$ contains only two elements, can this proposition be directly replaced by enumeration as follows? $$a\in \bigcup\{u,v\}\Leftrightarrow (a\in u\lor a\in v)$$ If so, how does this replacement use the proposition $$w\in\{u,v\}\Leftrightarrow (w=u\lor w=v)$$？ I am unsure how to incorporate this proposition into the original statement to derive the final result. Is there a more rigorous theory regarding $$\exists$$ that addresses this?

• Yes, of course. $\exists$ "works" like disjunction. Thus, for finite domains you can simply write $x=a \lor x=b \lor \ldots \lor x=z$. The same for $\forall$ that works as a conjunction. Commented Jul 23 at 9:31
• The symbol $\bigcup$ is extraneous. Commented Jul 23 at 10:10
• @RobArthan it's not wrong. If $u = v = \mathbb{N}$ then $a \in \mathbb{N} \Leftrightarrow \exists w \in \{\mathbb{N}\}. a \in w$, as expected. Commented Jul 23 at 22:00
• @NaïmFavier: apologies. I misread the question. Commented Jul 23 at 22:04

Keep in mind that all quantifications are unbounded in single-sorted first-order logic (which ZF is based upon): formally, $$\exists w\in\{u, v\}. a \in w$$ is shorthand for $$\exists w. w \in \{u, v\} \land a \in w$$

Now by definition of $$\{u, v\}$$ (the axiom of pairing) this is equivalent to $$\exists w. (w = u \lor w = v) \land a \in w$$

We can distribute $$\land$$ over $$\lor$$ to get $$\exists w. (w = u \land a \in w) \lor (w = v \land a \in w)$$ and distribute $$\exists$$ over $$\lor$$ to get $$(\exists w. w = u \land a \in w) \lor (\exists w. w = v \land a \in w)$$

Finally, you should convince yourself that $$\exists x. x = y \land P(x)$$ is equivalent to $$P(y)$$¹, so that this is equivalent to $$a \in u \lor a \in v$$

¹ And dually $$\forall x. x = y \to P(x)$$ is equivalent to $$P(y)$$. This is a simple form of the Yoneda lemma.

• Your answer was really helpful, thank you! So, can I consider $[\exists x. x=y\land P(x)]\Leftrightarrow P(y)$ as a logical axiom? Commented Jul 23 at 9:52
• Well, it's not an axiom, it's a theorem. You can prove it from the equality axioms. Commented Jul 23 at 9:59
• Thank you! Is my understanding correct that using the axiom of substitution, we can prove $(\Rightarrow)$, and for $(\Leftarrow)$, there indeed exists $y=y$ such that $P(y)$ holds true? It seems I can't elaborate further on this. I feel that $\exists$ and $\forall$ are quite subtle, and differ from logical connectives defined by truth tables. Commented Jul 23 at 10:21
• @user1361001 yes, that's all there is to it. Commented Jul 23 at 10:29

$$\exists a\in A:p(a)$$

can be written as the disjunction

$$\bigvee_{a\in A} p(a)$$

which expands as $$p(a)\lor p(b)\lor\cdots$$

$$\exists w\in\{u,v\}: a\in w\iff a\in u\lor a\in v$$