与 Set 和的可判定相等语句。支柱

Question

在查看具有可判定相等性的类型的结果时（尤其是在 Eqdep_dec 中），有一些结果（对于 A 类型）需要

  forall x y : A, x = y \/ x <> y

有些需要

  forall x y : A, {x = y} + {x <> y}

我的印象是最后一个被称为可判定相等，但我非常不确定有什么区别。我知道Prop 和{x = y} + {x <> y} 中的x = y \/ x <> y 在Set 中，我可以从第二个证明第一个，但不能反过来证明。据我了解，这是因为我不允许从Set 类型的值构造Prop 类型的值。

谁能说出两者的区别？是否有一些类型的例子可以证明第一个陈述但不能证明第二个陈述。另外，{x = y} + {x <> y} 的版本是不是所谓的可判定相等？

Answer 1

你是正确的，后一个定义，即存在于Set 中的定义被称为可判定相等。

直观地说，我们将Set 中的对象解释为程序，将Prop 中的对象解释为证明。因此，可判定相等类型是一个函数的类型，它采用某种类型A 的任意两个元素并决定它们是否相等。

另一种说法稍弱。它描述了A 的任意两个元素要么相等要么不相等的命题。值得注意的是，对于x 和y 的特定值，我们将无法检查哪个结果，至少在证明中的案例分析之外。这是您提到的 Prop 消除限制的结果（尽管您倒退了：不允许通过消除/匹配排序 Prop 的元素来构造排序 Set/Type 的值)。

如果不添加公理，Prop 宇宙是建设性的，所以我相信不会有任何类型A 使得相等性是不可判定的，但命题变体是可证明的。但是，考虑我们通过添加以下公理使Prop 宇宙成为经典的场景：

Axiom classic : forall P, P \/ ~P

这将使命题变体对于任何类型A 都可以轻松证明，而可判定的等式可能无法实现。

请注意，我们的公理是一个命题。直观地说，一个命题或其否定必须成立是有道理的。如果我们没有将其设为Prop（例如，如果我们将forall P, {P} + {~P} 公理化），那么我们可能不会接受这个公理，因为它会声明存在一个通用决策过程。

这有点跑题了，但希望它能证明我们对Props 和Sets 的解释存在一些差异。