在 Coq 中，induction 策略的理论基础为 structural induction，中文维基称其为“结构归纳法”。但“归纳”二字易同“归纳推理”混淆。诚然英语亦面临此问题，但汉语能否更通达地表述此概念？
已知掣肘因素如：“数学归纳法”是 structural induction 在自然数之特例，此概念在中学已普及。
請教台灣同仁：國語中“歸納”是否兼具 inductive reasoning 和 structural induction 含義？
我不是认真的：
我总觉得中英的逻辑和数学用语陷入一种困境。
一方面，如果英语的用了一个用烂的词指代一个特定的概念，那么中文的意思表达就特定得多。比方说群（group），环（ring），格（lattice)，范畴（category），中文都比英文要好太多。
但是另一方面，如果术语用到的是组合型的词汇，那英语实在是好太多了。这些词汇的中文翻译简直无法直视，意思也难以表达。比方说morphism, intuitionism, homotopy等。
最后点一下题：
翻译的话我觉得归纳法就挺好的，毕竟中学也是这么教的。没必要修改译法，免得和大部分人的固有知识不匹配。
1 Like
试释之：
归纳者，归有限以纳无穷也。
演绎者，循式列陈诸言，以竟厥辞也；
其中结构归纳者，穷其里，俱现其外也。虽无穷者，皆整础也，故言之凿凿。
几经查阅，日韩越均以“归纳”论上述两概念，我也觉得与其逆四国通行之用法，不如将“结构归纳”诠释为：通过演绎，实现严谨的归纳。
无论如何，在我们使用的严格的语境（sf 的翻译中，比如）下，常见的“归纳推理”不出现在任何地方，所以我觉得没有辨析的需要。
所谓数学归纳法的，就已经是“通过演绎，实现严谨的归纳”的了。只是此处我们使用CIC，才会出现“结构”的。数学上，还有其他乱七八糟的归纳法，就是大体跟 well-founded 对应的那些，我们可以在不是“序列”而是“网”或者“滤子”上做归纳，毕竟归纳这事情只跟序结构有关系。在这些情况下，都没有使用“结构归纳法”的先例，或者说，“数学归纳法”的意涵已经足够 general 了。（事实错误）
此处讨论的翻译事宜不限于特定教材，旨在为整个中文数理科学社区提供参考。
视野内关于数学归纳法的讨论似乎均面向自然数，故建议以“结构归纳法”谓广义狭义之辨。
1 Like
那是统统用结构归纳法还是用数学归纳法 when possible 呢？
“数学归纳法”甚普及，可用作体词。
例：加法结合律
定理：对任意自然数 n、m、p，均有：n + (m + p) = (n + m) + p。
证明：以数学归纳法对 n 分类讨论：
- 对于
n = 0：
试论：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 分类讨论”这种说法。
1 Like
你提到的三种用法，谓语均为“用”。该动词虚无缥缈，不表示任何动作。我因此代之以“讨论”，并前置“归纳”为状语。命名定式尚可鉴，修辞糟粕不得取。
用“用”并没什么问题吧，否则要是开头是别的提示文字，你怎么对应？
- 证明：用归纳法。
和
- 证明：用 Zorn’s Lemma。
有一样的结构，这样的相似性是我不愿意失去的。把这些文字放在证明的最开头，只是点明构成证明主体的主要工具 n.，不应该要费心挑一个谓语（因为不是重点）。现在这样恐怕是能找到的最简练最强调重点的说法了。要是“我们用归纳法来证明定理1”这种，你准备如何调整？
另外，称共同体的选择为糟粕可是很严肃的指控啊。 
“用”可用于动宾短语作状语，例如你提到的：
此句谓语“证明”是具体的动作，故可取。
所谓共同体，数学水平我惮于指控，但落笔佶屈聱牙，令学生头痛不堪，此吾敢言也。
“结构归纳法”是个直译的专有名词呀, 并且我觉得这个直译非常的达意, 没有必要在这种地方搞创新.
另外 “数学归纳法” 中的 “数学”, 特指 “算术”, 指对自然数运用归纳法, 这个意思也非常明确, 建议不要混淆两者.
暂定遣词循惯例，造句略区分，例：
请批评指正。
我认为数学归纳法歧义很大，数学归纳法可以是对n的structural induction；也可以是对某个k的k-induction；也可以是strong induction。可以避免的时候应该尽量避免。
你的建议是 structural induction 均译为“结构归纳”，而不考虑对象是否为自然数？
这样确实更为精准。
对，无须考虑。本质上也就只有structural induction，没必要引入多种术语引起歧义。
1 Like