A Set-Theoretical Foundation for Formalised Mathematics

这个博士项目旨在开发一种集合论的变体，旨在产生更忠实的普通，教科书风格的数学形式化。我们还寻求有助于计算机辅助数学领域，通过实施这一理论的证明助理伊莎贝尔。Zermelo-Fraenkel（ZF）集合论被数学家认为是一个久经考验的基础，在世纪得到了广泛的研究。然而，ZF在计算机辅助数学中的实际应用与Coq，Agda和现在的Lean等类型理论系统的巨大成功相比相形见绌。然而，这样的系统仍然没有获得数学家的吸引力，因为在实践中，它们使用自然语言，集合论和一阶逻辑的组合。数学的严格形式化是一个费力的过程，因为大部分推理都隐藏在散文中。我们希望通过扩展ZF来部分缓解这个问题，这些特征是数学家通过自然语言隐式使用的。我们强调三个主要特点，我们希望实现：抽象数据类型，例外，并明确的descriptions.Objects在大多数集理论是由一组公理描述的行为集成员关系。因此，话语领域中的所有对象都被视为集合。这迫使我们使用低级定义，例如a，B =（（a），（a，B））和3 =（0，1，2）。在缺乏定义机制的情况下，这允许我们证明奇怪的定理，如（a）in（a，B）和2 in 3。以前的工作从我的本科论文提出了一个变种的ZF集理论，它承认有序对，作为结构化的，非集对象（urelements）。对这一点的推广将提供一个框架，用于创建具有不同内部（集合）表示和外部（元素）表示的对象类。未定义的术语通常出现在数学中，最著名的例子是整数除以零。引入一个类似于大多数编程语言中的“异常”概念的对象，可以更好地支持这些未定义的术语和部分函数。当数学家使用诸如“唯一的x使得.等短语来指代一个对象时，就采用了确定性描述。我们将使用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.