La respuesta depende del sistema formal en la que trabaja. Aquí están algunos ejemplos - y de hecho, como se especuló que podría ser el caso, en todas ellas hemos de inducción integrada directamente en el axiomatics o la definición de ${\mathbb N}$:
En Constructivo de la Teoría de conjuntos como Intuitionistic Zermelo Fraenkel (IZF) que usted necesita para encontrar un reemplazo para el Axioma de Fundación ya que implica la Ley de Medio Excluido (para una proposición $\phi$, considere la posibilidad de una $\in$-el mínimo elemento de $\{\emptyset\ |\ \phi\}\cup\{\{\emptyset\}\}$). El (clásico equivalente) una alternativa utiliza es la siguiente:
$$ \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 \(X\X)\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\a 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))...))$ de los naturales.
En Coq la definición de un tipo inductivo, tales como
Inductive Nat :=
| O : Nat
| succ : Nat -> Nat.
automáticamente los resultados en la aplicación de la inducción de esquemas tales como
Nat_ind: forall P : Nat -> Prop, P O -> (forall n : Nat, P n -> P (succ n)) -> forall n : Nat, P n
permitiendo que el "inductivo" construcción de una prueba de $\forall n\in{\mathbb N}: P(n)$ fuera de una prueba de $P(0)$ y una regla de giro de una prueba de $P(n)$ en una prueba de $P(n+1)$.
