To define nonstandard models of Peano arithmetic or set theory, many articles use enumerations like $x>0, x>1, \dots$ where $x$ is said to be a nonstandard natural number, ie a number that is finite from the PA model's point of view, but infinite from outside.
I find those enumerations confusing, especially when trying to construct a subtle notion such as a finite infinity. What kind of infinity is hidden in the dots "$\dots$" ? Some articles acknowledge the problem, and quickly offer to repair it by the compactness theorem. Then they consider a theory starting with the Peano axioms and adding a new constant symbol $c$, with axioms $c>0, c>1, \dots$ And that's even more confusing.
So far, the best definition I found of a nonstandard PA model is a structure $(M,0,S,+,\times,\leq)$ that satisfies the Peano axioms, and such as the order $\leq$ on $M$ is not a well-order. It may be more abstract than an enumeration "$\dots$", but I think it has the merit of being precise.
Is there a similar definition of a nonstandard model of ZF, not using enumerations or "intuitive" natural numbers ? It's more difficult because it concerns a model of PA inside a model of ZF. I don't manage to access the inner PA order $\leq$ from the ambiant logic.
Best Answer
The problem is that being standard or non-standard is in relation to your meta-theory.
Suppose that $M$ is a non-standard model of $\sf ZFC$, say with uncountably many "finite ordinals". Then the natural numbers of $M$ is a non-standard model of $\sf PA$. But as far as $M$ is concerned, it is the standard model of $\sf PA$. Or, it might be that $N$ is a standard model of $\sf ZFC$ inside $M$, but it is certainly not going to be a standard model outside of $M$ because we know that the natural numbers of $M$ and $N$ are ill-founded.
This is why you need to resort to that "$...$" that you dislike. Because you're appealing to the meta-theory's integers. The simplest way to formalize this is by saying that there exists an $x$ such that $x$ is not a numeral, where a numeral is a constant term in the language of arithmetic which is obtained by iterative application of the successor function symbol to the $0$ symbol.
Now, as for a non-standard model of $\sf ZFC$, yes there is such a thing. But first you need to learn that the term "standard model" is different in set theory and in arithmetic. In set theory it simply means that the model's $\in$-relation is the meta-theory's one. Usually we require that the model is also transitive, but $\in$ is a well-founded and extensional relation, so by the Mostowski collapse lemma a standard model is isomorphic to a transitive model, and often the two are used interchangeably.
A non-standard model, therefore, is one whose $\in$ is not the real $\in$. Or rather, not isomorphic to a standard model. In other words, it is a model of $\sf ZFC$, $(M,E)$ such that $E$ is not a well-founded relation on $M$. The axiom of regularity, however, does tell us that it is internally well-founded. There is no set in $M$ which is a counterexample to well-foundedness.
There are two additional points here:
It is possible that there are models of $\sf ZFC$ which are not standard models, but their $\omega$ is in fact standard. These are called $\omega$-models.
The consistency of "There is a standard model" or even "there is an $\omega$-model" is greater than that of "there is a model of $\sf ZFC$", specifically because an $\omega$-model (and thus a standard model too) agree with the universe on things like consistency statement. So if there is an $\omega$-model, it must satisfy $\operatorname{Con}\sf (ZFC)$, which is something that $\sf ZFC$ by itself cannot prove.