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.
$\begingroup$
$\endgroup$
2
asked Sep 11, 2019 at 21:42
-
2$\begingroup$ Well, how do you prove that structural induction works? $\endgroup$– Eric WofseySep 11, 2019 at 21:48
-
$\begingroup$ You can't do induction on infinite lists... (though, I think you more meant that $\mathsf{Nat}\cong\mathsf{List}(1)$, i.e. a natural number is isomorphic to a list of unit types). $\endgroup$– Derek Elkins left SESep 11, 2019 at 23:07
Add a comment
|
1 Answer
$\begingroup$
$\endgroup$
6
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.
answered Sep 11, 2019 at 23:15
-
$\begingroup$ Isn't inductive definition of $\mathbb{N}$ (1. 0 is a natural number; 2. For every natural number n, S(n) is a natural number) enought for structural induction to hold? What do I need more for it to work? After all many languages I saw were defined same way and structural induction was used for them. $\endgroup$ Sep 12, 2019 at 11:36
-
1
-
$\begingroup$ @Trismegistos No. As a first-order theory, that just means you have a constant and a unary function symbol. This is modeled by any non-empty set. Often when you see descriptions like that (in a set-theoretic context) they'll have the word "smallest", and it will be implied that $0$ and $S$ are meant to be "symbolic" which can be encoded in various ways. If you unfold what "smallest" should mean, you'll see it's a set-theoretic induction formula. Whether this smallest set exists is a statement that needs to be proven and, e.g., won't be true without the Axiom of Infinity. $\endgroup$ Sep 12, 2019 at 17:39
-
$\begingroup$ Do I understand correctly that structural induction works for sets but Peano Axioms define natural numbers but not set of natural number so I can't use structural induction? $\endgroup$ Sep 13, 2019 at 14:32
-
$\begingroup$ @Trismegistos What "(structural) induction" means depends on the context in which you are working. Induction involves showing some "property" holds for all of something if it holds in various special cases. Different foundations have different ways of representing "property". For first-order logic, this is handled meta-theoretically with formulas. For second-order logic, we can directly quantify over predicates. For set theory, we use subsets. For constructive type theory, we use $\mathsf{Prop}$- or $\mathsf{Type}$-valued functions. In (ZFC) set theory, induction on naturals can be... $\endgroup$ Sep 13, 2019 at 19:42