# How best to formalize propositions suffering from “size issues”?

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.

• Every model of $\sf ZFC_2$ is necessarily $V_\kappa$ for an inaccessible $\kappa$, if you don't want to get into large cardinals then perhaps it's best to avoid them here as well; if you do then you probably want to formalize this statement in $\sf ZFC$ augmented by some large cardinals axiom (e.g. there is a proper class of inaccessible cardinals, also knowns as the universes axiom). – Asaf Karagila Jan 11 '14 at 17:40
• Honestly, you've edited this eight times in just under six hours. Perhaps it's worth to take your time a little while longer before clicking the "Post" button? – Asaf Karagila Jan 11 '14 at 23:04
• @AsafKaragila ah sorry, when I'm excited about a question I tend to check back on it kind of frequently, reread it etc. and end up tinkering with it a lot. I should probably be a bit more conscientious about this kind of thing. – goblin Jan 11 '14 at 23:11
• Then perhaps tinker with it on a separate page, not on this site. Sleep on it, and then make just one edit instead? I can understand you, I'm just sharing my process when asking a question. (This is probably why I don't ask many questions, I let them sit for a day or two, and then I often come up with the answer on my own. And if not, then I have a good enough preliminary version.) – Asaf Karagila Jan 11 '14 at 23:13
• @MartinBrandenburg, thanks, I replaced the stipulation "complete" with "$V$-complete" to make it correct. What do you mean by "enlarge $\mathsf{Set}$"? – goblin Jan 12 '14 at 10:25