Coq中的公理和变量有什​​么区别

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

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

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