Prove an existential quantifier goal by assuming there exists an arbitrary value that makes the expression true.

Question

I'm trying to prove the following:

Suppose { A$_{i}$ | i $\in$ I } is an indexed family of sets and I $\neq$ $\emptyset$. Prove that $\cap$$_{i \in I}$A$_{i}$ $\in$ $\cap$$_{i \in I}$$\mathcal{P}(A_{i})$.

I first analysed the logical structure of $\cap$$_{i \in I}$A$_{i}$ $\in$ $\cap$$_{i \in I}$$\mathcal{P}(A_{i})$:

$\cap$$_{i \in I}$A$_{i}$ $\in$ $\cap$$_{i \in I}$$\mathcal{P}(A_{i})$

$\exists$i $\in$ I($\cap$$_{i \in I}$A$_{i}$ $\in$ $\mathcal{P}(A_{i})$)

$\exists$i $\in$ I($\cap$$_{i \in I}$A$_{i}$ $\subseteq$ A$_{i}$)

In order to prove a goal of the form $\exists$x P(x), I should present a variable and prove that P(x) is true for that variable.

In this case, I should present a variable that is a member of I, and makes $\cap$$_{i \in I}$A$_{i}$ $\subseteq$ A$_{i}$ true.

I did the following instead:

• Let i be an arbitrary element of I.
• That allowed me to transform my goal to $\cap$$_{i \in I}$A$_{i}$ $\subseteq$ A$_{i}$.
• Using the subset definition, this becomes $\forall$x(x $\in$ $\cap$$_{i \in I}$A$_{i}$ $\implies$ x $\in$ A$_{i}$).
• Let x be arbitrary, suppose x $\in$ $\cap$$_{i \in I}$A$_{i}$ and transform my goal to x $\in$ A$_{i}$.
• x $\in$ $\cap$$_{i \in I}$A$_{i}$ becomes $\forall$i $\in$ I(x $\in$ A$_{i}$).
• As I'm letting i be an arbitrary element of I, I can use universal instantiation to conclude x $\in$ A$_{i}$.
• I can then conclude that there exists a value i $\in$ I such that $\cap$$_{i \in I}$A$_{i}$ $\subseteq$ A$_{i}$ and finish my proof.

Is this valid reasoning? I'm concerned about assuming that there exists an arbitrary element that makes the existential quantifier goal true, and relying on that to check that in fact there exists such a value, when my book recommends that I should choose a specific value that makes the predicate true instead.

Answer 1

You got off on the wrong foot right at the beginning, I’m afraid. You want to prove something of the form $x\in\bigcap_{i\in I}S_i$; this is true if and only if $x\in S_i$ for every $i\in I$, so your goal is a universal statement, not an existential one. Specifically, you want to show that

$$\bigcap_{i\in I}A_i\in\wp(A_j)\tag{1}$$

for each $j\in I$. Note that I’ve avoided a clash of indices by using $j$ for the specific index on the right and $i$ for the dummy index on the left.

Technically it’s not incorrect to write $\bigcap_{i\in I}A_i\in\wp(A_i)$, since the syntax itself tells us that the $i$ on the left is a dummy variable and that the one on the right is not, but it’s very confusing and best avoided.

Apart from the confusing clash of indices, what you then did is almost correct for this goal: $(1)$ translates to

$$\bigcap_{i\in I}A_i\subseteq A_j\text{ for each }j\in I$$

and then to

$$\forall x\left(x\in\bigcap_{i\in I}A_i\to x\in A_j\right)\text{ for each }j\in I\;,$$

and so on. In short, you’re simply missing the universal quantifier on $j$ in each step.

At the end, however, your conclusion should not be that there is a $j\in I$ such that $(1)$ holds, but rather that $(1)$ holds for each $j\in I$: your goal is the univerally quantified statement.

Your goal would be existentially quantified if, for instance, you were trying to prove that

$$\bigcap_{i\in I}A_i\in\bigcup_{i\in I}\wp(A_i)\;,$$

which is true, or that

$$\bigcup_{i\in I}A_i\in\bigcup_{i\in I}\wp(A_i)\;,$$

which is false in general and therefore couldn’t be proved.

Answer 2

This is not really an answer to your question, but still it might be helpful. Here is an alternative way to design and write down this proof, where the analysis of the logical structure is done more systematically: we expand the definitions, and then use the laws of logic to simplify.

$ \newcommand{\calc}{\begin{align} \quad &} \newcommand{\op}[1]{\\ #1 \quad & \quad \unicode{x201c}} \newcommand{\hints}[1]{\mbox{#1} \\ \quad & \quad \phantom{\unicode{x201c}} } \newcommand{\hint}[1]{\mbox{#1} \unicode{x201d} \\ \quad & } \newcommand{\endcalc}{\end{align}} \newcommand{\ref}[1]{\text{(#1)}} \newcommand{\then}{\Rightarrow} \newcommand{\followsfrom}{\Leftarrow} \newcommand{\true}{\text{true}} \newcommand{\false}{\text{false}} \newcommand{\P}[1]{\mathcal P(#1)} $We calculate as follows, where $\;i,j\;$ range over the index set $\;I\;$:

$$\calc \langle \cap i :: A_i \rangle \;\in\; \langle \cap i :: \P{A_i} \rangle \op\equiv \hints{definition of (rightmost) $\;\cap\;$,} \hint{renaming the leftmost $\;i\;$ to $\;j\;$ to prevent 'shadowing'} \langle \forall i :: \langle \cap j :: A_j \rangle \in \P{A_i} \rangle \op\equiv\hint{definition of $\;\P\;$} \langle \forall i :: \langle \cap j :: A_j \rangle \subseteq A_i \rangle \op\equiv\hint{definition of $\;\subseteq\;$} \langle \forall i :: \langle \forall x :: x \in \langle \cap j :: A_j \rangle \;\then\; x \in A_i \rangle \rangle \op\equiv\hint{definition of $\;\cap\;$} \tag{*} \langle \forall i :: \langle \forall x :: \langle \forall j :: x \in A_j \rangle \;\then\; x \in A_i \rangle \rangle \op\equiv\hint{logic: specialization using $\;j := i\;$} \langle \forall i :: \langle \forall x :: \true \rangle \rangle \op\equiv\hint{logic: simplify} \true \endcalc$$

This proves the statement.

Note how everything up until $\ref{*}$ is just definition expansion, and the simplification is easy to see at that point, by inspecting the shape of the formula. Note also how writing $\;i\;$ and $\;j\;$ instead of $\;i \in I\;$ and $\;j \in I\;$ helps to keep the expressions readable, and focus on their essential structure.