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

Question

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

我想就这个声明寻求澄清，我正在向 Coq 论坛提问，因为这个问题适用于 Coq 和 Lean 一样多（但我觉得我更有可能在这里得到答案）。

在阅读“经典公理”时，我了解到我们有与排中律等价的东西：

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 的证明。但他们实际上在谈论不同的事情。为了更清楚起见，我将把这个概念称为abuse-of-terminology-decidable。

现在，如果你在 Coq 中添加一个像 LEM 这样的公理，你基本上会声明每个谓词 P 都变成abuse-of-terminology-decidable。当然，你不能仅仅通过在 Coq 开发中添加一个公理来改变 conventionally-decidable 的含义，因此不再包含。

多年来，我一直在与这种滥用术语作斗争，但没有成功。

更准确地说，在 Coq 术语中，术语可判定不是用于享受 LEM 的命题或谓词，而是用于享受更强的以下语句的命题或谓词：

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

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