# Is "induction" polysemic?

**URL:** <https://discourse.rocq-prover.org/t/is-induction-polysemic/241>\
**Category:** Miscellaneous\
**Created:** [March 21, 2019, 1:13am UTC](https://discourse.rocq-prover.org/t/is-induction-polysemic/241 "2019-03-21T01:13:25Z")\
**Posts on this page:** 2\
**Page:** 1

<div class="post-metadata">

**Author:** ![Lys](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/lys/32/48_2.png) [@Lys](https://discourse.rocq-prover.org/u/Lys)\
**Post date:** [March 21, 2019, 1:13am UTC](https://discourse.rocq-prover.org/t/is-induction-polysemic/241/1 "2019-03-21T01:13:25Z")

</div>

I was trying to translate “induction” accurately, but the term seems overloaded: There is “[structural induction](https://en.wikipedia.org/wiki/Structural_induction)” as in `induction` tactic, and there is “[inductive reasoning](https://en.wikipedia.org/wiki/Inductive_reasoning)”. Shall we treat them as related/similar concepts?

Related topic in Chinese:

> [@术语：induction](https://discourse.rocq-prover.org/t/induction/240):
>
> 在 Coq 中，induction 策略的理论基础为 [structural induction](https://en.wikipedia.org/wiki/Structural_induction)，中文维基称其为“[结构归纳法](https://zh.wikipedia.org/wiki/%E7%BB%93%E6%9E%84%E5%BD%92%E7%BA%B3%E6%B3%95)”。但“归纳”二字易同“[归纳推理](https://zh.wikipedia.org/wiki/%E5%BD%92%E7%BA%B3%E6%8E%A8%E7%90%86)”混淆。诚然英语亦面临此问题，但汉语能否更通达地表述此概念？ 已知掣肘因素如：“数学归纳法”是 structural induction 在自然数之特例，此概念在中学已普及。 請教台灣同仁：國語中“歸納”是否兼具 inductive reasoning 和 structural induction 含義？

---

<div class="post-metadata">

**Author:** ![palmskog](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/palmskog/32/38_2.png) [@palmskog](https://discourse.rocq-prover.org/u/palmskog)\
**Post date:** [March 21, 2019, 7:57pm UTC](https://discourse.rocq-prover.org/t/is-induction-polysemic/241/2 "2019-03-21T19:57:51Z")

</div>

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.