如何在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理論中證明一致性

回答

相關問題