Based on the feedback of the past week, I've gone ahead and created a tag (following Monroe Eskew's suggestion of "higher-order-logics" instead of "second-order-logic"). I've kept the tag description very short, and others should feel free to improve it. I'll add this tag to relevant questions ov...

I forgot to mention originally: this was motivated by this old MSE question. It's not hard to show in $\mathsf{ZFC}$ that there are nontrivial elementary embeddings from $(Ord; \in)$ to itself - or rather, it's not hard to write down specific formulas which $\mathsf{ZFC}$ proves define such maps....