set - Isabelle 中的无类型集合操作

Question

我在伊莎贝尔有以下代码：

typedecl type1
typedecl type2

consts 
  A::"type1 set"
  B::"type2 set"

当我想对 A 和 B 使用联合操作时，如下所示：

axiomatization where
 c0: "A  ∩ B = {}"

由于 A 和 B 是不同类型的集合，因此我得到了类型冲突的错误，这是有道理的！

我想知道是否有任何对应的集合操作，他们隐含地将其操作数视为纯集合（即忽略它们的类型），因此像 A ∩' B 这样的东西成为可能（∩' 在上述意义上是 ∩ 操作对应物）。

PS：另一种解决方法是类型转换，我在这里将其作为一个单独的问题编写，以更好地组织我的问题。

谢谢

score 3 · Accepted Answer

Isabelle/HOL 中的集合总是有类型的，即它们只包含一种类型的元素。如果你想要无类型的集合，你必须切换到另一个逻辑，比如 Isabelle/ZF。

同样，HOL 中的所有值都用它们的类型进行注释，这是逻辑的基础。例如，相等只能应用于相同类型的两个值。因此，不同类型的值之间不存在相等的概念。因此，不存在忽略值类型的集合操作，因为这样的操作必须知道如何识别不同类型的值。

1 回答 1