This question might be extremely naïve for which I apologise in advance.
The induction principle can be stated as:
If $A ⊂ ℕ$ such that
- $1 ∈ A$, and
- $ν(A) ⊂ A$ (where $ν\colon ℕ → ℕ$ is the successor function),
then $A = ℕ$.
It can be proven as follows:
If $ℕ\setminus A$ was non-empty, it would have a least element (which again can be proven from the axiom of regularity using a set-theoretic definition of naturals and using contradiction), say $x ∈ ℕ\setminus A$: By 1.) $x ≠ 1$, so there is a $y ∈ ℕ$ with $x = ν(y)$. By assumption, $y ∈ A$, and by 2.) $x = ν(y) ∈ A$ which cannot be.
This proof uses contradiction. But it is, of course, assuming (other) axioms from ZF.
But how is this handled with intuitionistic logic where contradiction isn’t allowed? Is induction an axiom on its own?
The answer depends on the formal system you are working in. Here are some examples - and indeed, as you speculated it might be the case, in all of them we have induction directly built into the axiomatics or the definition of ${\mathbb N}$:
In Constructive Set Theory like Intuitionistic Zermelo Fraenkel (IZF) you need to find a replacement for the Axiom of Foundation since it implies the Law of Excluded Middle (for a proposition $\phi$, consider a $\in$-minimal element of $\{\emptyset\ |\ \phi\}\cup\{\{\emptyset\}\}$). The (classically equivalent) alternative one uses is the following:
$$ \text{(Law of Set Induction):}\quad\quad\forall x ((\forall y\in x: A(y))\Rightarrow A(x))\Rightarrow \forall z: A(z)$$
Thus, inductive proofs of statements parametrized over ${\mathbb N}$ are realized directly through the axiomatics.
In topos theory, which one can also view of an intuitionistic foundation of mathematics, one uses the notion of a natural number object, which is by definition the initial pointed object with an endomorphism. Hence, it is the definition of ${\mathbb N}$ there that maps with domain ${\mathbb N}$ are constructed inductively.
In type theory, ${\mathbb N}$ is an example of an inductive type which usually comes directly with the corresponding induction scheme.
In System F, for example, the natural numbers could be implemented as the polymorphic type ${\mathbb N}:\equiv\forall X: X \to (X\to X)\to X$ which reads as: An element of ${\mathbb N}$ is a uniform procedure to associate to any type $X$, any element $x_0:X$ and any rule $X\to X$ an element of $X$. Indeed it turns out that these are, up to normalization, the Church presentations $\lambda X.\lambda (x_0:X) (f:X\to X). f(f(...(f(x))...))$ of the naturals.
In Coq the definition of an inductive type such as
automatically results in the implementation of induction schemes such as
allowing the 'inductive' construction of a proof of $\forall n\in{\mathbb N}: P(n)$ out of a proof of $P(0)$ and a rule turning a proof of $P(n)$ into a proof of $P(n+1)$.