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

Question

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

Definition eq_add_S n m (H: S n = S m): n = m := f_equal pred H.

Hint Immediate eq_add_S: core.

它看起来像一个公理(？)，但让我困惑的是，在该页面的顶部它说:

It states various lemmas and theorems about natural numbers, including Peano's axioms of arithmetic (in Coq, these are provable)

这句话是不是有点歧义？

Answer 1

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

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