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?"