在 Coq 中， induction 策略的理论基础为 structural induction ，中文维基称其为“ 结构归纳法 ”。但“归纳”二字易同“ 归纳推理 ”混淆。诚然英语亦面临此问题，但汉语能否更通达地表述此概念？
已知掣肘因素如：“数学归纳法”是 structural induction 在自然数之特例，此概念在中学已普及。
請教台灣同仁：國語中“歸納”是否兼具 inductive reasoning 和 structural induction 含義？

我不是认真的：

我总觉得中英的逻辑和数学用语陷入一种困境。

一方面，如果英语的用了一个用烂的词指代一个特定的概念，那么中文的意思表达就特定得多。比方说群（group），环（ring），格（lattice)，范畴（category），中文都比英文要好太多。

但是另一方面，如果术语用到的是组合型的词汇，那英语实在是好太多了。这些词汇的中文翻译简直无法直视，意思也难以表达。比方说morphism, intuitionism, homotopy等。

最后点一下题：
翻译的话我觉得归纳法就挺好的，毕竟中学也是这么教的。没必要修改译法，免得和大部分人的固有知识不匹配。

无论如何，在我们使用的严格的语境（sf 的翻译中，比如）下，常见的“归纳推理”不出现在任何地方，所以我觉得没有辨析的需要。
所 谓 数 学 归 纳 法 的 ， 就 已 经 是 “ 通 过 演 绎 ， 实 现 严 谨 的 归 纳 ” 的 了 。 只 是 此 处 我 们 使 用 CIC ， 才 会 出 现 “ 结 构 ” 的 。 数 学 上 ， 还 有 其 他 乱 七 八 糟 的 归 纳 法 ， 就 是 大 体 跟 well - founded 对 应 的 那 些 ， 我 们 可 以 在 不 是 “ 序 列 ” 而 是 “ 网 ” 或 者 “ 滤 子 ” 上 做 归 纳 ， 毕 竟 归 纳 这 事 情 只 跟 序 结 构 有 关 系 。 在 这 些 情 况 下 ， 都 没 有 使 用 “ 结 构 归 纳 法 ” 的 先 例 ， 或 者 说 ， “ 数 学 归 纳 法 ” 的 意 涵 已 经 足 够 general 了 。 （事实错误）

sora:

数学上，还有其他乱七八糟的归纳法，就是大体跟 well-founded 对应的那些，我们可以在不是“序列”而是“网”或者“滤子”上做归纳，毕竟归纳这事情只跟序结构有关系。在这些情况下，都没有使用“结构归纳法”的先例，或者说，“数学归纳法”的意涵已经足够 general 了。

视野内关于数学归纳法的讨论似乎均面向自然数，故建议以“结构归纳法”谓广义狭义之辨。

试论： 0 + (m + p) = (0 + m) + p 。
由加法之定义，上式显而易见。

对于 n = S n' ，其中 n' 满足 n' + (m + p) = (n' + m) + p ：
试论： (S n') + (m + p) = ((S n') + m) + p 。
由加法之定义，上式等价于：
S (n' + (m + p)) = S ((n' + m) + p) 。
据归纳假设，上式显而易见。证毕。

“结构归纳法”可简称“归纳”，用作谓词。
例： 链表联接结合律
定理：对任意链表 l1 、 l2 、 l3 ，均有： (l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3) 。
证明： 归纳讨论 l1 之构造：

对于 l1 = [] ：
试论： ([] ++ l2) ++ l3 = [] ++ (l2 ++ l3) 。
由链表联接之定义，上式显而易见。

对于 l1 = n::l1' ，其中 l1' 满足 (l1' ++ l2) ++ l3 = l1' ++ (l2 ++ l3) ：
试论： ((n :: l1') ++ l2) ++ l3 = (n :: l1') ++ (l2 ++ l3) 。
由链表联接之定义，上式等价于：
n :: ((l1' ++ l2) ++ l3) = n :: (l1' ++ (l2 ++ l3) 。
据归纳假设，上式显而易见。证毕。

那鉴于“数学归纳法”是“结构归纳法”的特例，用法不同恐怕要引发疑惑？

另外，我觉得“以数学归纳法对 n 分类讨论”中提到 分类讨论 实际模糊了重点。

中文文献（不光是中译文献，毕竟数学家平时也会说到归纳法）中，常见的用法是

对 n 用数学归纳法

对 n 用归纳法（保持 m 固定）

用数学归纳法

下面这样的才是可见于教材的论述文字。

证明：用归纳法。 n = 0 时，易得结论成立。现假设 n = k 时结论成立，则对于 n = k + 1 有…

这不仅是个翻译问题，甚至，完全不是个翻译问题：对数学归纳法一词的使用，在中文语境里早有定式。更武断一点，我认为，没有数学家会用“以数学归纳法对 n 分类讨论”这种说法。

证明：用 Zorn’s Lemma。

有一样的结构，这样的相似性是我不愿意失去的。把这些文字放在证明的最开头，只是点明构成证明主体的 主要工具 n. ，不应该要费心挑一个谓语（因为不是重点）。现在这样恐怕是能找到的最简练最强调重点的说法了。要是“我们用归纳法来证明定理1”这种，你准备如何调整？

另外，称共同体的选择为糟粕可是很严肃的指控啊。

试论：0 + (m + p) = (0 + m) + p。 由加法之定义，上式显而易见。 对于 n = S n'，其中 n' 满足 n' + (m + p) = (n' + m) + p： 试论： (S n') + (m + p) = ((S n') + m) + p。 由加法之定义，上式等价于： S (n' + (m + p)) = S ((n' + m) + p)。 据归纳假设，上式显而易见。证毕。 “结构归纳法”可简称“归纳”，用作谓词。 例： 链表联接结合律 定理：对任意链表 l1、l2、l3，均有：(l1 ++ l2) ++ l3 = l1 ++ (l2 ++ l3)。 证明：归纳讨论 l1 之构造： 对于 l1 = []： 试论：([] ++ l2) ++ l3 = [] ++ (l2 ++ l3)。 由链表联接之定义，上式显而易见。 请批评指正。