# Two definitions of $\limsup$ on sequences of sets and underlying logic systems

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?