A set theory with support for partial functions

Studia Logica 66 (1):59-78 (2000)
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-Gödel 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  NBC  mechanized mathematics  theorem proving systems  partial functions  undefinedness  sorts
Categories (categorize this paper)
Reprint years 2004
DOI 10.1023/A:1026744827863
 Save to my reading list
Follow the author(s)
Edit this record
My bibliography
Export citation
Find it on Scholar
Mark as duplicate
Request removal from index
Revision history
Download options
Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 30,300
Through your library
References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles
Added to PP index

Total downloads
34 ( #155,467 of 2,193,260 )

Recent downloads (6 months)
1 ( #290,647 of 2,193,260 )

How can I increase my downloads?

Monthly downloads
My notes
Sign in to use this feature