Suppose we want to formalize a proposition (say, from category theory or model theory) that has "size" issues. For concreteness, lets take the following statement as a fairly typical example.
Proposition. The functor category $[\mathrm{Grp}, \;\mathrm{Set}]$ is complete.
If our chosen foundational theory is ZFC, then we might be tempted to formalize the above proposition as follows.
First-order Formalization. For every model $V$ of ZFC, the functor category $[\mathrm{Grp}.\!V, \mathrm{Set}.\!V]$ is $V$-complete.
(If the meaning of the above notation isn't clear, please comment.) However, there's another way to formalize the proposition of interest, in which we restrict to second order models.
Second-order Formalization. For every model $V$ of second-order ZFC, the functor category $[\mathrm{Grp}.\!V, \mathrm{Set}.\!V]$ is $V$-complete.
Note that even if we use something stronger than ZFC, the issue doesn't go away. For example, suppose we've chosen Tarski-Grothendieck set theory (TG) as our foundational theory. Well there are both first and second order versions of TG, thus there are two different ways of formalizing the proposition of interest with respect to TG. Thus, my question is:
Question. In general, which is the "correct" formalization of the original proposition? The first order version, or the second order version? And does it even matter?
Furthermore, if there is a "third way" that outperforms the aforementioned approaches to formalizing the proposition, I'd like to know.
I don't think there's any one best answer to your question, but the topic is considered in great detail in Mike Shulman's Set Theory for Category Theory.