Coq中Axiom和Variable的区别是什么？

Question

在 Coq 中，我可以写

Variable A : False.
Axiom B : False.

假设在名称为“A”和“B”的情况下，False成立。这两个语句都适用于证明，因此我可以。

Theorem nothing_makes_sense : forall (a : Type), a.
  destruct true; exfalso.
  * apply A.
  * apply B.
Qed.

实际上有什么区别？什么情况下应该使用其中一个而不是另一个？

- radrow

Answer 1

建议使用Axiom、Conjecture和Hypothesis(及其复数形式)作为逻辑公设的命令(即当断言类型为Prop时)，在其他情况下(对应于抽象数学实体的声明)使用Parameter和Variable(及其复数形式)。如您所见，在Coq规范中https://coq.inria.fr/refman/coq-cmdindex.html，它们被定义为相同的方式。

- Carolina Carreira