Coq中的Peano算术

Question

Coq的标准库表示此归纳类型给出Peano自然数：

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

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

但是这个回购声称它在古德斯坦定理的 Coq中有一个证明。而且我们知道，该定理不能仅用Peano的公理来证明。因此，似乎Coq的nat强于Peano的公理，它更像是它们的模型，其中Goodstein定理是正确的。它是否正确 ？

Coq是否可以证明与natZFC集合论在标准自然数上所做的算术定理相同？如果我们在Coq中添加经典逻辑，则存在相同的问题：

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

背后的根本问题是Coq证明的真实性。他们给予什么保证？我是一名开发人员，所以我对程序的证明特别感兴趣，因此对算术特别感兴趣。

Answer 1

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

Benjamin Werner证明了 Coq 和 ZFC 在表达能力方面几乎是等价的：如果假设足够大的基数，则可以在 ZFC 中解释 Coq，并且可以通过假设一些非构造性公理在 Coq 中解释 ZFC。（当然，计算机检查的 Coq 证明的状态更为复杂，因为 Coq 中实现的理论与该论文中考虑的理论略有不同，并且 Coq 实现或运行的计算机中可能存在错误它。）