As with many of you, I've been following Peter Scholze's recent question about universes with great interest. In ring theory, we don't often have to deal with proper classes, but they occasionally pop their heads. For instance, one cannot take the product of all countable rings---but one can replace that proper class with the set of isomorphism types of countable rings and get something that "would have been" isomorphic to that product (if it existed). I've similarly viewed the axiom of universes as an elegent way to avoid Russell's paradox when wanting to talk about something "close" to the proper class of all rings, groups, sets, etc.; the discussion at Peter Scholze's question has been very enlightening in that regard.

This brings to mind a related question I've been struggling with for quite a while. I view ZFC as a formalization of those mathematical techniques that I take for granted when working with collections. As I've delved deeper into first order logic, and formal languages, the importance (in my mind) of metamathematical assumptions has increased. One of the questions that I'm told was historically important was whether or not there was a "completed" infinity, or in other words whether or not the natural numbers actually form a completed whole collection.

I'd say that modern mathematics comes down strongly on the side of a completed infinity. In particular, I've understood that the axiom of infinity in ZFC is supposed to reflect a similar metamathematical assumption. One does not think of the axiom of infinity merely as a formal rule, interpretable in a finitistic sense (even if, technically, it could be). On a more concrete level, I'd guess most mathematicians think of questions about the infinite behavior of Turing machines as actually having answers (metamathematically and/or Platonically).

(This is not to dismiss those who prefer to think of the natural numbers as an uncompleted collection. These issues definitely raise interesting philosophical question as well as mathematical questions, such as how much these metamathematical assumptions affect standard mathematics.)

So, my first question is whether or not, metamathematically speaking, we should take $V$ (the proper class of all sets) as a completed whole or not. If that is too philosophical, the second is much more mathematical: Does this matter for formalizing mathematics? If not, does taking $\mathbb{N}$ as a completed whole matter for formalizing/doing mathematics, or can we easily do without that assumption?

If we believe $\mathbb{N}$ exists as a completed whole, and work by analogy, then the answer to the first question seems to be obviously yes. But if we take Russell's paradox at face value, then the answer seems to be obviously no.

Moreover, the different standard options available to formalize mathematics seems to leave this question open-ended:

1. A ZFC-formalist might say no, there is no meta-$V$ because there are not even any formal proper classes, they are just an elegant informal way to talk about uncompleted infinities.

2. An NBG-formalist might say yes, and our meta-$V$ is only somewhat like sets.

3. An MK-formalist might say yes, and our meta-$V$ is really nearly a set.

4. A believer in ZFC+Universes, might say yes or no. Yes, if we think of our meta-$V$ varying as we change our universe of expression, but maybe no if we want it to have all the properties of being the full (meta-)universe (on pain of Russell's paradox).

The reason I'm asking this question is that I would guess most mathematicians would say something like "No, it doesn't matter whether or not we take $V$ as meta-mathematically existing." But I'd guess those same mathematicians would say that it does matter that we take $\mathbb{N}$ as meta-mathematically existing, else we can't even begin to formalize how to construct a (completed) language, etc.