One of the reasons I think ultrapowers are interesting is the following corollary of Łoś's theorem:



> 
> Let $V$ be a relational structure and $^\*V$ an ultrapower of $V$. Then a first order statement about $V$ is true if and only if the corresponding statement for $^\*V$ is true, where the relations $R$ on $V$ are replaced by their enlargements $^\*R$.
> 
> 
> 


This suggests the following question: what construction should replace the ultraproduct if I want a similar result for 2nd or higher order statements? A little googling suggests that a book by van Benthem called Modal Logic and Classical Logic might contain an answer, but I don't have access to a copy.



ultrapowers and higher order logic
Look. Suppose you take an infinite sequence of sets $ A\_0, A\_1, A\_2, \dots $ (with no structure apart from equality, that is, no relations or functions), such that $ A\_n $ has $ n $ elements. If you take a ultraproduct of these sets (using a non-principal ultrafilter over their indices), can the product be a finite set? No, because for any natural number $ n $, all but finite of these sets have more than $ n $ elements, and ther being more than non-equal $ n $ elements is a first-order property, so this same property must be true for the ultraproduct as well, so the product has more than $ n $ elements for any natural number $ n $. So far, so good. 


But now suppose you could take some kind of advanced ultraproduct of these sets that keeps not only the first order statements but all second order statements that are true in the majority of the sets. But there being only finitely many elements is a second order statement, so this advanced ultraproduct would have to be finite as well, because all the sets are finite. This is, in simple terms, why you can't have such a generalization of ultraproducts.


