Natural numbers
Framework
We can set up ${\mathbb N}$ via Peano axioms. In this case induction is a seperate (schema) of axioms.
If one has a notion of the set/type of Rational numbers ${\mathbb Q}$, one may consider
definiendum | $ {\mathbb N}$ |
inclusion | $ {\mathbb N}\subseteq {\mathbb Q}$ |
postulate | $ 0\in{\mathbb N}$ |
for all | $ n\in{\mathbb N}$ |
postulate | $ (n+1)\in{\mathbb N} $ |
postulate | $ n = 0\ \lor\ \exists (k\in{\mathbb N}).\ n = k+1 $ |
Discussion
In logic, the natural numbers $0,1,2,\dots$ can be categorically (uniquely up to isomorphism) captured via the Peano axioms written down in second order logic. Many different set theoretical models for this infinite collection exists, and it's denoted by
${\mathbb N}\equiv\{0,1,2,\dots\}$.
E.g. they can be models using the first infinite von Neumann ordinal
$\omega_{\mathcal N}=\{\emptyset,\ \ \{\emptyset,\{\emptyset\}\},\ \ \{\emptyset,\{\emptyset\},\{\{\emptyset,\{\emptyset\}\}\},\dots\}$,
where $0\equiv\emptyset$ the successor of any $n$ is given by $n\cup\{n\}$.
The model is pretty much irrelevant. What one really want is any infinite set for which any member is either a singled out element “$0$” or the value of a function “$\mathrm{succ}:{\mathbb N}\to{\mathbb N}\setminus\{0\}$”, which must be a computable injection.
Note
Smallest proper math proposition for which nobody knows the answer:
$∀a. ∃b. ∀x. ∀y. (a+b)·(a+b) \neq SS((SSx)·(SSy))$
Roughly: “Are there infinitely many primes of the form $c^2-2$ for some $c\in\mathbb N$?” ($c=a+b$),
were “prime” is being captured as not being of the form $X\cdot Y$ (for some $X:=x+2\ge 2$ and $Y:=y+2\ge 2$).
Towards arithmetic
Using the set of natural numbers, one can use the successor operation to recursively declare arithmetic operations, see Arithmetic structure of natural numbers. Algebraically speaking, the natural numbers together with addition and multiplication form a commutative semiring.
Predicates
Let $a,b,c\in\mathbb N$
predicate | $ a\ \mathrm{divides}\ c\equiv a\mid c\equiv\exists b.\ a\cdot b=c $ |
Reference
Wikipedia: Peano axioms, Natural number