# Formal logic and functions (I am struggling with writing my proof)

I wish to show that $f\left(\bigcup_aX_a\right)=\bigcup_af(X_a)$

My attempt:
$$y\in f\left(\bigcup_aX_a\right)\implies\exists x\in\bigcup_aX_a:y\in f(\{x\})$$ which I didn't like, so I re-wrote it as:
$$\forall y\in f\left(\bigcup_aX_a\right)\exists x\in\bigcup_aX_a:y\in f(\{x\})$$

I have to introduce an $x$, I need to put an exists somewhere (unlike proving De Morgan's laws, where you can just say $x\in$left hand side $\implies\in$RHS and then the other way)

Now I can write the "if $x$ is in the union of some sets it is in at least one of them" nicely as:

$$\forall x\in\bigcup_aX_a\exists b:x\in X_b$$ - given an $x$ I can get a $b$.

How do I use this above?

$$\forall y\in f\left(\bigcup_aX_a\right)\exists x\exists b:x\in X_b\implies y\in f(\{x\})$$

I am saying for all y there exists an x (based on that y) there exists a b based on that x and y with $x\in X_b$.... surely I could also say "there exists a b where there exists an x such that x in $X_b$ implies...."

I will want to go to:

$\forall y\in f\left(\bigcup_aX_a\right)\exists b:y\in f(X_b)$ which makes me want to swap round the order of exists.

Then from this we go (not sure how to write it with equal rigor) that y would be in the union of $f(X_a)$ over a.

Completing the proof

## My first attempt:

$y\in f\left(\bigcup_aX_a\right)\implies f^{-1}(\{y\})\subset \bigcup_aX_a$ so $\exists x\in f^{-1}(\{y\})$ with $x\in\bigcup_aX_a$ which doesn't feel as concrete as I'd like.

-
@MauroALLEGRANZA have I made a mistake? I intentionally wrote $f^{-1}(\{y\})$ it is the set that contains $x$ if the function maps x to y. For an infinite set $f:\mathbb{R}\rightarrow\mathbb{R}$ given by $f(x)=x^2$ you'd have $f^{-1}(4)=f^{-1}(\{4\})=\{-2,2\}$, I used the set notation to make this more explicit. I never state that the function is surjective or injective because it might be neither. – Alec Teal Apr 30 '14 at 14:53

This is not a real answer, but a long comment to jdc's answer.

To be totally "formal" is an hard task, due to the huge amont of defined symbols used in set language [see as example : Yuri Manin, A Course in Mathematical Logic for Mathematicians (2010), Chapter 1.3 : Beginenrs' Course in Translation, page 9-on].

Let us try with :

$∃x \in \bigcup_a X_a (f(x)=y)$.

In order to simplify it, abbreviate the formula $(f(x)=y)$ as $\varphi(x,y)$; thus, we have (more "formally") :

$(\exists x) (x \in \bigcup_a X_a \land \varphi(x,y))$.

Now, if we have the simpler case of $X_1 \cup X_2$, our formula will be :

$(\exists x) [(x \in (X_1 \cup X_2)) \land \varphi(x,y)]$.

This is "quite" first-order logic ...

The condition $x \in (X_1 \cup X_2)$, by definition of union of sets, is equivalent to:

$(x \in X_1) \lor (x \in X_2)$.

Now, with the "$\bigcup$-case", we are not allowed to write a "potentially" infinite disjunction; thus, we have to use $\exists$.

We have that $x \in \bigcup_a X_a$ is equivalent to :

$(\exists a) [(a \in A) \land (x \in X_a)]$,

where $A$ is the (left implicit) index-set.

We try now to "assemble" all together :

$(\exists x) ( \quad (\exists a) [(a \in A) \land (x \in X_a)] \land \varphi(x,y) \quad )$.

Now we need a rule for quantifiers :

$\exists x P(x) \land Q \leftrightarrow \exists x (P(x) \land Q), \quad$ provided that $x$ is not free in $Q$.

In our formula above, $i$ is not free in $\varphi(x,y)$; thus we apply the rule to get :

$(\exists x) (\exists a) ( [(a \in A) \land (x \in X_a)] \land \varphi(x,y) )$.

Now we need a second rule for quantifiers :

$\exists x \exists y P(x,y) \leftrightarrow \exists y \exists x P(x,y)$.

Applying it we have :

$(\exists a) (\exists x) ( [(a \in A) \land (x \in X_a)] \land \varphi(x,y) )$.

An this is (again "omitting" the index-set) :

$(\exists a) (\exists x) [(x \in X_a) \land f(x)=y]$

that, with a little "sloppiness", we write it as :

$∃a ∃x \in X_a (f(x)=y)$.

An then we can try to go on ...

Recalling that a function in set theory is a set of ordered couples, we have that $f(x)=y$ is :

$(x,y) \in f$

where in turn $f \subseteq X_a \times f[X_a]$.

Thus : $x \in X_a$ and $y \in f[X_a]$.

In conclusion, from : $∃a ∃x \in X_a (f(x)=y)$

we have that :

$\exists a (y \in f[X_a])$.

The last step is easy ... and I hope it can help.

-
I feel that is an actual answer, because it hints that what the OP is trying to accomplish is not doable in this context, it lacks background, which you gave. – Git Gud Apr 30 '14 at 16:08

I'm not sure what you mean by "concrete," but the following is correct.

$y \in f[\bigcup_\alpha X_\alpha]$ if and only if there exists $x \in \bigcup_\alpha X_\alpha$ such that $f(x) = y$. This happens if and only if there exists an $\alpha$ such that $x \in X_\alpha$ and $f(x) = y$, which in turn means that there is an $\alpha$ such that $y \in f[X_\alpha]$. But that means $y \in \bigcup_\alpha f[X_\alpha]$.

Given the number of things you've said above you don't like, this may or may not be anything like what you're looking for.

Edit: In the vague hope that you might like something more formal (and don't mind chaining "iff" signs in a manner that some mathematicians consider abusive), I offer the following.

\begin{align*} y \in f\Big[\bigcup_\alpha X_\alpha\Big] &\iff \exists x \in \bigcup_\alpha X_\alpha \ \big(f(x) = y\big)\\ &\iff \exists \alpha\ \exists x \in X_\alpha \big(f(x) = y\big)\\ &\iff \exists \alpha\ \big(y \in f[X_\alpha]\big) \\ &\iff y \in \bigcup_\alpha f[X_\alpha]. \end{align*}

-
By don't like I mean "if I couldn't see that the thing I was trying to prove was right, I'd have no confidence that I had proved it" quite often with the more "intuitive" proofs I would end up proving something that wasn't true because I imagined a special case or something. So I try and at least have the ability to be overly demanding on the rigor I want in a proof. – Alec Teal Apr 30 '14 at 14:58
But yeah, I got what you're saying, that is my 2 line proof which I start at the bottom, which I agree with. I'm dragging myself though the rigor of the top part of the question intentionally. I ought to be able to be that rigorous. – Alec Teal Apr 30 '14 at 14:59
Superb, thanks! One quick question, why did you choose to go $\exists\alpha\exists x$ why not, $\exists x\exists\alpha$ this is actually why I posted the question. – Alec Teal Apr 30 '14 at 15:21
@AlecTeal Quantifiers of the same kind commute. Why is this? It comes from formal systems. In regular mathematics this is simply assumed. Without more background, it's not possible to justify this commutativity. – Git Gud Apr 30 '14 at 15:27
@AlecTeal Any Mathematical Logic book. For instance Enderton's A mathematical introduction to logic. – Git Gud Apr 30 '14 at 15:33

Using slightly different notations which I find more convenient, the statement to be proved is $$\tag{0} f[\langle \cup a :: X_a \rangle] \;=\; \langle \cup a :: f[X_a] \rangle$$ where the definitions are \begin{align} \tag{1} & y \in f[X] \;\equiv\; \langle \exists x : f(x) = y : x \in X \rangle \\ \tag{2} & z \in \langle \cup a :: V(a) \rangle \;\equiv\; \langle \exists a :: z \in V(a) \rangle \\ \end{align}

For me, the simplest way to prove $(0)$ is to go to the element level using these definitions, and use the laws of logic: investigate which elements are part of the left hand side, and then transform into the right hand side.

In other words, for any $\;y\;$ we calculate as follows:

\begin{align} & y \in f[\langle \cup a :: X_a \rangle] \\ \equiv & \qquad \text{"definition (1) for $\;\cdot[\cdot]\;$"} \\ & \langle \exists x : f(x) = y : x \in \langle \cup a :: X_a \rangle \rangle \\ \equiv & \qquad \text{"definition (2) for $\;\langle \cup \ldots \rangle\;$"} \\ & \langle \exists x : f(x) = y : \langle \exists a :: x \in X_a \rangle \rangle \\ (*) \;\;\; \equiv & \qquad \text{"logic: exchange $\;\exists\;$ quantifications"} \\ & \langle \exists a :: \langle \exists x : f(x) = y : x \in X_a \rangle \rangle \\ \equiv & \qquad \text{"definition (1) for $\;\cdot[\cdot]\;$"} \\ & \langle \exists a :: y \in f[X_a] \rangle \\ \equiv & \qquad \text{"definition (2) for $\;\langle \cup \ldots \rangle\;$"} \\ & y \in \langle \cup a :: f[X_a] \rangle \\ \end{align}

which proves $(0)$ by set extensionality.

This proof clearly shows that the key step $(*)$ is that two nested $\;\exists\;$ quantifications (or two nested unions) may be exchanged.

-