遗传有穷集理论片段的形式化
Formalization of Fragments of the Theory of Hereditarily Finite Sets
浏览论文内容
中文总结 AI 辅助
该研究在Isabelle/HOL中形式化遗传有穷集理论片段，采用locale层级结构对应不同公理片段，用一阶可定义谓词的归纳定义处理公理模式，分析等价的有穷性与正则性公理，并通过模型形式化公理独立性结论。
中文摘要 AI 辅助
本文在Isabelle/HOL中系统探究并形式化了一阶经典逻辑下遗传有穷集理论的公理化体系。该形式化工作采用locale层级结构，每个locale对应由一组特定公理给出的理论片段。文中引入了一阶可定义谓词的归纳定义，并将其用于形式化公理模式。研究特别关注若干等价的有穷性公理，以及多种等价的正则性表达方式。此外，本文还通过定义恰当的模型，形式化了关于某条公理相对于公理系统独立性的若干结论。
英文摘要
The axiomatization of the theory of hereditarily finite sets in first-order classical logic is systematically explored and formalized in Isabelle/HOL. The formalization uses a hierarchy of locales, each corresponding to a fragment of the theory given by a particular collection of axioms. An inductive definition of first-order definable predicates is introduced and used to formalize axiom schemata. Special attention is paid to several equivalent axioms of finiteness, as well as to several equivalent ways of expressing regularity. The work also formalizes several facts about the independence of an axiom from a system of axioms by defining appropriate models.
发表机构
- Institute of Computer Science of the Czech Academy of Sciences（捷克科学院计算机科学研究所）
- Faculty of Mathematics and Physics, Charles University, Prague（布拉格查理大学数学与物理学院）
机构由 AI 辅助整理，请以论文原文为准。
