Why Induction Axiom is needed if structural induction holds

Question

Peano axioms introduce induction as an axiom because it can not be proven from other axioms. On the other hand I used structural induction on structures like lists and trees. These structures are more complicated (infinite list can be seen as chain of natural numbers) so I could use structural induction on natural numbers as well because they are defined recursively (0 is base element and s(n) is natural number if n is natural). So why I can't use structural induction for natural numbers and why we need induction as an axiom.

Answer 1

If you are working in a framework that allows you to define inductive types/inductively defined sets, like the Calculus of Inductive Constructions, then you wouldn't need to add induction on naturals as an axiom.

First-order logic, the framework in which Peano Arithmetic is defined (or second-order logic if you want the second-order induction axiom) and the typical framework for most mathematics doesn't have inductive types.

If you are working in set theory, e.g. ZFC, then, again, you don't need to add any axioms to model the naturals or inductively defined sets.

In other words, having structural induction as a "primitive" concept is not the usual thing to do (except in modern type theories). Also, given induction on naturals and some other stuff (e.g. if you are working in ZFC), you can define structural induction, so induction on naturals is more minimal in that context.

On a more personal note, I do think there should be more emphasis on structural induction and less on induction over natural numbers. Many inductions in texts are structural inductions but get reformulated as inductions over natural numbers in ways that just add work because the author is either unfamiliar with structural induction or didn't feel like introducing it and can't assume the reader will know what is meant.