Coq中的Peano算术答案

【问题标题】：Peano arithmetic in CoqCoq中的Peano算术
【发布时间】：2019-01-03 21:35:33
【问题描述】：

Coq 的 standard library 说这种归纳类型给出了 Peano 自然数：

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

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

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

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

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

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

【问题讨论】：

我认为，当大多数人说“Peano naturals”时，他们谈论的是自然数的特定表示，即从零和后继生成的，而不是二进制自然数，这将是将它们表示为有限的二进制字符串。它与任何被称为“皮亚诺算术”的特定理论没有任何关系。

标签： coq

【解决方案1】：

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

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

【讨论】：