Is it to say that whenever we use mathematical induction, we're inevitably admitting Peano axioms for $\Bbb N$ indeed?

Question

From Enderton's mathematical logic book sec 1.1, there is a thing called construction sequence for wffs. For example, $P\wedge Q\to R$ can be thought as $\langle P,~Q,~P\wedge Q,~R,~P\wedge Q\to R\rangle$. And then he used it to prove a theorem, which he called Induction Principle, saying that if a set $S$ of wffs contains primitive sentential symbols and is closed under $\vee,\wedge,~\cdots$ etc, then $S$ is no more or less the set of all wffs.

My problem is that, in his proof he used mathematical induction on the position of the construction sequence. However, does it mean that he implicitly assumed the Peano axioms (of course I especially refers to the mathematical induction axiom)? But when I look closer to this, I somehow feel that the induction used here is very "intuitive" and reflects the human mind ... you know what I mean. So my question is stated blurred as "whenever we use mathematical induction (even if we are not explicitly dealing with a predicate for $\Bbb N$), are we inevitably admitting Peano axioms for $\Bbb N$ indeed?"

Answer 1

Not necessarily.

See Structural induction:

Structural induction is a proof method that is used in mathematical logic, computer science, graph theory, and some other mathematical fields. It is a generalization of mathematical induction over natural numbers.

Structural induction is used to prove that some proposition $P(x)$ holds for all $x$ of some sort of recursively defined structure, such as formulas, lists, or trees. A well-founded partial order is defined on the structures ("subformula" for formulas, "sublist" for lists, and "subtree" for trees). The structural induction proof is a proof that the proposition holds for all the minimal structures, and that if it holds for the immediate substructures of a certain structure $S$, then it must hold for $S$ also.