coq - Coq 中的 Peano 算术

Question

Coq's standard library说这个归纳类型给出了皮亚诺自然数:

  Inductive nat :=
  | O : nat
  | S : nat -> nat.

听起来不错，因为我们可以在 Coq 中证明 nat 上的所有 Peano 公理，包括归纳原理，由 Coq 给出为 nat_ind .

但是这个 repo声称它在 Coq 中有一个证明 Goodstein's theorem .我们知道这个定理不能仅用皮亚诺公理证明。所以看起来 Coq 的 nat比皮亚诺公理更强，它宁愿是它们的模型，其中古德斯坦定理是正确的。这样对吗 ？

Coq 能否在 nat 上证明相同的算术定理？就像 ZFC 集合论对标准自然数所做的那样？如果我们在 Coq 中添加经典逻辑，同样的问题:

Axiom excluded_middle : forall P : Prop, P \/ ~P.

这背后的潜在问题是 Coq 证明的真实性。他们提供什么保证？我是一名开发人员，所以我对程序的证明特别感兴趣，因此对算术的具体问题很感兴趣。

Answer 1

你是对的。任何可以在 Peano 算术中证明的结果也可以在 Coq 中证明(至少，如果我们允许自己使用排中式的话)；然而，有些 Peano 算术的句子在该系统中无法证明，但可以在 Coq 中证明。

本杰明·维尔纳 showed Coq 和 ZFC 在表达能力方面几乎相同:如果您假设足够大的基数，您可以在 ZFC 中解释 Coq，并且您可以通过假设一些非构造性公理来解释 Coq 中的 ZFC。 (当然，计算机检查的 Coq 证明的状态更复杂，因为 Coq 中实现的理论与该论文中考虑的理论略有不同，并且 Coq 实现或计算机运行中可能存在错误它。)