A Set-Theoretical Foundation for Formalised Mathematics

这个博士项目旨在开发集合论的变体，旨在为普通的、教科书风格的数学产生更忠实的形式化。我们还试图通过在证明助手Isabelle中实施这一理论，为计算机辅助数学领域做出贡献。Zermelo-Fraenkel(ZF)集合论被数学家认为是一个经过考验的基础，在20世纪得到了深入的研究。然而，与Coq、AGDA和现在的精益等类型理论系统的巨大成功相比，ZF在计算机辅助数学中的实际应用相形见绌。然而，这样的系统仍然无法吸引数学家，因为在实践中，它们使用了自然语言、集合论和一阶逻辑的组合。严格的数学形式化是一个费力的过程，因为大部分推理都隐藏在散文中。我们希望通过使用数学家通过自然语言隐式使用的特性来扩展ZF，从而部分缓解这个问题。我们重点介绍了我们希望实现的三个主要特性：抽象数据类型、异常和明确描述。大多数集合论中的对象由一组描述集员关系行为的公理来管理。因此，话语领域中的所有对象都被视为集合。这迫使我们使用低级定义，例如a，b=((A)，(a，b))和3=(0，1，2)。在没有定义机制的情况下，这允许我们证明奇怪的定理，如(A)在(a，b)中的，和在‘3中的2’。我在本科毕业论文中的以前的工作提出了ZF集合论的一个变体，它允许有序对作为结构化的非集合对象(Urelement)。这一点的推广将提供一个框架，用于创建具有不同的内部(集合)表示和外部(Urelement)表示的对象类。未定义的术语通常出现在数学中，最著名的例子是将整数除以零。引入一个类似于大多数编程语言中的“异常”概念的对象，将允许更好地支持这些未定义的术语和部分函数。当一个数学家用一个短语来描述一个物体时，我们将使用ZF作为扩展的基础，以保持逻辑上的一致性，以及其他所需的性质。在形式系统中实现这些特征将允许更具表现力的数学语言，更符合人类的书面数学。

This PhD project aims to develop a variant of set theory, intended to yield more faithful formalisations of ordinary, textbook style mathematics. We also seek to contribute to the area of computer assisted mathematics, via implementation of this theory in the proof-assistant Isabelle. Zermelo-Fraenkel (ZF) set theory is recognised by mathematicians as a tried and tested foundation, having been intensely studied over the 20th century. However, practical applications of ZF in computer assisted mathematics pale in comparison to the great success of type theoretical systems such as Coq, Agda, and now, Lean. Yet still, such systems fail to gain the attraction of mathematicians, because in practice, they use a combination of natural language, set theory, and first order logic. Rigorous formalisation of mathematics is a laborious process, since much of the reasoning is hidden in prose. We hope to partially alleviate this issue by extending ZF with features which are implicitly employed by the mathematician through natural language. We highlight three main features we wish to implement: abstract data types, exceptions, and definite descriptions.Objects in most set theories are governed by a set of axioms which describe the behaviour of the set membership relation. As a consequence, all objects in the domain of discourse are viewed as sets. This forces us to use low-level definitions, such as a,b = ((a),(a,b)), and 3 = (0,1,2). In the absence of a definition mechanism, this allows us to prove strange theorems like (a)'in'(a,b), and 2'in'3. Previous work from my undergraduate dissertation presented a variant of ZF set theory, which admits ordered pairs, as structured, non-set objects (urelements). A generalisation of this would provide a framework for creating classes of objects which have a distinct internal (set) representation and external (urelement) representation.Undefined terms commonly arise in mathematics, with the most known example of dividing an integer by zero. The introduction of an object similar to the notion of an ``exception'' found in most programming languages, would allow better support for these undefined terms, and partial functions. Definite descriptions are employed when a mathematician refers to an object using a phrase such as ``the unique x such that ...''We will use ZF as a foundation to be extended, in order to preserve logical consistency, among other desirable properties. Implementation of these features in a formal system would allow for a more expressive language of mathematics, more aligned with human written mathematics.