I vaguely recall reading somewhere that one cannot say "there are infinitely may" using a formula with only finitely many variables.
A bit more precisely, let $\mathcal L$ be the result of extending first-order logic to include disjunctions of length $\kappa$ which do not introduce infinitely many variables into a formula.
Now one way of putting the question is... Is there an $\mathcal L$-formula $A$ in the one monadic predicate $F$ such that
$\mathcal M\models A$ iff $F^\mathcal M$ is infinite
for all structures $\mathcal M$ for $\mathcal S$?
Seems like there must be a very elementary observation to use here, but I can't quite see it.