A Set Theory with Support for Partial Functions

William M. Farmer, Joshua D. Guttman

2000

Abstract

Partial functions can be easily represented in set theory as certain
sets of ordered pairs.  However, classical set theory provides no
special machinery for reasoning about partial functions.  For
instance, there is no direct way of handling the application of a
function to an argument outside its domain as in partial logic.  There
is also no utilization of lambda-notation and sorts or types as in
type theory.  This paper introduces a version of
von-Neumann-Bernays-Goedel set theory for reasoning about sets, proper
classes, and partial functions represented as classes of ordered
pairs.  The underlying logic of the system is a partial first-order
logic, so class-valued terms may be nondenoting.  Functions can be
specified using lambda-notation, and reasoning about the application
of functions to arguments is facilitated using sorts similar to those
employed in the logic of the IMPS Interactive Mathematical Proof
System.  The set theory is intended to serve as a foundation for
mechanized mathematics systems.

Keywords: Set theory, NBG, mechanized mathematics, theorem
proving systems, partial functions, undefinedness, sorts.