"The Language of Mathematics"
Mohan Ganesalingam (Cambridge)
4:15pm, Cordura 100

We describe an ongoing project to construct a formal language closely resembling the actual language used by working mathematicians. We begin by showing that the latter is in several respects demonstrably untreatable by conventional formal languages, and continue to show that it exhibits phenomena such as generalised quantification, underspecification and presupposition, which are characteristic of natural language. We also argue that some distinctively formal properties of mathematical language (such as variables and type) can be exploited to counteract the standard difficulties associated with processing natural language.

These observations lead us to fuse concepts from linguistics and theories of formal language to create a "natural formal language" for mathematics. We continue to describe such a language, including its syntax and DRT-based compositional semantics. We finish by outlining some of the problems that needed to be solved to construct such a language and illustrate one such problem, 'typed parsing', in length. (In mathematics, parsing a sentence correctly depends on knowing the types of all constituents, while knowing those types depends in turn on having a correct parsing for the sentence. Typed parsing attempts to resolve this apparent circularity.)