Type

Abstract

In this chapter, following on from our discussion of ambiguity (Chapter 4), we will introduce the types which are necessary to disambiguate mathematical language. As noted in §4.4, the actual inference of types will need to be fused into the parsing process; this will be the subject of the next chapter (Chapter 6). Additionally, in the course of this chapter, we will encounter a number of issues relating to the foundations of mathematics; these issues will be discussed extensively in Chapter 7.

There are two major difficulties that arise when one is trying to find the types necessary to describe mathematics. First, a great many type systems seem reasonable until a key counterexample is discovered; and, more specifically, these counterexamples are difficult to find because they are mathematically counterintuitive. There is a real disparity between what the rules of mathematics itself allow, and the way in which we think about mathematical objects. Each of the counterexamples we will present below reflects this disparity in a different way.