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.

  • 1
    $\begingroup$ 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). $\endgroup$ – Asaf Karagila Jan 11 '14 at 17:40
  • 1
    $\begingroup$ 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? $\endgroup$ – Asaf Karagila Jan 11 '14 at 23:04
  • 1
    $\begingroup$ @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. $\endgroup$ – goblin Jan 11 '14 at 23:11
  • 1
    $\begingroup$ 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.) $\endgroup$ – Asaf Karagila Jan 11 '14 at 23:13
  • 1
    $\begingroup$ @MartinBrandenburg, thanks, I replaced the stipulation "complete" with "$V$-complete" to make it correct. What do you mean by "enlarge $\mathsf{Set}$"? $\endgroup$ – goblin Jan 12 '14 at 10:25

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.

  • $\begingroup$ Honestly, Mike's article doesn't say much about how to actually formalize a proposition. Its more about different strengths of set theory, which isn't really the crux of the question. $\endgroup$ – goblin Jan 14 '14 at 13:40

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.