Formalizing undefinedness arising in calculus

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 stated 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.