coq - Coq中自然数后继的内射性

Question

我有点困惑，在自然数上定义的后继函数的内射性是否Coq是公理？根据Wikipedia/Peano axioms，它是一个公理 (7)。当我查看Coq.Init.Peano手册页时，我看到以下内容：

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

提示立即 eq_add_S：核心。

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

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

这句话有点模棱两可吧？

Answer 1

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

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