# 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. Mar 12, 2018 at 10:51
• @CarlMummert Thanks. I see.
– Eric
Mar 12, 2018 at 10:57

Not necessarily.

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.

• 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, 2018 at 10:34
• @Eric - it depends on the context... we cannot prove all. In set theory, induction is proved (both structural and mathematical). Mar 12, 2018 at 10:36
• I see the point. Actually the construction sequence in Enderton's book is formalized under ZFC, and so the induction is justified (to be clear, included as an axiom) by the "ZFC axiom". Is it?
– Eric
Mar 12, 2018 at 10:37
• @Eric - Yes; recursion is justified (i.e. proved from axioms) in $\mathsf {ZFC}$. See Enderton, page 73. Mar 12, 2018 at 10:41
• @Eric - as said above, we have to start from somewhere. Our intuition about the natural numbers (formalized with Peano's axioms) is probably the "best and deepest" intuition we have. At the intuitive level, it is the source for any other "more abstract" form of induction. It is hard to mantain that e.g. the Axiom of infinity has any ground "outside" of our intuition about the succession of natural numbers. Mar 12, 2018 at 10:53