coq - 如何证明 COQ 理论的一致性

Question

我如何证明(或更好:令人信服的论证)我的 COQ 理论是一致的？
让我们假设 COQ 系统和标准库是一致的。我知道由于哥德尔不完备性定理，一般形式的一致性证明是不可能的。
但是，是否有一些方法或经验法则可以证明该理论是一致的？
更具体一点:如果我只使用归纳数据类型而不使用明确的公理命题，我的理论是否自动一致？

Answer 1

Coq 的全部意义在于，如果系统接受了您的定义和证明，那么您可以相信它们在逻辑上是合理的。但是，有两个注意事项:

• 您必须相信系统的底层逻辑是健全的，并且已正确实现。

• 您不得使用任意公理扩展基础理论，或启用不安全的选项(例如 -type-in​​-type)。

最后一点值得解释。使用 Fixpoint、Definition 或 Inductive 等命令陈述的定义和证明属于 Coq 的基本理论，因此自动保持一致。这就是 Coq 对这些命令施加一些限制的原因，例如只允许某些类型的递归函数。另一方面，如果您使用 Axiom 命令或类似命令要求 Coq 接受任意命题，那么您可能会得到不一致的开发结果。

一些公理，例如排中律和泛函外延性，已经得到了相对充分的研究和理解，因此假设使用也不会太危险。根据经验，您可以信任标准库中声明的公理。尽管如此，您还是应该小心:例如，一些标准公理与 -impredicative-set 选项不兼容(参见 here )。

如果您想确保您的开发不依赖于特殊的公理，您可以使用 Print Assumptions 命令(参见 here )列出您的结果中使用的所有公理。