Natural numbers in Set Theory We seem to accept the fact $(\omega,+,\times,<,0,1)^{V}$, where $V:=x=x$ is the set theoretic universe, properly reflects what is intuitively understood to be the set of natural numbers, i.e. we seem to accept that given any element $n\in{\omega}$, there is some  meta-mathematical finite number $m$ (which properly reflects what it means to be finite) s.t. $n$ is obtained as the $m^{\text{th}}$ successor of $0$. Why is this the case?
I realize that you cannot state the above requirement in a coherent way using sentences in set theory. But we do seem to accept the above fact as a given. I asked a similar question as a part of an other question Meta Theory when studying Set Theory The answer given there; "we often take the universe to have the same integers as the metatheory" by which I assumed that it was an implicit assumption that $(\omega,+,\times,<,0,1)^{V}$ actually reflects natural numbers in the above, makes sense. But my question is: Why are we so sure that this is the case? 
 A: We understand $\omega$ as a model for the natural numbers because it satisfies the categorical second-order theory of $\sf PA$. So if we understand "the natural numbers" as the unique (up to isomorphism) model of $\sf PA_2$, this means that indeed $\omega$ is this model.
So working internally to $V$, this has to be the case. However, it is possible to have a model of $\sf ZFC$ which disagrees on its integers with its meta-theory. Still, internally, $\sf ZFC$ proves the induction schema, so even if $V$ has non-standard integers, it still thinks they can be generated by applying the successor to $\varnothing$ finitely many times.
This means that when $V$ and the meta-theory disagree on the notion of finite we have a bit of a trouble when translating induction on formulas in the meta-theory, to induction on the integers internally. So we assume this is not the case. Why can we even assume that? Well, we can't really assume that. Even if our meta-theory is $\sf ZFC$, the existence of a model which agrees with the universe of the integers is a stronger assumption than just assuming there is a model of $\sf ZFC$.
But set theory, and mathematics in general, is a utilitarian science. If the assumption is useful, and it's not "horrible" then we are likely to assume it. Since we often work with much stronger things (like transitive models, large cardinals, etc.) assuming that the universe and its meta-theory agree on the integers is not a big deal.
It should be noted that often we don't need that, and we don't care for that. If we just fix some universe of set theory in order to develop classical analysis, say, then we can forget about the meta-theory completely and just prove everything internally to the model. The need for this interaction comes up mostly when we talk about set theory itself.
And that we do, as I said, often under much stronger assumptions in consistency strength. If you have large cardinals in the universe, and the meta theory doesn't agree with the universe somehow, work internally to the universe, using some model which agrees with the universe on the integers (and much more if you want). So suddenly, this assumption is not that horrible. It's quite innocent. So we make it.

