Graduate studies at Western
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||set theory NBC mechanized mathematics theorem proving systems partial functions undefinedness sorts|
|Categories||categorize this paper)|
|Through your library||Configure|
Similar books and articles
Jeanleah 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.
Added to index2009-01-28
Total downloads2 ( #246,859 of 739,517 )
Recent downloads (6 months)0
How can I increase my downloads?