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?
Should the above be un-attainable, then is there a known argument against for example $n=10$ being such an upper bound?
Related is the following question: is it the case that definability of being strictly subnumerous to $\aleph_\alpha$ is always equal or greater than definability of being strictly subnumerous to $\aleph_\beta$ for all $ \beta >\alpha$? By 'definability' I mean the shortest defining expression of course.