Formalizing Undefinedness Arising in Calculus

William M. Farmer

2004

Abstract

Undefined terms are commonplace in mathematics, particularly in
calculus.  The traditional approach to undefinedness in mathematical
practice is to treat undefined terms as legitimate, nondenoting terms
that can be components of meaningful statements.  The traditional
approach enables statements about partial functions and undefined
terms to be expressed very concisely.  Unfortunately, the traditional
approach cannot be easily employed in a standard logic in which all
functions are total and all terms are defined, but it can be directly
formalized in a standard logic if the logic is modified slightly to
admit undefined terms and statements about definedness.  This paper
demonstrates this by defining a version of simple type theory called
Simple Type Theory with Undefinedness (STTwU) and then formalizing in
STTwU examples of undefinedness arising in calculus.  The examples are
taken from M. Spivak's well-known textbook Calculus.