Isabelle 中的无类型集合操作答案

【问题标题】：Untyped set operations in IsabelleIsabelle 中的无类型集合操作
【发布时间】：2014-11-11 11:10:26
【问题描述】：

我在 Isabelle 中有以下代码：

typedecl type1
typedecl type2

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

当我想对 A 和 B 使用联合操作时：

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

由于 A 和 B 是不同类型的集合，我得到一个 clash of types 的错误，这是有道理的！

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

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

谢谢

【问题讨论】：

【解决方案1】：

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

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

【讨论】：

谢谢，您能否给我一些提示，告诉我如何切换到 Isabelle/ZF？我正在使用安装了 isabelle 的 JEdit，并且我正在我的文件中导入 Main 理论。 Isabelle/ZF 的语法与 Isabelle/HOL 的语法有区别吗？我会感谢更多的解释。
要切换到ZF逻辑，在理论面板中选择逻辑图像ZF并重新启动。请注意，ZF 与 HOL 完全不相交，即，HOL 中的任何定义都不能在 ZF 中使用。此外，ZF 使用不同的语法。 $ISABELLE_HOME/src/ZF 中的 ROOT 文件包含对 ZF 逻辑的一些参考文献。
我认为切换到 Isabelle/ZF 是理论上的。与 Isabelle/HOL 不同的是，它的库和工具在过去 20 年没有开发过。再次仔细查看您的应用程序，您应该找到使用 HOL 类型系统的方法。