Reasoning about Partial Functions with the Aid of a Computer

William M. Farmer

1995

Abstract

Partial functions are ubiquitous in both mathematics and computer
science.  Therefore, it is imperative that the underlying logical
formalism for a general-purpose mechanized mathematics system provide
strong support for reasoning about partial functions.  Unfortunately,
the common logical formalisms -- first-order logic, type theory, and
set theory -- are usually only adequate for reasoning about partial
functions in theory.  However, the approach to partial functions
traditionally employed by mathematicians is quite adequate in
practice.  This paper shows how the traditional approach to partial
functions can be formalized in a range of formalisms that includes
first-order logic, simple type theory, and Von-Neumann-Bernays-Goedel
set theory.  It argues that these new formalisms allow one to directly
reason about partial functions; are based on natural, well-understood,
familiar principles; and can be effectively implemented in mechanized
mathematics systems.