Using infinitary logic to express your statement is somewhat overkill. The usual formulation of 2nd order logic only allows subsets $X\subseteq\mathbb{N}$ to be quantified over (which can be seen as functions $X\rightarrow {\bf 2}$) rather than arbitrary functions, which would easily allow you to define two sequences $x,y:\mathbb{N}\rightarrow\mathbb{R}$ and say $$ \forall i\in\mathbb{N},\ x(i)>y(i)$$ as mentioned in the comments.

However, the usual formulation of 2nd order logic is quite strong, and functions $\mathbb{N}\rightarrow\mathbb{N}$ and sequences $\mathbb{N}\rightarrow\mathbb{R}$ can easily be coded in it! I'll try to sketch the argument below, but first note that because of all this expressive power, there's no hope of quantifier elimination or decidability in this logic.

1. Coding rationals: first note that by usual arithmetic tricks that I won't get into here, it's easy to code pairs in $\mathbb{N}\times\mathbb{N}$, triples etc. even finite sequences using just natural numbers. By suitably defining operations and equality, we can code $\mathbb{Z}$ as a subset of $\mathbb{N}\times\mathbb{N}$, and $\mathbb{Q}\subset \mathbb{N}\times \mathbb{Z}$, so $\mathbb{Q}$ is coded as a subset of triples, themselves coded as natural numbers.

2. Building real numbers. So by 1. to build a function $\mathbb{N}\rightarrow \mathbb{Q}$, it suffices to build functions $\mathbb{N}\rightarrow \mathbb{N}$! But this can be done by describing a function $f$ as a subset $f\subseteq\mathbb{N}\times\mathbb{N}$ with certain properties, as is done in set theory. As before, pairs can be coded as individual numbers, so you can describe these subsets in 2nd order arithmetic.

3. Now that real numbers are described as sequences of natural numbers (elements of $\mathbb{N}\rightarrow\mathbb{N}$, it's pretty easy to build sequences of real numbers, by noticing that a function $f:\mathbb{N}\rightarrow \mathbb{N}^{\mathbb{N}}$ is just a function $\hat{f}:\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ (known as the reverse curryfication of $f$, or as Schönfinkel's trick).

Using infinitary logic to express your statement is somewhat overkill. The usual formulation of 2nd order logic only allows subsets $X\subseteq\mathbb{N}$ to be quantified over (which can be seen as functions $X\rightarrow {\bf 2}$) rather than arbitrary functions, which would easily allow you to define two sequences $x,y:\mathbb{N}\rightarrow\mathbb{R}$ and say $$ \forall i\in\mathbb{N},\ x(i)>y(i)$$ as mentioned in the comments.

However, the usual formulation of 2nd order logic is quite strong, and functions $\mathbb{N}\rightarrow\mathbb{N}$ and sequences $\mathbb{N}\rightarrow\mathbb{R}$ can easily be coded in it! I'll try to sketch the argument below, but first note that because of all this expressive power, there's no hope of quantifier elimination or decidability in this logic.

1. Coding rationals: first note that by usual arithmetic tricks that I won't get into here, it's easy to code pairs in $\mathbb{N}\times\mathbb{N}$, triples etc. even finite sequences using just natural numbers. By suitably defining operations and equality, we can code $\mathbb{Z}$ as a subset of $\mathbb{N}\times\mathbb{N}$, and $\mathbb{Q}\subset \mathbb{N}\times \mathbb{Z}$, so $\mathbb{Q}$ is coded as a subset of triples, themselves coded as natural numbers.

2. Building real numbers. So by 1. to build a function $\mathbb{N}\rightarrow \mathbb{Q}$, it suffices to build functions $\mathbb{N}\rightarrow \mathbb{N}$! But this can be done by describing a function $f$ as a subset $f\subseteq\mathbb{N}\times\mathbb{N}$ with certain properties, as is done in set theory. As before, pairs can be coded as individual numbers, so you can describe these subsets in 2nd order arithmetic.

3. Now that real numbers are described as sequences of natural numbers (elements of $\mathbb{N}\rightarrow\mathbb{N}$, it's pretty easy to build sequences of real numbers, by noticing that a function $f:\mathbb{N}\rightarrow \mathbb{N}^{\mathbb{N}}$ is just a function $\hat{f}:\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ (known as the reverse curryfication of $f$, or as Schönfinkel's trick).

To answer your follow-up question, I don't know of any quantifier elimination for ${\cal L}_{\omega_1\omega_1}$, but keep in mind that even quantifier-free formulas are undecidable in that logic, because of it's infinitary nature (which makes it not very interesting, in my opinion).

