Coq 中的 Axiom 和 Variable 有什么区别

Question

在 Coq 中我可以写

Variable A : False.
Axiom B : False.

假设 False在名称A和B. 这两个陈述都适用于证明，所以我可以

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

实际的区别是什么？我什么时候应该使用一个而不是另一个？

Answer 1

建议使用命令 Axiom、Conjecture 和 Hypothesis（及其复数形式）进行逻辑假设（即当断言类型为 sort Prop 时），其他情况下使用命令 Parameter 和 Variable（及其复数形式） （对应于抽象数学实体的声明）。

正如您在 coq https://coq.inria.fr/refman/coq-cmdindex.html的规范中所见，它们的定义方式相同。