I was trying to translate “induction” accurately, but the term seems overloaded: There is “structural induction” as in induction tactic, and there is “inductive reasoning”. Shall we treat them as related/similar concepts?
Related topic in Chinese:
1 Like
Inductive reasoning in empirical science (typically: going from particular observations to some general theory of how “all” things work) isn’t really connected to induction in mathematics, other than in spirit. In the philosophy of science, there is a long debate about the validity of empiricist inductive reasoning, and on whether it’s really a form of (logical) reasoning at all. One classic book on the topic is Popper’s The Logic of Scientific Discovery.
Induction in mathematics, in contrast, has been uncontroversial and well understood since the 19th century, with De Morgan being the first to name and fully describe the concept. Most mathematicians would probably say that structural induction is just one of many instances of the more general concept of well-founded induction, which can be applied using the well_founded_ind and well_founded_type recursors in Coq.
5 Likes