2004 | OriginalPaper | Buchkapitel
Formalizing Undefinedness Arising in Calculus
verfasst von : William M. Farmer
Erschienen in: Automated Reasoning
Verlag: Springer Berlin Heidelberg
Enthalten in: Professional Book Archive
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
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.