Easy and concise way to define the natural numbers I want to define the natural numbers, and then, based on that go to the integers, then to the rational numbers and then to the real numbers. While the last steps are relatively clear, I am not sure what a short and concise way to define the natural numbers is. After reading many answers to related questions, I think this question might be more subtle than I initially thought (see e.g. here, here, here, here, here).
After reading the linked answers my current approach would be to use first order Peano axioms, i.e.


*

*$0\in \mathbb{N}$.

*If $n \in \mathbb{N}$ then $s(n) \in \mathbb{N}$.

*There is no $n \in \mathbb{N}$ such that $s(n)=0$. 

*If $n,m \in \mathbb{N}$ and $s(n)=s(m)$ then $n=m$.

*If, for a property $P$, $P(0)$ is true and whenever $P(n)$ is true also $P(s(n))$ is true, then $P(m)$ is true for all $m \in \mathbb{N}$. 


If we define the natural numbers that way, I have the following questions (I am aware that some parts of these questions are already answered in the linked answers, but I was not yet able to connect the dots to a coherent picture):


*

*How can I prove the existence of $\mathbb{N}$? And what exactly does this mean? Is this a stronger claim than claiming that there are no contradictions within these axioms? 

*If I understand correctly, since I used the first order Peano axioms, there are non-standard models satisfying these axioms. How is non-standard defined here? What exactly is a model?

*There are several models satisfying these axioms. But is this somehow "bad"? If we prove something based on the axioms, it clearly holds for any model that satisfies the axioms, doesn't it? Can we provide a non-standard model explicitly (for every infinite cardinality) or is only the existence of non-standard models known? Are there non-standard models with the same cardinality as the standard model?

*Could these first order Peano axioms be contradictory? Can we prove that we cannot prove that they do not lead to a contradiction?

*Is there a relation to ZFC? (Since we consider the first order axioms, we do not need any set theory here, or do we?)

*Are there propositions that are undecidable in that system?

*How is the term "property" defined formally? Is the fifth Peano axiom (or axiom scheme?) a first order axiom or second order? What is intuitively the difference to the second order Peano axioms?


My main motivation is that I want to concisely define the natural numbers but still keep every step accessible to a first semester student. However, the closer I look at the topic the more I realise that there are some subtleties. Which approach would you recommend to define the natural numbers in a first semester course?  
Edit: First, thank you very much for your answers so far. It seems that complete rigour isn't easily achieved when reasoning about the natural numbers. To fully understand all the answers I need to follow the advice to learn more about logic / set theory, I will get a book. However, as the question was set on hold as it needs more focus, I would like to narrow it down to the last question in the original post: How would you introduce the natural numbers in the first semester, balancing rigour and accessability? And what are the drawbacks of the respective approach, i.e. how can the gap to a more rigorous approach be described (informally)? I hope that the question can be reopened now.
 A: Proofs don't occur in vacuum, and you cannot construct what is not there.
What you really aim to do is to fix some mathematical universe, satisfying some properties (in the case here, a universe of set theory satisfying $\sf ZFC$, but this can be any other foundational approach, more on this later) and within that universe claim that a certain object can be used to interpret the natural numbers, and that the rest of the construction can continue.
In the "standard case" that would mean that we point at a set that can be used to model the natural numbers as sets. This is the von Neumann ordinal $\omega$, that we define by stating that $\varnothing$ is the new $0$, and $S(n)$ is given by $n\cup\{n\}$.
The Axiom of Infinity, along with a few other axioms of $\sf ZFC$, guarantee that there is a smallest set containing all the natural numbers. And so we prove that there is a model to the axioms of Peano, and therefore the theory is consistent.
The standard model of Peano arithmetic is also the unique second-order model. But to talk about second-order logic it is somewhat necessary to have some notion of a "set" to begin with. Lucky for us, we're working inside set theory. So that we can verify that $\omega$, as above, is indeed a model of second-order arithmetic (here we replace the induction schema by a single second-order axiom).
Inside our universe, therefore, the standard model of arithmetic is $\omega$, or anything else isomorphic to it. There are other models, as you stated, and those are non-standard models. By Löwenheim–Skolem there are also countable non-standard models, and here countable means "inside the universe" which means that they have the same cardinality as $\omega$. Of course, there are also others, much larger.
Now, all of this happens within a given universe of set theory. But we can show that actually the process with which we did all of that is quite explicit, and the universe we chose was arbitrary, so in fact $\sf ZFC$ proves that second-order arithmetic has a model (and therefore that the first-order counterpart is consistent).
But we can also use other foundations of mathematics. We can use type theory of some sort, or category theory, or we can even use arithmetic. If we are being entirely formal, then we are just "playing with strings and inference rules", and this is something we can recursively code into the integers. So in fact we can have our foundation of mathematics as some very weak arithmetic theory. But then we can no longer talk about models as something that "exists", since models are sets, and so we can no longer guarantee the above. 
As a consequence of Gödel's incompleteness theorem, if we use $\sf PA$ as our foundation (or even weaker), then we cannot prove that the axioms of $\sf PA$ have no contradiction in them. This is subtle, since the meaning of "the axioms of $\sf PA$" has now shifted from "outside" of mathematics, to inside of mathematics, as did the rules of inference, and so on.
There are a lot of incredible difficulties and subtle points that require a lot of reading, practice, and mathematical maturity to understand in full. So I am not going to get into that.
But I can suggest that you start by reading a basic book about logic and about set theory.
A: 
How can I prove the existence of $\mathbb N$?

