David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Jack Alan Reynolds
Learn more about PhilPapers
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)|
Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
|Through your library|
References found in this work BETA
No references found.
Citations of this work BETA
No citations found.
Similar books and articles
William M. Farmer (1990). A Partial Functions Version of Church's Simple Theory of Types. Journal of Symbolic Logic 55 (3):1269-1291.
Robert E. Byerly (1982). An Invariance Notion in Recursion Theory. Journal of Symbolic Logic 47 (1):48-66.
Silvio Ghilardi & Giancarlo Meloni (1996). Relational and Partial Variable Sets and Basic Predicate Logic. Journal of Symbolic Logic 61 (3):843-872.
François Lepage (2000). Partial Monotonic Protothetics. Studia Logica 66 (1):147-163.
Solomon Feferman (1995). Definedness. Erkenntnis 43 (3):295 - 320.
Michael Rathjen (1992). A Proof-Theoretic Characterization of the Primitive Recursive Set Functions. Journal of Symbolic Logic 57 (3):954-969.
Jeanleah Mohrherr (1983). Kleene Index Sets and Functional M-Degrees. Journal of Symbolic Logic 48 (3):829-840.
William M. Farmer (1995). Reasoning About Partial Functions with the Aid of a Computer. Erkenntnis 43 (3):279 - 294.
Added to index2009-01-28
Total downloads18 ( #132,725 of 1,696,592 )
Recent downloads (6 months)6 ( #94,197 of 1,696,592 )
How can I increase my downloads?