I know that, from compactness theorem, one can prove that there are models of first order arithmetic in which there is some "number" which is not a successor of zero, in the sense that it is strictly bigger than any successor of zero (i.e. any element of the model obtained by applying the successor function to zero finitely many times). 


From the axiom of infinity, it follows that every model of ZFC must contain an element which one can think of as "the natural numbers", in the sense that it is a model of Peano Axioms. Peano Axioms are a second-order theory, since the principle of induction is a second order axiom, and from the principle of induction it follows that the Peano Axioms have a unique model in ZFC, so that we can call this model among the others of first-order arithmetic, the "standard" model of arithmetic.


But picking one model of ZFC, how do we know what's really inside its standard model of arithmetic? How do we know there is nothing else than the successors of zero? After all, every model of ZFC thinks that his natural numbers are the standard ones, so one can use compactness to produce a model of ZFC which has non-standard natural numbers from an external point of view, and in which there will be a standard natural numbers object containing elements bigger than any successor of zero. 


So, if one wants to do mathematics inside a model of a first order theory of sets, how can one know that he is able to pick a model in which the natural numbers are not non-standard?



Existence of a model of ZFC in which the natural numbers are really the natural numbers
This, in fact, cannot be proven, even in $ZFC+Con(ZFC)$. This is because $ZFC$ proves the following statement:



> 
> If we have a model $M$ of $ZFC$ whose natural numbers are standard, then $M$ satisfies $ZFC+Con(ZFC)$.
> 
> 
> 


Indeed, $Con(ZFC)$ is an arithmetic statement. Since we are assuming that $ZFC$ has a model $M$, and hence that $ZFC$ is consistent, $\mathbb N\vDash Con(ZFC)$, and since $\mathbb N^M\cong\mathbb N$, $\mathbb N^M\vDash Con(ZFC)$, and hence $M\vDash Con(ZFC)$.


Now if $ZFC$ could prove "if there is a model of $ZFC$, then there is a model of $ZFC$ with standard $\mathbb N$", then we would get that $ZFC+Con(ZFC)$ proves that $ZFC+Con(ZFC)$ has a model, contradicting Godel's second incompleteness theorem.


Therefore, we cannot conclude, from existence of a model, existence of a model with standard $\mathbb N$.




---


Thought it might be worth mentioning that this reasoning is under the assumption that $ZFC+Con(ZFC)$ is consistent. In the other case, $ZFC$ proves that $ZFC$ has no models, so the implication I discuss holds vacuously.




---


Will Sawin asks whether existence of a model of $ZFC$ with standard $\mathbb N$ (apparently called $\omega$-models, as Gro-Tsen's comment to the question notes) is equivalent to ZFC being arithmetically sound. The answer is negative (of course, again, under blanket consistency assumptions).


The idea is very similar. Suppose $ZFC$ is arithmetically sound, and that there is an $\omega$-model $M$ of $ZFC$. We claim $M$ satisfies "$ZFC$ is arithmetically sound". If we show that then we're done, since "$ZFC$ is arithmetically sound" cannot prove $Con$("$ZFC$ is arithmetically sound").


Arithmetic soundness is equivalent to "for all $n$, $ZFC$ is $\Sigma^0\_n$-sound, and $\Sigma^0\_n$-soundness is an arithmetic statement for each $n$. Since $M$ has standard $\mathbb N$, $\Sigma^0\_n$-soundness holds in $M$ as well. Now we use standardness of $M$'s $\mathbb N$ again, to observe that $\Sigma^0\_n$-soundness in $M$ for all $n$ in (external) $\mathbb N$ is equivalent to arithmetic soundness internally in $M$.


As you can see, existence of an $\omega$-model is a fairly strong property, much stronger than any consistency or soundness assumption.


