I'm trying to express the closure under countable union by using formal language, as I'm praticing the language. The following is the statement that I found on proofwiki. $$\forall x_n\in\Sigma:n=1,2,\cdots:\bigcup_{n=1}^{\infty}x_n\in\Sigma$$ It seems that it's written in formal language, but strictly speaking, the sentence has some grammatical errors, somewhat informal and implicit (e.g., an alphabet after a quantifier must be a variable, but $x_n$ is implicitly given as a function, and dots in $n=1,2,\cdots$ is not an alphabet of formal language.)
I think the sentence should be in $L^{\mathrm{II}}$, which means it's second-order logic. What I've done is the following but am not sure. $$\forall x:((\exists f:f:S\leftrightarrow\mathbb{N}\wedge Sx\wedge \Sigma x)\implies \Sigma\bigcup S)$$ ($f:S\leftrightarrow\mathbb{N}$ means a bijection from a set $S$ to the set of natural numbers $\mathbb N$, $S$ and $\Sigma$ are unary relations.)