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

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

• The proofs in Enderton's book, like almost all mathematics, don't specify the specific axioms being used. It is safe to pretend that the entire book assumes ZFC, because all the proofs could be formalized into that system. This not strictly necessary - we could view the proofs as being formalized in some other system if we preferred. However, the point of the proofs Enderton presents is not to study the axioms required to prove hist theorems, the point is simply to prove the mathematical theorems. This is the same as most other mathematical proofs. – Carl Mummert Mar 12 '18 at 10:51
• @CarlMummert Thanks. I see. – Eric Mar 12 '18 at 10:57

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.
• Do we need to prove the validity of "Structural induction" itself? If so, does such proof get rid of the traditional mathematical induction (and/or Peano axioms for $\Bbb N$)? – Eric Mar 12 '18 at 10:34
• @Eric - Yes; recursion is justified (i.e. proved from axioms) in $\mathsf {ZFC}$. See Enderton, page 73. – Mauro ALLEGRANZA Mar 12 '18 at 10:41