Expressive power of $\omega$-order logic

Question

According to the article Second-order and Higher-order Logic from the Stanford Encyclopedia of Philosophy,

there is no need to stop at second-order logic; one can keep going. [...] we can allow quantification over super-predicate symbols. And then we can keep going further.

We reach the level of type theory after ω steps.

I wonder what the expressive power of "$\omega$-order logic" is:

Can you give an example of two structures $\mathcal A$, $\mathcal B$ that satisfy the same $\omega$-order sentences but are not isomorphic?

Answer 1

Instead of an example, I give an existence proof:

Take any finite or countable language, for example the language of equality. Since all formulas (even in $\omega$-logic) are finite, there are only countably many formulas, hence at most $\mathfrak c:= 2^{\aleph_0}$ many theories. Find more than continuum many cardinalities (for example $\{\aleph_\alpha:\alpha < \mathfrak c^+\}$), and for each such cardinality $\kappa$ find a structure whose size is $\kappa$. These structures are pairwise non-isomorphic, but there must be two that satisfy the same set of $\omega$-sentences.

(For languages with $\lambda$ many symbols, replace $\mathfrak c^+$ by $(2^\lambda)^+$.)