论文标题
Isabelle/Hol/GST：广义设置理论的正式证明环境
Isabelle/HOL/GST: A Formal Proof Environment for Generalized Set Theories
论文作者
论文摘要
广义集理论（GST）就像标准集理论，但也可以具有可能包含其他结构化对象在内的非集合结构化对象。本文介绍了Isabelle/HOL对GST的支持，GST被视为类型类，这些类别结合了指定数学对象的特征，例如集合，序数，序数，函数等。GSTS可以具有一个例外功能，该功能可轻松地表示代表部分功能和不确定性。组装GST时，按用户模型策略填补规范空白，会生成额外的公理。广泛使用了称为软类型的专用类型的谓词。尽管可以在没有模型的情况下使用GST，但为了对其一致性充满信心，我们为每个GST构建一个模型，这些组件从组件中指定每个特征对Von-Neumann式累积累积层次结构的贡献，从而通过序数递归定义，然后我们将模型连接到GST占用的单独类型的模型。
A generalized set theory (GST) is like a standard set theory but also can have non-set structured objects that can contain other structured objects including sets. This paper presents Isabelle/HOL support for GSTs, which are treated as type classes that combine features that specify kinds of mathematical objects, e.g., sets, ordinal numbers, functions, etc. GSTs can have an exception feature that eases representing partial functions and undefinedness. When assembling a GST, extra axioms are generated following a user-modifiable policy to fill specification gaps. Specialized type-like predicates called soft types are used extensively. Although a GST can be used without a model, for confidence in its consistency we build a model for each GST from components that specify each feature's contribution to each tier of a von-Neumann-style cumulative hierarchy defined via ordinal recursion, and we then connect the model to a separate type which the GST occupies.
