coq - mathcomp/ssreflect 是否支持经典逻辑

Question

例如，coq 在其标准库中有一个 Classical 包，其中包含经典逻辑中的引理，例如与 forall 和 exists 相关的引理 (https://coq.inria.fr/library/Coq.Logic.Classical_Pred_Type.html)。

我的问题是 mathcomp 或 ssreflect 本身是否有类似的支持。到目前为止，我只找到了 https://github.com/coq/stdlib2/blob/master/src/bool.v#L548 中的一些定义和引理。

谢谢

Answer 1

我认为基本的 mathcomp 库中没有任何类似的内容。最接近的可能是 ssrbool 中的 classically 运算符，它模仿直觉逻辑中的经典推理。但是，实验性 mathcomp 分析库采用经典公理并具有与您提到的结果类似的结果 (https://github.com/math-comp/analysis/blob/master/theories/boolp.v)。