According to the article <a href="http://plato.stanford.edu/entries/logic-higher-order/">Second-order and Higher-order Logic
</a> 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?