Axiom to exclude nonstandard natural numbers In Peano Arithmetic, the induction axiom states that there is no proper subset of the natural numbers that contains 0 and is closed under the successor function. This is intended to rule out the possibility of extra natural numbers beyond the familiar ones. It doesn't accomplish that goal; there remains the possibility that other natural numbers exist and the familiar ones do not form a set. In Internal Set Theory (IST), which is an extension of ZFC that is consistent relative to ZFC, there is a distinction between standard and nonstandard sets, and it can be shown that
(1) 0 is standard;
(2) if $n \in \mathbb{N}$ is standard, then so is its successor;
(3) $\mathbb{N}$ has nonstandard elements.
The induction axiom is not violated because the standard natural numbers do not form a set.
Is there a way to axiomatize set theory so that no such nonstandard natural numbers can exist?
(Note: this question is not about nonstandard models of arithmetic. In IST, $\mathbb{N}$ is a standard set, and within a given model of IST, all models of second-order Peano arithmetic are isomorphic to $\mathbb{N}$.)
 A: As long as you axiomatize set theory in first-order logic, the answer to your question is no.  The axioms would be consistent with each finite subset of the following set of sentences involving a new constant symbol $c$: "$c$ is a natural number" and "$c\neq n$" for each  (standard name of a) natural number $n$.  By compactness, there would be a model of the axioms plus all of these sentences, and in that model $c$ would denote a nonstandard natural number.
On the other hand, if you're willing to go beyond first-order logic, then the answer to your question is yes.  For example, in second-order logic, you can express the induction axiom as a single sentence and be confident that "set" really means arbitrary set (not "internal set" or anything like that).  In other words, once you're sure that "set" has its intended meaning, the induction principle guarantees that "natural number" also has its intended meaning.  (To me, this doesn't look very helpful, since the intended meaning of "set" seems more complicated than the intended meaning of "natural number".) 
For another example, if you're willing to use infinitary logic, then you can formulate the axiom "every natural number is equal to 0 or to 1 or to 2 or to 3, or ..."  
A: By Gödel's incompleteness theorem, there can't be any such axiom in a first-order, recursively enumerable theory.
You can axiomatize $\mathbb N$ by adding an infinitary rule of inference, the Hilbert $\omega$-rule:
$$P(0)\wedge P(1) \wedge P(2) \wedge \cdots \over \forall n P(n)$$
to PA for each arithmetic predicate P.  This says, if predicate P holds for each of the natural numbers (0,1,2...) then you can deduce the formula $\forall n P(n)$.  The resulting system is called  ω-logic.  
Obviously this is something of a "cheat" since you no longer have an effective theory.  As one example (maybe there are better ones) of how it can be used, Michael Rathjen's article "The Art of Ordinal Analysis" describes using the $\omega$-rule to analyze stronger and stronger arithmetic theories, and is pretty interesting.
