coq - 经典公理意味着每个命题都是可判定的？

Question

在精益手册“精益中的定理证明”中，我读到:“利用经典公理，我们可以证明每个命题都是可判定的”。

我想就此声明寻求澄清，我正在问一个 Coq 论坛，因为这个问题既适用于 Coq 也适用于精益(但感觉我更有可能在这里得到答案)。

在阅读《With the classical axioms》时，我了解到我们有等价于排中律的东西:

Axiom LEM : forall (p:Prop), p \/ ~p.

当读到“每个命题都是可判定的”时，我明白我们可以定义一个函数(或者至少我们可以证明这样一个函数的存在):

Definition decide (p:Prop) : Dec p.

其中 Dec 是归纳类型族:

Inductive Dec (p:Prop) : Type :=
| isFalse : ~p -> Dec p
| isTrue  :  p -> Dec p
.

然而，根据我对 Coq 的了解，我无法实现 decide 因为我无法破坏 (LEM p) (属于 Prop 类型)返回 Prop 以外的东西。

所以我的问题是:假设没有错误，并且“用经典公理，我们可以证明每个命题都是可判定的”这个陈述是有道理的，我想知道我应该如何理解它，所以我离开了我强调的悖论。是否我们可以证明函数 decide 的存在(使用 LEM)但实际上不能提供这种存在的见证？

Answer 1

在没有任何公理的结构的微积分中，元理论属性表明 A \/ B 的每个证明必然证明 A持有(使用构造函数打包 or_introl )或 B 的证明持有(使用其他构造函数)。所以 A \/ ~ A 的证明是 A 的证明持有或证明 ~ A持有。

遵循这个元理论属性，在 没有任何公理的 Coq 中，命题的所有证明都是 forall x, P x \/ ~P x 形式的实际上是证明 P是可判定的。在本段中，可判定 的含义是可计算性书籍中普遍接受的含义。

一些用户开始对任何谓词使用 decidable 这个词 P因此存在 forall x, P x \/ ~ P x 的证明.但他们实际上在谈论另一件事。为了更清楚地说明这一点，我将此概念称为可判定的滥用术语。

现在，如果你在 Coq 中添加一个像 LEM 这样的公理，你基本上声明每个谓词 P变得可判定滥用术语。当然，您不能通过在 Coq 开发中添加公理来改变 conventionally-decidable 的含义，因此不再包含包含。

我多年来一直在反对这种术语滥用，但没有成功。

更准确地说，在 Coq 术语中，术语 decidable 不是用于享受 LEM 的命题或谓词，而是用于享受更强的以下陈述的命题或谓词:

forall x, {P x}+{~P x}

此类命题的证明通常以 _dec 命名后缀，其中 _dec直接引用可判定的。这种滥用不那么强烈，但仍然是对术语的滥用。