A Set-Theoretical Foundation for Formalised Mathematics

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.