Incompleteness and nonstandard models of arithmetic The following are a collection of doubts, some of which shall have concrete answers while others may have not. Any kind of help will be welcome.
Reading Peter Smith's "Gödel Without (Too Many) Tears", particularly where he gives a nonstandard model of Q, I began wondering if the reason for the existence of nonstandard models of arithmetic has anything to do with incompleteness theorems.
I do not know if categoricity implies completeness (in the sense of every sentence being decidable by proof), but anyway, it seems reasonable, when one is formalizing a given (informal) theory, to try to "force" somehow the formal theory to talk "almost exclusively" about the intended interpretation. So I started thinking if some axiom (or axiom schema) could be added to PA in order to forbid its most obvious nonstandard models.
The first idea in this line was: ok, we have our class of terms 0, S0, SS0, etc. So, if we found a way to tell that for every x there is some term to which it is equal, we would be done.
But then I realized that our terms are defined inductively and that we are making implicitly the assumption: “and nothing else is a term”, very similar to the desired “and nothing else is a number” we would like to add to PA. This thought sort of worried me: every metatheoretic concept (terms, formulas, and even proofs!) is based on assumptions like these! (I have not still found a way out of these worries).
Leaving that apart. What if we move on to a stronger theory (with different axioms, but with an extension by definitions that proves every axiom of PA), for example ZFC? Natural numbers become then 0 (the empty set) plus the von Neumann ordinals (obtained by Pair and Union) that contain no limit ordinal. The set of natural numbers is obtained from Infinity, just selecting them by Comprehension. Kunen says in page 23 of his “The Foundations of Mathematics” that the circularity in the informal definition of natural number is broken “by formalizing the properties of the order relation on omega”. Could nonstandard models survive this formalization?
Well, I think I've read somewhere that being omega is absolute, so forcing would not be a way to obtain such nonstandard models. Also, I am not sure if (the extension by definitions from) ZFC set theory is a conservative extension of PA, but then it would not be able to prove anything about natural numbers (expressible in the language of arithmetic) that PA alone cannot prove. So somehow it looks like nonstandard models must manage to survive! Maybe due to the notion of being a subset of a given set not being particularly clear (although it looks like it should not be problematic with hereditarily finite sets).
Thank you in advance.
 A: That's the blue pill. Forgive me if I can't resist mentioning the red pill. 
One way out is (constructive) Church's Thesis, from which it follows there are no nonstandard models of first-order arithmetic. 
http://www.jstor.org/pss/2274603
http://en.wikipedia.org/wiki/Extended_Church%27s_thesis
A: Lowenheim-Skolem holds for first-order languages.  If you replace the induction axiom schema of first-order PA with a sentence quantifying over properties you get second-order PA.  Second-order PA is categorical but incomplete.
A: Unfortunately, nonstandard models will survive any such attempt. This is guaranteed by the Löwenheim-Skolem Theorem which says that if a countable first-order theory T has an infinite model then it has one of every infinite cardinality. Since an uncountable model necessarily has nonstandard elements, this guarantees that there is a nonstandard model of T (and even countable ones).
Actually, in your case you need a "two-cardinal" version of Löwenheim-Skolem. In your ZFC example, you move to a theory which interprets arithmetic inside a definable substructure (the set ω). The definable substructure of such a model which might still be countable even if the model itself is uncountable. Nevertheless, one can still blow up the size of the natural number substructure via the ultrapower construction, for example.
To evade the Löwenheim-Skolem Theorem, one has to move beyond first-order logic. For example, in infinitary logic one allows infinite disjunctions such as
$$\forall x(x = 0 \lor x = S0 \lor x = SS0 \lor \cdots)$$
which ensures that the model is standard. Also, second-order allows quantification over arbitrary sets under the standard interpretation, which again prohibits non-standard models. (See this related question.) This is the characterization of N most commonly used by working mathematicians.
A: I think Francois Dorais has done a good job of answering your questions as stated, but let me add some comments that may get at the issues that may be worrying you under the surface.  Many people I've met seem to view nonstandard models as demonstrating some kind of "flaw" in the set of axioms.  They seem to have some kind of tacit expectation that the purpose of writing down the first-order axioms of Peano Arithmetic is to single out the natural numbers from among all other mathematical structures.  But this is not the purpose of writing down the first-order axioms of Peano Arithmetic.  If you want to single out the natural numbers, then you should proceed in the normal mathematical manner: Say what it means for two structures to be isomorphic, and prove that the natural numbers are unique up to isomorphism.
First-order logic is weak.  We say that two structures are elementarily equivalent if they satisfy exactly the same set of first-order sentences.  It is the norm, rather than the exception, for there to exist non-isomorphic structures that are elementarily equivalent.  In the case of the natural numbers, the set of first-order sentences satisfied by the natural numbers is usually denoted $Th(\mathbb{N})$.  This is an extremely rich set of statements about the natural numbers.  (Incompleteness is tangentially relevant here, because for any sentence $S$ in the first-order language of arithmetic, either $S$ or its negation is in $Th(\mathbb{N})$, so incompleteness tells us that we can never hope to capture $Th(\mathbb{N})$ with a recursive set of axioms.)  Nevertheless, there are plenty of nonstandard models that are elementarily equivalent to $\mathbb{N}$ (i.e., satisfy all the sentences in $Th(\mathbb{N})$.
There are lots of reasons to study first-order languages, but hoping to use elementary equivalence to capture isomorphism is not one of them.  The existence of non-isomorphic elementarily equivalent structures does not demonstrate any kind of "flaw" with first-order logic, any more than the existence of non-diffeomorphic but topologically homeomorphic manifolds demonstrates any kind of flaw with the axioms for a topological space.
