Motivated by a recent post here(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 found uses in some more outer fields(for example have they ever beend used in computability theory in any meaningful way, given that it is my favorite branch of logic).