Is there a metamathematical $V$? 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 encodes a lot of the important information that would have existed in the proper class 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:

*

*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.


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


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


*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.
 A: Let me offer a different perspective, informed by my recent conversion from ZFC to ETCSR, i.e. Lawvere's elementary theory of the category of sets (with replacement). Recall that the two theories are "equivalent" in that each interprets the other, and models naturally correspond; the difference between them is essentially linguistic. In ETCSR, one formalizes the category of all sets. So there is a (meta?)mathematical category of all sets $\mathrm{Set}$. I'd like to make the following analogy:
Mathematics probably starts by counting, leading to the integers $0,1,2,\ldots$. This quickly leads one to wonder how far this goes -- is there a "largest integer"? Of course, that's an obviously self-contradictory concept.
Then there was a conceptual leap in mathematics, from mere numbers to the concept of sets. We allowed ourselves to contemplate taking all the integers, forming a new kind of object, a set. Then just like Peano arithmetic formalizes the integers on some inductive idea of the formation of integers, we formalize sets in ZFC based on some inductive idea of the formation of sets. In particular, we can form larger and larger sets. But just like for the integers, it turns out that the idea of "largest set" is self-contradictory.
In the ETCSR point of view, what we do now is to make another conceptual leap in mathematics, from sets to categories. In this conception, we allow ourselves to contemplate the category of all sets, and then also "completed" categories of groups, of rings, etc. So somehow just like for the integers, the correct question was now that of "a largest integer larger than all the others", but that of collecting all the integers into a new kind of object -- a set -- the correct question here is not that of "a largest set containing all the other sets", but that of collecting all the sets in to a new kind of object -- a category.
I realize that the last 'correct' is up for debate, and that this perspective puts me on a (slippery?) slope that would ultimately want to formalize the category of all categories, ..., leading one to $\infty$-categories and homotopy type theory. Maybe that's the way to go, but for now I'd only take one step at a time.
A: Kameryn Williams has already given a very good answer, but perhaps it is worth saying explicitly that there is not 100% consensus on the exact meaning of completed infinity (or actual infinity).
Having said that, it is common practice to formalize "$\mathbb N$ is not a completed infinity" with the formal system $\mathsf{ZF} - \mathsf{Inf} + \neg\mathsf{Inf}$ (i.e., $\mathsf{ZF}$ with the axiom of infinity replaced by its negation), which is bi-interpretable with first-order Peano arithmetic $\mathsf{PA}$. With this interpretation, the answer to your question about whether it would make any mathematical difference to deny that $\mathbb{N}$ is a completed infinity is yes. Specifically, we would lose theorems that are provable in $\mathsf{ZF}$ but not provable in $\mathsf{PA}$, such as the Paris–Harrington theorem.
There are alternatives. As Kameryn Williams mentioned, Linnebo and Shapiro have argued for a novel interpretation of "$\mathbb{N}$ is only a potential infinity."  Under their interpretation, one does lose some theorems, but not quite the same ones.  There was some discussion of this point recently on the Foundations of Mathematics mailing list.
As for what it means for $V$ to be a completed whole, there is perhaps even less consensus about what that would mean.  As you suggest, one possibility is to introduce a distinction between sets and classes and to assert that $V$ is the class of all sets.  You could then point to the conservativity of $\mathsf{NBG}$ over $\mathsf{ZFC}$ as evidence that such an assertion does not prove any new theorems about sets.  However, some might argue that the assertion that $V$ is a completed whole amounts to the assertion that $V$ is the set of all sets, and that of course leads to a contradiction in a well-known way. The conclusion is that $V$ is not a completed whole. This is arguably how Cantor thought about the Absolute Infinite.
A: (taken from a comment)
To me, the idea of ordinals being a completed infinity contradicts the idea of ordinals (I mean the informal idea of ordinals, that is, that after every "completed collection" of ordinals there should be another ordinal).
A: 
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.

This is something that philosophers of mathematics—along with some mathematicians—have thought about. The basic point is, like the old Aristotelian distinction between the potential infinite versus the actual infinite, as one might apply to e.g. the integers, one can distinguish between a potentialist view of $V$ versus an actualist view of $V$. And one can argue for one position as having merits over the other.
Let me point to a couple refernces which go into more detail. For a philosophical treatment, Øystein Linnebo's "The potential hierarchy of sets" is a nice paper on the subject, arguing for a potentialist view on $V$. For a treatment of some of the mathematical issues which arise from this potentialist perspective, "The modal logic of set-theoretic potentialism and the potentialist maximality principles" by Joel David Hamkins and Linnebo is a good overview.

If that is too philosophical, the second is much more mathematical: Does this matter for formalizing mathematics?

