There exist models of the natural numbers which include infinite numbers. Such models are called non-standard models of arithmetic. Just like the standard model $\mathbb{N}$, the non-standard models satisfy the induction axiom for formulas, although in this case only for forumlas expressible in the first-order language of Peano arithmetic.
The proof of this fact is usually given as: there exist models of Peano arithmetic satisfying any finite subset of the axioms Peano + $\exists c.0<c,S0<c,SS0<c,\dotsc$, therefore by the compactness theorem, there exists a model satisfying all of them.) See for example Henning Makholm's analogous answer about Presburger arithmetic at Nonstandard models of Presburger Arithmetic
Can one instead ask for an explicit verification that the induction axiom holds in some simple nonstandard model, instead of appealing to powerful model theoretic theorems?
In answers like this one, we get explicit constructions of these non-standard models. In short, we adjoin to our well-ordered infinite chain $\omega=\{0,1,2,3,\dotsc\}$ another chain, $\dotsc < c-1<c<c+1<\dotsc$ of order type $\omega^*+\omega,$ with $n<c+m, \forall n\in\mathbb{N},m\in\mathbb{Z}$. If we're modeling PA, so that our model has addition and multiplication, we will adjoin a more intricate order type (a densely ordered collection of such chains), as explained at this question, whereas if we just want to model the successor operation and induction, a single chain will suffice.
That this model will satisfy most of the Peano axioms is obvious, but validity of the induction axiom is not. It in fact contradicts naive intuition (presumably based in second-order thinking?) about how mathematical induction works, which is that it bootstraps up a connected well-ordered total chain from the first element through all successors. Second order thinking suggests this should not be valid through the disconnected total chain present in the non-standard model.
The proof that the induction axiom holds for nonstandard models typically relies on the compactness theorem is nonconstructive, since it relies on some weak form of the axiom of choice. Is this obligatory? Is there a possibility of an explicit verification of the induction axiom for this model?
Or is this analogous to the existence of a Hamel basis of the real numbers over the rationals? Is it possible that in some choice-negating set theory like Solovay's model, where all sets of reals are Lebesgue-measurable, that also all models of numbers which satisfy the induction axioms are order-isomorphic to $\omega$?