Is there a known result to the effect that it cannot be the case that for some natural $n$, there is a formula of length $n$ such that all cardinals can be defined by a formula whose length is shorter than $n$? I'm speaking in the milieu of some fragment of a standard set theory extending first order logic with identity and membership, for example $\text{ZF-Regularity}$. I've always expected that as regards the $\aleph_\alpha$ numbers the bigger it is the longer is the shortest definition of it. Or in general there cannot be a finite bound on definability of all of them. Is that correct?