2013 | OriginalPaper | Chapter
Type
Author : Mohan Ganesalingam
Published in: The Language of Mathematics
Publisher: Springer Berlin Heidelberg
Activate our intelligent search to find suitable subject content or patents.
Select sections of text to find matching patents with Artificial Intelligence. powered by
Select sections of text to find additional relevant content using AI-assisted search. powered by
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.