I'm not crazy about using infinitary logic to express something that can easily be said in much weaker fragments. The usual formulation of 2nd order logic only allows subsets $X\subseteq\mathbb{N}$ to be quantified over (which can be seen as functions $X\rightarrow {\bf 2}$) rather than arbitrary functions, which would easily allow you to define two sequences $x,y:\mathbb{N}\rightarrow\mathbb{R}$ and say $$ \forall i\in\mathbb{N},\ x(i)>y(i)$$ as mentioned in the comments.

However, the usual formulation of 2nd order logic is quite strong, and functions $\mathbb{N}\rightarrow\mathbb{N}$ and sequences $\mathbb{N}\rightarrow\mathbb{R}$ can easily be coded in it! I'll try to sketch the argument below, but first note that because of all this expressive power, there's no hope of quantifier elimination or decidability in this logic.

1. Coding rationals: first note that by usual arithmetic tricks that I won't get into here, it's easy to code pairs in $\mathbb{N}\times\mathbb{N}$, triples etc. even finite sequences using just natural numbers. By suitably defining operations and equality, we can code $\mathbb{Z}$ as a subset of $\mathbb{N}\times\mathbb{N}$, and $\mathbb{Q}\subset \mathbb{N}\times \mathbb{Z}$, so $\mathbb{Q}$ is coded as a subset of triples, themselves coded as natural numbers.

2. Building real numbers. So by 1. to build a function $\mathbb{N}\rightarrow \mathbb{Q}$, it suffices to build functions $\mathbb{N}\rightarrow \mathbb{N}$! But this can be done by describing a function $f$ as a subset $f\subseteq\mathbb{N}\times\mathbb{N}$ with certain properties, as is done in set theory. As before, pairs can be coded as individual numbers, so you can describe these subsets in 2nd order arithmetic.

3. Now that real numbers are described as sequences of natural numbers (elements of $\mathbb{N}\rightarrow\mathbb{N}$, it's pretty easy to build sequences of real numbers, by noticing that a function $f:\mathbb{N}\rightarrow \mathbb{N}^{\mathbb{N}}$ is just a function $\hat{f}:\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ (known as the reverse curryfication of $f$, or as Schönfinkel's trick).

Using infinitary logic to express your statement is somewhat overkill. The usual formulation of 2nd order logic only allows subsets $X\subseteq\mathbb{N}$ to be quantified over (which can be seen as functions $X\rightarrow {\bf 2}$) rather than arbitrary functions, which would easily allow you to define two sequences $x,y:\mathbb{N}\rightarrow\mathbb{R}$ and say $$ \forall i\in\mathbb{N},\ x(i)>y(i)$$ as mentioned in the comments.

However, the usual formulation of 2nd order logic is quite strong, and functions $\mathbb{N}\rightarrow\mathbb{N}$ and sequences $\mathbb{N}\rightarrow\mathbb{R}$ can easily be coded in it! I'll try to sketch the argument below, but first note that because of all this expressive power, there's no hope of quantifier elimination or decidability in this logic.

1. Coding rationals: first note that by usual arithmetic tricks that I won't get into here, it's easy to code pairs in $\mathbb{N}\times\mathbb{N}$, triples etc. even finite sequences using just natural numbers. By suitably defining operations and equality, we can code $\mathbb{Z}$ as a subset of $\mathbb{N}\times\mathbb{N}$, and $\mathbb{Q}\subset \mathbb{N}\times \mathbb{Z}$, so $\mathbb{Q}$ is coded as a subset of triples, themselves coded as natural numbers.

2. Building real numbers. So by 1. to build a function $\mathbb{N}\rightarrow \mathbb{Q}$, it suffices to build functions $\mathbb{N}\rightarrow \mathbb{N}$! But this can be done by describing a function $f$ as a subset $f\subseteq\mathbb{N}\times\mathbb{N}$ with certain properties, as is done in set theory. As before, pairs can be coded as individual numbers, so you can describe these subsets in 2nd order arithmetic.

3. Now that real numbers are described as sequences of natural numbers (elements of $\mathbb{N}\rightarrow\mathbb{N}$, it's pretty easy to build sequences of real numbers, by noticing that a function $f:\mathbb{N}\rightarrow \mathbb{N}^{\mathbb{N}}$ is just a function $\hat{f}:\mathbb{N}\rightarrow\mathbb{N}\times\mathbb{N}$ (known as the reverse curryfication of $f$, or as Schönfinkel's trick).