Set 与 Prop 的可判定相等语句

Question

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

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

而有些则需要

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

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

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

Answer 1

您是正确的，后一个定义（位于 中的定义Set）被称为可判定的相等性。

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

另一种说法则稍弱一些。它描述了以下命题： 的任何两个元素A要么相等，要么不相等。值得注意的是，我们无法检查 和的特定值的结果是哪种情况，至少在证明中的案例分析之外是这样。这是您提到的消除限制的结果（尽管您得到了相反的结果：不允许通过消除/匹配 sort 元素来构造 sort /的值）。xyPropSetTypeProp

在不添加公理的情况下，Prop宇宙是构造性的，因此我相信不会存在任何类型A使得等式不可判定但命题变体是可证明的。Prop然而，考虑一下我们通过添加以下公理使宇宙变得经典的场景：

Axiom classic : forall P, P \/ ~P

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

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

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