$A_1 \cap A_2 \cap \cdots \cap A_n \ne \emptyset$ holds for all $n$. Must it be that $\bigcap_{n = 1}^{\infty} A_n \ne \emptyset$?

Question

Let $A_1, A_2, A_3, \,\ldots$ be sets such that $A_1 \cap A_2 \cap \cdots \cap A_n \ne \emptyset$ holds for all $n$.

Must it be that $\bigcap_{n = 1}^{\infty}A_n \ne \emptyset$?

I answered no. Here is my "proof".

Define $A_n = \{n+1, n+2, \,\ldots\}$.

Then $A_1 \cap A_2 \cap \cdots \cap A_n = \{n+1, n+2, \,\ldots\}$.

For all integers $n$, $\{n+1, n+2, \,\ldots\} \ne \emptyset$, since it contains $n+1$, and there is no largest integer.

Now consider $\bigcap_{n = 1}^{\infty} A_n$.

Suppose it contains an integer $m$. But $m \notin A_{m}$ by definition, hence $m \notin \bigcap_{n = 1}^{\infty} A_n$, so $\bigcap_{n = 1}^{\infty} A_n = \emptyset$.$$\tag*{$\blacksquare$}$$

Is that correct?

I ask because in my lecture notes, the definition of $\bigcap_{n = 1}^{\infty} A_n$ is $\{x : x \in A_n \ \forall n \}$ which (to me) seems to be equivalent to "$A_1 \cap A_2 \cap \cdots \cap A_n \ne \emptyset$ holds for all $n$", which would of course mean the answer is yes.

Answer 1

The key here, as Ian's comment says, is that the first statement $\;\langle \forall n :: \langle \cap i : i \leq n : A_i \rangle \not= \emptyset \rangle\;$ is (by the definitions) equivalent to $$ \langle \forall n :: \langle \exists x :: \langle \forall i : i \leq n : x \in A_i \rangle \rangle \rangle $$ while the second statement $\;\langle \cap i :: A_i \rangle \not= \emptyset\;$ is equivalent to $$ \langle \exists x :: \langle \forall i :: x \in A_i \rangle \rangle $$

These two are not equivalent, as you correctly show by your counterexample of $\;A_i = \{j | j > i\}\;$ which makes the first statement true (by choosing $\;x := n+1\;$) and the second false.

$ \newcommand{\calc}{\begin{align} \quad &} \newcommand{\calcop}[2]{\\ #1 \quad & \quad \text{"#2"} \\ \quad & } \newcommand{\endcalc}{\end{align}} $However, note that the second statement does imply the first:

$$\calc \langle \forall n :: \langle \exists x :: \langle \forall i : i \leq n : x \in A_i \rangle \rangle \rangle \calcop{\Leftarrow}{logic: strengthen by weakening range of $\;\forall i\;$} \langle \forall n :: \langle \exists x :: \langle \forall i :: x \in A_i \rangle \rangle \rangle \calcop{\Leftarrow}{logic: remove unused $\;\forall n\;$} \langle \exists x :: \langle \forall i :: x \in A_i \rangle \rangle \endcalc$$

Answer 2

Take $A_n = \left(0, \dfrac{1}{n}\right)$, then $\displaystyle \bigcap_{k=1}^n A_k = \left(0,\dfrac{1}{n}\right)$, and $\displaystyle \bigcap_{k=1}^\infty A_k = \emptyset$.