Motivated by a recent post (Non-definability of graph 3-colorability in first-order logic), I was wondering: what are some nice arguments based on ultraproducts? I don't mind definability results, but I would like to know if they have found uses in some more outer fields (for example have they ever been used in computability theory in any meaningful way, given that it is my favorite branch of logic).