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

Question

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

我想对此声明进行澄清，我想问一个Coq论坛，因为这个问题不仅适用于Coq，而且适用于精益（但我很可能在这里得到答案）。

[阅读《经典公理》时，我了解到我们有等同于排除中间定律的东西：

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

在没有任何公理的构造演算中，具有元理论