A Language for Mathematics

Oct 2012: I have removed the thesis from this website as a revised version will soon be available as a book.

The work presented here is part of a project to construct programs which 'understand' mathematics well enough to be useful to mathematicians. This is a long-term joint project (T. Barnet-Lamb and M. Ganesalingam); the material presented here only treats the linguistic side of our work.

Thesis. (Aug 2009.) The most up-to-date description of the work appears in the following thesis. A short summary intended for a lay audience may be found here.

The main chapters of the thesis may also be downloaded individually:

2. The Language of Mathematics. This chapter gives an informal overview of the language of mathematics, presented from a linguistic perspective. PDF

3. Theoretical Framework. This chapter sets out the basic theoretical framework used to describe mathematics in the thesis. PDF

4. Ambiguity. This chapter gives a extensive discussion of ambiguity in both words and symbols in mathematics, and shows that mathematics exhibits kinds of ambiguity which are not found in other languages. PDF

5. Type. This chapter presents the system of types which are needed to correctly analyse and disambiguate mathematics. PDF

6. Typed Parsing. This chapter gives a unified model for the process of interpretation and disambiguation of mathematics. PDF

7. Foundations. This chapter discusses linguistic, philosophical and technical problems appearing in all existing accounts of the foundations of mathematics, and provides a novel account. It is relatively independent of the remainder of the thesis. PDF

8. Extensions. This chapter briefly discusses a number of phenomena that could not be discussed in the main thesis for reasons of space. It also discusses an approach to ellided information in mathematics, which will be expanded on in a separate paper. PDF

Specialised audiences may find particular chapters of the thesis more relevant than others. We would recommend that linguists initially look at chapters 2 and 3, that mathematicians look at chapter 7, that philosophers of mathematics look at section 2.6 and chapter 7, and that computer scientists with an interest in automated theorem proving look at chapters 5 and 7 and section 8.3.
Most of the older documents that were previously included on this website have now been superseded by the thesis. Exceptions are listed below. The old version of the website may also be found here if required.

Chained Infixed Formal Relations. (Jan 2008.) Rather than writing 'a<b and b<c', mathematicians generally write 'a<b<c'. There are restrictions on what binary relations can be 'chained' in this way --- for example, 'a<b>c' is illegal. This document outlines the criteria licensing chaining of relations. PDF

Higher-Order Constructs. (Feb 2008.) Explicitly higher-order material is rare in mathematics --- mathematicians tend to introduce sets to convert statements into first order variants. (Cf. the two common versions of Peano's fifth axiom.) Nevertheless higher-order material does occur -- in the axioms of specification and replacement, and more silently in certain definitions. This document outlines a treatment of this material which also allows a library-introduced treatment of ellipsis, as occurs in 1^2+2^2+...+n^2. PDF

Flatlands: Linguistic Phenomena in Mathematics. (Jun 2008.) Slides from a paper given at the 2008 Flatlands conference. The first half gives an overview of the project. The second presents evidence that first order logic is not an adequate semantic representation for mathematics, and shows that Discourse Representation Theory is. Slides (PDF)

Parallel Text. (Dec 2008.) The linguistic work presented here forms the basis for a computer language closely resembling real mathematics. We present material drawn from an original textbook and illustrate how it needs to be restricted in order to fall within the scope of this language. The material chosen is taken from 'An Introduction to the Theory of Groups' (Rotman), and covers group theory from the beginnings to Sylow's Theorems. Text with Explanation (PDF) Slides (PDF)

While looking at the parallel text, you may also find it useful to look at a provisional version of the restrictions that need to be followed when writing documents in the language. Restrictions (PDF)

CSLI: A Language for Mathematics. (Jan 2009.) I (M. Ganesalingam) spent a fortnight as a visitor to the Centre for the Study of Language and Information in Stanford. During that time I presented the linguistic side of our work; the slides are available here. Slides (PDF)