Coq 中自然数后继的内射性

Question

我有点困惑在自然数上定义的后继函数的单射性是否Coq是一个公理？根据维基百科/皮亚诺公理，它是一个公理（7）。当我查看Coq.Init.Peano手册页时，我看到以下内容：

定义 eq_add_S nm (H: S n = S m): n = m := f_equal pred H。

提示立即 eq_add_S: core.

它看起来像一个公理（？），但令我困惑的是，在该页面的顶部它说：

它陈述了有关自然数的各种引理和定理，包括皮亚诺算术公理（在 Coq 中，这些是可证明的）

这句话是不是有点歧义？

Answer 1

你看到的命令实际上是构造函数单射性的证明S。更准确地说，它说后继函数是单射的，因为它有一个逆函数：前趋函数 ( pred)。（在 Coq 中，公理通常用关键字 来引入Axiom。）

您似乎对我认为“公理”一词的两个相关含义感到困惑。逻辑中更广泛的含义是“推理的起点”（维基百科）。狭义的说法是在演绎系统中被视为理所当然而无需进一步证明的断言。在皮亚诺算术中，皮亚诺的公理在两种意义上都是公理，因为它们是原始的。在Coq、ZFC集合论和其他系统中，它们可以从更基本的事实中得到证明。