Strictly speaking, you can't. There's a famous theorem by Gödel that states that any consistent logical system strong enough to do arithmetic cannot prove its own consistency.
But you can prove that there's a copy of $\mathbb N$ in ZFC, right? Well, yes, but that only tells you that $\mathbb N$ exists if ZFC describes something that exists. But since ZFC is strong enough to do arithmetic (or else you could not have a model of the Peano axioms in it), you just moved the problem to showing that ZFC is consistent. Which ZFC itself cannot do either.
Moreover, deriving the existence of $\mathbb N$ from ZFC is sort of cheating, since one of the axioms of ZFC, the axiom of infinity, in essence states that $\mathbb N$ exists (actually it states that a superset of $\mathbb N$ exists). So ZFC contains the set $\mathbb N$ because we explicitly included the assumption that this set exists. If you remove the axiom of infinity, the remaining axioms cannot prove that $\mathbb N$ exists.
Note that replacing ZFC by something else doesn't really help either. Whatever you come up with, if it is strong enough to prove $\mathbb N$ exists, it cannot prove its own consistency.
Indeed, there is a small minority of mathematicians who believe that $\mathbb N$ does not exist.
However given that there's a huge body of mathematics that assumes that $\mathbb N$ exists, and no one has ever found a contradiction with that, most mathematicians are indeed confident that $\mathbb N$ indeed exists.

Is this a stronger claim than claiming that there are no contradictions within these axioms?

Indeed the existence of $\mathbb N$ is stronger than the existence of the natural numbers. In particular, the first order Peano axioms do not state that $\mathbb N$ exists. They only state that the natural numbers themselves exist, but not that there exists something that contains them all.
Moreover, you do not need the axiom of infinity to get the natural numbers in ZFC, you only need it to get the set of natural numbers, that is, $\mathbb N$.
For example, take the hereditary finite sets, that is, any sets that have finitely many elements, and all the elements are themselves hereditary finite (so you'll find no infinite set no matter how deep you go). Those fulfil all the ZFC axioms except for the axiom of infinity (obviously). You could even add an “axiom of anti-infinity” that says that there are no infinite sets.
Now you can define the von-Neumann ordinals also in those sets, and since now all sets are finite, also all von-Neumann ordinals are. And then the von-Neumann ordinals fulfill the Peano axioms. However, the hereditary finite sets do not contain the set $\mathbb N$, as that one is not finite.
A: (A partial answer)

How can I prove the existence of N?

It can be shown that in any Dedekind infinite set $X$, there exists a "copy" of the natural numbers, i.e. there exists a $N \subset X$, a function $f$ and $x_0$ such that 


*

*$x_0 \in N$

*$\forall a\in N: f(a)\in N$

*$\forall a, b \in N: [f(a)=f(b) \implies a=b]$

*$\forall a \in N: f(a)\neq x_0$

*$\forall P\subset N: [x_0 \in P \land \forall a \in P: [f(a)\in P] \implies P=N]$ (the Principle of Mathematical Induction)


Informally, $N=\{x_0, f(x_0), f(f(x_0)), \cdots \}$ where $x_0$ is the "first number" and $f$ is the "successor function" on $N$.

EDIT

Which approach would you recommend to define the natural numbers in a first semester course?

Start by simply stating Peano's Axioms. You might justify them by starting with something more verbal and self-evident:


*

*Zero is a natural number.

*Every natural number has a unique successor.

*Different natural numbers have different successors.

*Zero is the "first" natural number. It has no predecessor.

*Every natural number (except zero) can be reached by a process of repeated succession starting at zero. (This can be formally shown to be equivalent to the usual Principle of Mathematical Induction, though it is not a trivial proof for beginners. 228 lines)

A: This is adapted from the Definition by Recursion given by R.L. Goodstein in "Recursive number theory", and although provisional and exploratory, the aim here would be to think from a computational point of view to establish the existance of counting numbers.
Empirical Observation: There exist many elementary operations that can repeated, such as the operation $+1$:
For example:
$$+1$$
$$+1+1$$
$$+1+1+1$$
$$+1+1+1+1$$
$$...$$
$$+1+1+1+1...+1$$
Definition: $u$ is a variable to process a start point operation, any number of repeated operations, and an end point operation.
The process:
Let the start point operation be: Replace $u$ by $u+0$. 
Let the repeatable operation be: Replace $u$ by $u+1$.
Let the end point operation be: Replace $u$ by $+0$.
By continually incrementing by 1 the number of repeatable operations carried out from the initial start point to the end point operation, gives the following sequence of values, which we have chosen to encode in their equivalent decimal number form or the arbitary variable $n$:
$$+0+1+0\equiv1$$
$$+0+1+1+0\equiv2$$
$$+0+1+1+1+0\equiv3$$
$$+0+1+1+1+1+0\equiv4$$
$$...$$
$$+0+1+1+1+1+1...+1+0\equiv n$$
If no repeatable operations have occurred then we define
$$+0+0\equiv 0$$
If at least one repeatable operation must occur then the complete notional set of encoded decimal numbers which can be generated in this way is labeled $\mathbb{N}^*$. If a count with no reapeatable operations is also included in the notional set then it is labeled  $\mathbb{N}_0$ .    
