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. The documents listed below were produced over the course of a year; some of them have become outdated as our understanding of the theory advanced. As such, their purpose is not to provide an exact statement on the theory we have developed, but to illustrate its character. We would recommend starting with the following report, which introduces the project and reproduces the more self-contained material in its appendices.
Report. (Aug 2008.) Main Text Table 1 Insert A3 Chart Appendices
Sketch of Discourse Representation Theory. (Oct 2007.) Since the semantics of the project depend closely on Discourse Representation Theory, I produced a very brief summary suitable for non-linguists familiar with logic. Most of the important material is in the first two pages. PDF
Introductory Example. (Oct 2007.) This example takes a very simple proof, that of the irrationality of sqrt(2), and steps through the treatment of this example in the language. The first third of the document introduces many of the basic concepts of the language. The remainder focuses on justifying in detail the choice of semantic representation. Main Text Accompanying Parse Trees
Introduction to Type. (Nov 2007.) This non-technical document discusses the type system needed to describe real mathematics. It is relatively independent of the other documents produced here and is likely to contain the material of most interest to mathematicians. PDF
Type and Parsing. (Dec 2007.) This document describes the type system and of the parsing process, which are closely related. The first half gives a detailed, technical version of the material presented in the 'Introduction to Type'. The second half gives a computational, i.e. nonalgorithmic, specification for the parsing process; it best exhibits the technical linguistic work which lies at the heart of the project. PDF
Reanalysis. (Jan 2008.) Reanalysis is the phenomenon where a surface string is assigned a novel analysis (i.e. new parse tree or new semantics) which does not change its meaning. For example, as one's mathematical knowledge increases, 'x^n' shifts from meaning ''the product of n copies of x'' to meaning 'e^(n \log x)'. This document discusses reanalysis and presents an argument for how it should be treated by the language. PDF
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
Systems and Models. (Feb 2008.) The orthodox view often taught to mathematicians, that numbers are sets, corresponds badly with actual mathematical practice; for example, 'A^B' is taken to mean very different things when A and B are numbers and when they are sets. On the other hand, discarding this position leads to a proliferation of axioms, and the fear that these may be inconsistent. (Mathematics is done in ZFC for a reason!) Similar problems arise with different kinds of numbers; integers are standardly constructed out of natural numbers, but in usage are identified with natural numbers.
This document shows how we may recover the best of both worlds, i.e. construct systems with the observed ontological relationships without expanding the epistemological basis. It is relatively independent of the other work presented here. 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
On Definitions. (Nov 2008.) One of the most striking features of mathematics, considered as a language, is that the syntax of the language changes as new 'definitions' are encountered. Definitions are described in full in this document. PDF
Parallel Text. (Dec 2008.) We present material drawn from an original textbook and illustrate how it needs to be restricted in order to fall within the scope of the language described here. 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 Slides
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. RestrictionsCSLI: A Language for Mathematics. (Jan 2009.) I 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