In ZFC, the axiom schemas of specification and replacement refer to "formulae in the language of set theory." Are there any canonical examples of sets which cannot be specified in this way?
Put another way, I know of many proper classes (in ZFC) which are proper because they are "too big." The class of all sets, the class of all groups, the class of all ordinals. What are some classes which are proper because they are "too complicated?"
I believe these would correspond to subsets specified by second-order predicates, but I am not very well versed in the subject and the simple examples I tried seemed to produce sets which could also be specified by some first-order sentence.
If this is one of those cases where no example can be constructed, a proof of existence would also be nice.