Originally asked and bountied at MSE:
Question: Can $\mathsf{ZFC}$ prove that for every countably infinite structure $\mathcal{A}$ in a countable language there is an ultrafilter $\mathcal{U}$ on $\omega$ such that the ultrapower $\mathcal{A}^\mathcal{U}$ has a nontrivial automorphism?
"Obviously" the answer is yes! (... right?)
Note that this is trivial in $\mathsf{ZFC+CH}$: $\mathsf{ZFC}$ alone proves that any nontrivial ultrapower is countably saturated, which in the presence of $\mathsf{CH}$ lets us run a back-and-forth argument to show that $\mathcal{A}^\mathcal{U}$ is non-rigid whenever $\mathcal{A}$ is countable and $\mathcal{U}$ is a nonprincipal ultrafilter on $\omega$. Separately, note that if we drop the requirement that the ultrafilter be on $\omega$ a positive answer follows from the Keisler-Shelah theorem, but $\mathsf{ZFC}$ can't bring down KS to $\omega$ as one might expect, so that ultimately doesn't seem like a promising direction.
I strongly suspect that I'm missing a very simple argument, but at present I'm not seeing it.
As a minor aside, I'm especially interested in a proof which avoids using results about first-order logic (techniques from the model-theory of first-order logic are fine). This comes from the original motivation for this question, which was a weakness in an MSE answer of mine where the whole point was to avoid some standard model theory. However, in retrospect this seems to be jumping the gun here, so I'll relegate this aspect of the question from the question itself to this mere side comment.