The answer here depends on the specifics of your potentialist commitments.
To explain, let me introduce some concepts. A potentialist system is a collection of structures in a fixed language, ordered by a reflexive, transitive relation which extends the substructure relation. If we're interested in doing this for set theory, this means we want structures equipped with a membership relation. This is supposed to formalize a domain which is unfixed and growing; something may not exist in the current universe, but we can potentially expand to a larger one and find the desired object.
There's a natural interpretation of modal logic in this context. Namely, $\varphi$ is possible, $\diamondsuit \varphi$, at a universe if it is true in some extension, and $\varphi$ is necessary, $\square \varphi$, at a universe if it is true in all extensions. You can then ask what modal assertions are valid for a potentialist system, and this tells you something about the structure of the potentialist system. The above-linked paper by Hamkins and Linnebo calculates the modal validities for a variety of set-theoretic potentialist systems, and has further details/definitions.
To now explain the "it depends": Linnebo and Stewart Shapiro have a mirroring theorem which applies in certain cases; see theorem 5.4 of the Linnebo paper linked above. In short, it says that if your modal system satisfies the modal axioms S4.2, then any proofs in the modal realm correspond to proofs in a classical realm, and vice versa. (See the Hamkins–Linnebo paper for a definition of S4.2; the way I like to think about it is that expresses directedness in your potentialist system.) It's a general result, so let me illustrate with an example.
You can consider $\mathbb N$ as a completed infinited whole, but you can also approach it via this potentialist framework. Namely, you can consider the potentialist system whose worlds are $\{0,1,\ldots, k\}$ for all $k \in \mathbb N$, equipped with the appropriate restrictions of the arithmetic operations. Then, a statement $\varphi$ of number theory is true in $\mathbb N$ if and only if the modal statement $\varphi^\diamondsuit$ is true in this potentialist system. Here, $\varphi^\diamondsuit$ is the modal statement you get by replacing every $\forall$ with $\square \forall$ and every $\exists$ with $\diamondsuit \exists$. The point is, in a universe in the potentialist system you may not yet have a witness to an existential statement, but you can find one by extending to a large enough universe.
So if your potentialist take on $V$ includes S4.2, then there's an equivalent system that takes $V$ as a completed whole, so there's in the end no difference for formalizing mathematics. Maybe one system might be easier to work with than another, but you can translate results from one to another.
On the other hand, there are set-theoretic potentialist systems which don't validate S4.2, and as you extend you make permanent choices as to what is true. (For examples, see Hamkins and Hugh Woodin's "The universal finite set" and Hamkins and my "The $\Sigma_1$-definable universal finite sequence". Both of these are variants on Woodin's universal algorithm for models of arithmetic, and if you're interested in understanding them the arithmetic case is a nicer starting point. Hamkins has a nice paper about the arithmetic case.)
So if your potentialist take on $V$ is more in line with these, then it would make a difference for formalizing mathematics, since it expresses something that cannot be captured with a single universe.
To express a bit of a personal opinion: I think an S4.2 set-up is probably more plausible than the situations in the Hamkins–Woodin or Hamkins–Williams papers. In particular, both of those require nonstandard models to work, and many—most?—mathematicians are predisposed to the view that nonstandard models aren't plausible candidates for being the 'true' universe of mathematics.
A: I'd like to add a few words on a different level than the ones very well discussed in the question and the answers so far, although perhaps you've already automatically discarded it: under my dual conceptualist/formalist point of view, I'd say that conceptually speaking, okay, the question is complex, and analyzing it may go in various directions as we can see in the other answers. But well, formally speaking, and I'd take metamathematics to be formal first, there are no sets, only terms for them, and no classes, let alone proper ones, only mere (potentially recursive) enumerations of syntactic gadgets or combinations of those... And as there are way too few syntactic witnesses for every conceivable set in the multiverse, there can be no completed V in that sense; that, I guess, is the only one that 'matters for formalizing mathematics', as in your second interrogation (we could fall back on some unary predicate defining the symbol V in some language of sets or classes, but that's not really absolute, since it's dependent on the ambient theory in this language that we definitionally extend this way).
The story for N along those lines differs, since there's a formal numeral for any conceptual natural number, whenever a numeral system is fixed (all being isomorphic); and the (meta)mathematically speaking best one might be the Peano numerals, namely sequences of the symbol $s$ ending with an appended $0$ (as finally, arithmetic boils down to structural properties of such strings). And those might be collected in a grammar recursively enumerating them and only them, say in Backus-Naur Form, as follows:
$$n::=0\mid sn$$
That's the only actual completed whole of actualized natural numbers I'd see, and I think there's no real doubt of its usefulness to formalize mathematics (if only because of recursive definitions of functions, inductive proofs of universal propositions...).
