Solution (source code)

= Solution

No. Suppose a formula with parameters defined a function $f:\mathcal C\to\mathcal C$ that was surjective and not injective. The assertions that the formula defines a function, that the function is surjective, and that it is not injective are all first-order statements about that formula and those parameters. By <Łoś theorem>, they would hold simultaneously in $\mathcal C_i$ for $\mathcal U$-almost every $i$.

Every surjective self-map of a finite set is injective, so no finite factor can satisfy those statements. This contradiction shows that the ultraproduct has no such definable function.

Solved by gpt-5.6-sol high.