(As promised, a summary on how to prove that $\omega$ satisfies $\sf PA_2$.)
In order to say that $\omega$ satisfies $\sf PA_2$ we need to be able and say that given a statement in the language of second-order arithmetic, whether or not it is true in $\omega$. However in the universe of set theory, talking about subsets and predicates over $\omega$ is all very tangible.
So we need to encode the language, for this we need symbols for first- and second-order variables (so we fix two disjoint countable sets for that) and we fix symbols for addition, multiplication, $0$, $1$ and $\leq$ (we may as well use the actual sets which are these objects, but it doesn't matter).
The rules for forming a formula are the same as in first-order logic, only we are allowed to quantify over second-order variable as well, and write $x\in A$ when $x$ is a first-order variable and $A$ is a second-order variable.
An assignment now is a function assigning first-order variables natural numbers, and second-order variables sets of natural numbers. Since we are talking about full semantics, we are allowed to use any set in the universe.
If $\sigma$ is an assignment and $\varphi(x_1,\ldots,x_n,A_1,\ldots,A_k)$ is a formula (where $x_i$ are first-order and $A_j$ are second-order variables), then we say that $\omega\models_\sigma\varphi(\ldots)$ by recursion exactly as we define the satisfaction for first-order logic.

*

*If $\varphi$ is atomic, then it is of the form $x\in A$ or some term $x+y\leq z$ or something similar to that. It is true if $\sigma(x)\in\sigma(A)$, etc.


*If $\varphi$ is a conjunction/disjunction/material implication/negation, we simply apply the truth function on the smaller formula, using the induction hypothesis.


*If $\varphi$ is $\forall x\psi$ where $x$ is a first-order variable, then $\omega\models_\sigma\varphi$ if and only if for every $n\in\omega$, $\omega\models_{\sigma[x/n]}\psi$ where we assign $n$ to the now-free variable $x$; similarly for $\exists x\psi$.
If $\varphi$ is $\forall A\psi$ where $A$ is a second-order variable, then $\omega\models_\sigma\varphi$ if and only if for every $M\subseteq\omega$, $\omega\models_{\sigma[A/M]}\psi$ where we assign the second-order variable the value $M$. Similarly for existential quantifiers.
All in all, this is exactly what we think it should be. No funky business going on. I should remark that there are variants of second-order logic where we take a limited range of subsets. For example Henkin semantics only allows us to assign to second-order variables sets which are first-order definable. This significantly weakens the logic. But here we talk about full semantics, so everything is a fair game.
Now from the induction theorem in $\sf ZF$ we have, in fact, a formula $\sf Sat_2$ which takes in an encoding of a formula, and an assignment and returns whether or not the formula is true or false in $\omega$.
So now, given that $\sf PA_2$ is in fact finite, we can ask whether or not the conjunction of all the axioms hold in $\omega$. It is not hard to verify all the first-order axioms are true; the second-order induction axiom is true simply because the definition of "inductive set" is the same in the context of $\sf PA_2$ in $\omega$ and in the full universe (since they agree on the successor and $0$).
Since $\sf ZF$ proves that $\omega$ is in fact the smallest inductive set, it follows that every subset of $\omega$ which is inductive, is in fact $\omega$ itself. So the second-order induction axiom holds as well. Therefore $\omega\models\sf PA_2$, as wanted.
A: The question asks why we assume that the natural numbers of the metatheory are the natural numbers of some model of ZFC. Of course there are nonstandard models of ZFC, so we can only hope that some "standard" models will have this property. In general, a model that has the same natural numbers as the metatheory is called an $\omega$-model.
First, three caveats: 


*

*Nothing that we can prove within ZFC can justify this. It would be naively possible that ZFC is consistent but not $\omega$-consistent (and thus has no $\omega$-model), and in that case we could still prove all the same things in ZFC.

*We have to firmly distinguish between the $\omega$ of the metatheory and the $\omega$ of each model of ZFC. Unfortunately, there is no established notation to keep these very clear. 

*Much of the answer depends on how one views the metatheory. 
There are at least two justifications for thinking ZFC has an $\omega$-model.


*

*There is a famous interpretation of ZFC in terms of the cumulative hierarchy. This interpretation claims that if the cumulative hierarchy is developed in the metatheory, it will satisfy ZFC. Thus, this interpretation suggests that ZFC has an $\omega$-model.

*Optimism. Set theorists feel as if they know ZFC relatively well, and that ZFC captures the "real" notion of set. This is a pragmatic argument, of course. 
On the other hand:


*

*We know that the statement "ZFC is consistent" does not imply "ZFC has an $\omega$-model" within ZFC. So we cannot hope to use the mere consistency of ZFC to prove within ZFC that it has an $\omega$-model.

*Recent work of Joel David Hamkins, colleagues, and others on multiverse set theory shows that is it also perfectly consistent to assume in a multiverse metatheory that ZFC has no $\omega$-model at all. The show that, if ZFC is consistent, then it is consistent that there is a multiverse of models of set theory in which every model is non-well-founded relative to some other model. In a multiverse like that, there is no $\omega$-model of set theory, since $\omega$ (assuming it it well defined, in this context) has to be well founded.
