A set theory with support for partial functions
Studia Logica 66 (1):59-78 (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-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 | No keywords specified (fix it) | |||||||||
| Categories | ||||||||||
| Options |
|
|||||||||
Download options| PhilPapers Archive |
Upload a copy of this paper Check publisher's policy on self-archival Papers currently archived: 5,701 |
| External links |
 |
| Through your library | Configure |
Similar books and articlesJeanleah Mohrherr (1983). Kleene Index Sets and Functional M-Degrees. Journal of Symbolic Logic 48 (3):829-840.
Michael Rathjen (1992). A Proof-Theoretic Characterization of the Primitive Recursive Set Functions. Journal of Symbolic Logic 57 (3):954-969.
Solomon Feferman (1995). Definedness. Erkenntnis 43 (3):295 - 320.
François Lepage (2000). Partial Monotonic Protothetics. Studia Logica 66 (1):147-163.
Silvio Ghilardi & Giancarlo Meloni (1996). Relational and Partial Variable Sets and Basic Predicate Logic. Journal of Symbolic Logic 61 (3):843-872.
Robert E. Byerly (1982). An Invariance Notion in Recursion Theory. Journal of Symbolic Logic 47 (1):48-66.
William M. Farmer (1990). A Partial Functions Version of Church's Simple Theory of Types. Journal of Symbolic Logic 55 (3):1269-1291.
William M. Farmer (1995). Reasoning About Partial Functions with the Aid of a Computer. Erkenntnis 43 (3):279 - 294.
Analytics
Monthly downloads
Sorry, there are not enough data points to plot this chart.
|
Added to index2009-01-28Total downloads2 ( #232,575 of 549,126 )Recent downloads (6 months)0How can I increase my downloads? |
My notes
Discussion
