Let $X$ be a set, $(E_n)$ be a sequence of subsets of $X$. As I know, the definition of $\limsup_n E_n$ is the subset of $X$ consists of $x \in X$ such that $x \in E_n$ for infinitely many $n$. Also, there is a definition using union and intersection: $\limsup_n E_n = \bigcap_{n = 1}^\infty \bigcup_{m = n}^\infty E_m$. I want to ask about if the choice of logic systems matters the equivalence of two definitions.
I am curious about the formalization of the condition $\varphi(x)$: "$x \in E_n$ for infinitely many $n \in \mathbb{N}$". I guess there are two of them:
- there exists a sequence $(n_k)$ of $\mathbb{N}$ such that $n_k < n_{k + 1}$ and $x \in E_{n_k}$ for every $k \in \mathbb{N}$.
- for any $n \in \mathbb{N}$, there exists $m \in \mathbb{N}$ such that $m > n$ and $x \in E_m$.
I think the former one is stronger than the latter one. Using latter one, $\{x: \varphi(x)\}$ is immediately equal to $\bigcap_{n = 1}^\infty \bigcup_{m = n}^\infty E_m$, but it seems not obvious if $\{x: \varphi(x)\} \supset \bigcap_{n = 1}^\infty \bigcup_{m = n}^\infty E_m$ if I use the former one. In order to show this containment, one should prove the existence of such infinite sequence, assuming the latter condition. I am not sure if I can go without proper axiom of choice. In particular, I wonder, in order to construct such infinite sequence, whether I need $\mathsf{DC}$, or I just can go with only mathematical induction.
By the way, I am going to construct such sequence, by taking $n_1$ as the minimum $m$ such that $m > 1$ and $x \in E_m$, and once $n_k$ is chosen, then I take $n_{k + 1}$ as $m$ such that $m > n_k$ and $x \in E_{m}$. In this construction, is the existence of $(n_k)$ immediate from the mathematical induction? Or, should I put more axioms?
