如何在COQ理论中证明一致性

如何证明（或更好的说服理由）我的COQ理论是一致的？
让我们假定COQ系统和标准库是一致的。由于Gödelian不完备性定理，我知道一致性的一般形式证明是不可能的。
但是，有没有一些方法或经验法则如何论证该理论是一致的？
更具体一点：如果我只使用归纳数据类型并且没有明确的公理命题，那么我的理论是否自动一致？如何在COQ理论中证明一致性

来源

2015-12-23 Cryptostasis

请停止发布这些f *** ing“这是一项作业”的评论。不，这不对。 20年前我学习了数学。而且我的问题肯定听起来不像家庭作业。如果你能回答它，然后发布答案。如果你不能，保持安静！ – Cryptostasis

嗯，我不知道你在想哪种理论，但至少对于逻辑来说，一种显示一致性的方法是使用（结构）证明理论论证，如[删除]（https：//en.wikipedia .ORG /维基/切割elimination_theorem）。 –

考虑到证明助理的用法，例如Coq，为了表示理论的一致性，我们需要考虑： - 定理证明逻辑是合理的（这就是（共）归纳结构演算的情况）。 - 定理证明器的实现是正确的。这是一件很难实现的事情。我不知道Coq的类型检查器是否完全验证。 [Barras]（http://www.lix.polytechnique.fr/~barras/publi/coqincoq.pdf）已经证明了Coq中Coq的类型检查器。但是，我不知道这个实现是否在Coq的当前版本中使用。 –

Coq的重点在于，如果系统接受您的定义和证明，它们在逻辑上是合理的。但有两点需要注意：

您必须相信系统的底层逻辑是正确的，并且它已正确实施。
你不能用任意公理来扩展基本理论，或者启用不安全的选项（例如-type-in-type）。

这最后一点值得一些解释。使用诸如Fixpoint,Definition或Inductive之类的命令陈述的定义和证明属于Coq的基本理论，因此是自动一致的。这就是Coq为什么会限制这些命令，比如只允许某些种类的递归函数。另一方面，如果您要求Coq使用Axiom命令或类似命令来接受任意命题，那么最终可能会出现不一致的发展。

一些公理，如被排除的中间和功能扩展性，是相对充分的研究和良好的理解，因此不会太危险，如果假设。作为一个经验法则，您可以信任标准库中声明的公理。您应该小心：例如，某些标准公理与-impredicative-set选项不兼容（请参阅here）。

如果要确保开发不依赖特殊公理，可以使用Print Assumptions命令（请参阅here）列出结果中使用的所有公理。

来源

2015-12-24 03:49:53

如何在COQ理论中证明一致性

回答

相关问题