Isabelle/HOL/GST：广义集合论的形式化证明环境
计算机科学中的逻辑
2022-07-26 v1 逻辑
摘要
广义集合论（GST）类似于标准集合论，但也可以具有非集合的结构化对象，这些对象可以包含其他结构化对象（包括集合）。本文提出对 GST 的 Isabelle/HOL 支持，将其视为类型类，组合了指定各类数学对象（例如集合、序数、函数等）特征的功能。GST 可具有一个异常特征，以简化偏函数与未定义性的表示。在组装 GST 时，会根据用户可修改的策略生成额外公理以填补规范缺口。广泛使用了称为软类型的专用类类型谓词。尽管 GST 可在无模型情况下使用，但为对其一致性保有信心，我们为每个 GST 从指定各特征对通过序数递归定义的冯·诺依曼式累积层次各层贡献的组件构建模型，然后将该模型连接到 GST 所占据的独立类型。
引用
@article{arxiv.2207.12039,
title = {Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories},
author = {Ciarán Dunne and J. B. Wells},
journal= {arXiv preprint arXiv:2207.12039},
year = {2022}
}