I read the following document: https://www.math.wustl.edu/~freiwald/310peanof.pdf . In this document, the author wants to formalize that natural numbers, that are informally thought of as a collection of $0,1,2,3,...$ (this is not really a set, is it? Meaning, something like $\{0,1,2,3,...\}$ doesnt have a formal meaning, does it?).
To formalize this idea, one has the Peano-axioms, which should intuitively be satisfied by what we think of the natural numbers. The author proceeds to construct $\mathbf{N}$ by using the axiom of infinity of ZFC and defining $\mathbf{N}:=\bigcap \{J: J \ \text{is an inductive set}\}$, where an inductive set is defined to be a set that has the properties:
$(i)$ $\emptyset \in J$
$(ii)$ if $x \in J$ then $s(x) \in J$. ($s(x)$ denotes the successor)
The set $\mathbf{N}$ as defined above indeed satisfies the Peano-axioms and one defines $0:=\emptyset,1:=\{\emptyset\},2:=\{\emptyset, \{\emptyset\}\}$ and so on. This gives that $\mathbf{N}$ indeed contains every object we consider to be a natural number. However, why can't it contain any "odd" elements, meaning elements that are not in the collection of $0,1,2,3,4,...$. Im looking for a formal way to prove this, but I am unsure if this is possible. I know that it is provable that any object $n \in \mathbf{N}$ is either $0$ or the successor of a natural number. However, I am not sure if it is formally provable from this that $\mathbf{N}$ only contains "numbers" and no other elements. Every argument I can think of is pretty hand-wavy and rather informal.
Edit: Might this be a way to do it? The object $0$ is an element in the collection $\{0,1,2,3,...\}$. Let $n$ be an object in this collection. Then also, by definition, $s(n)$ is an object in this collection, by definition of the collection (it contains the successors of the elements). I just wondered if the property "an element of the collection $\{0,1,2,3,...\}$" would be too informal to use for an induction.
What do you mean precisely by "odd element"? Essentially, the intersection of all inductive sets (or equivalently, the least inductive set with respect to $\subseteq$) is the formal definition of the set of natural numbers, hence giving a formal definition of "natural number" (i.e., "member of the least inductive set"), so by definition, there are no things in that set that are not natural numbers.
However, this question relates to non-standard models of PA / ZFC. The discussion in the preceding paragraph is all from the point of view of the universe $V$ of ZFC we are working in. If $V$ contains a smaller universe $U$ of ZFC, i.e. $U\in V$, then $U$ and $V$ might disagree about what the least inductive set is. Write $I^U$ for the least inductive set as computed in $U$, and $I^V$ for that computed in $V$. For simplicity, let's assume $I^V\subseteq I^U$ and $U$ agrees with $V$ about membership on the sets in $I^V$, so e.g., they both have the same empty set $\emptyset$, the same set $\{\emptyset\}$, the same $\{\emptyset,\{\emptyset\}\}$, etc, for all the elements of $I^V$. Now it can be that $I^V\subsetneq I^U$, and since $U$ thinks that $I^U$ is the least inductive set, it follows that $I^V\notin U$. Since $U$ thinks that $I^U$ is the least inductive set, $U$ has to think that every element of $I^U$ is either $\emptyset$ or a successor $x\cup\{x\}$. It follows that from the view of $V$, the $\in^U$-ordering (i.e. using the membership relation in $U$) of $I^U$ looks like $I^V\frown D$, where $D$ is some discrete strict linear order without endpoints (here $I^V\frown D$ denotes the ordering where $I^V$ is first, followed above by $D$). So $D$ indeed contains "odd" elements from the point of view of $V$, but $U$ disagrees, and thinks that these elements are true natural numbers. In $U$, the "cut" $I^V$ cannot be seen (as $I^V\notin U$), so there is no (obvious) contradiction. (The model $U$ is a non-standard model of ZFC.)
Working in our universe $V$ of ZFC, assuming $V$ thinks ZFC is consistent, these sorts of models $U$ can be formed by using the compactness theorem applied to the theory ZFC + T, where T uses constant symbols $n$ for each $n\in\mathbb{N}$, plus one further constant symbol $x$, and contains the formulas "$x$ is a natural number" and "$n<x$", for each natural number $n$. (One needs a little more thought to arrange the condition that $I^V\subseteq I^U$ and they agree about membership there.)