David Bourget (Western Ontario)
David Chalmers (ANU, NYU)
Rafael De Clercq
Ezio Di Nucci
Jonathan Jenkins Ichikawa
Jack Alan Reynolds
Learn more about PhilPapers
Erkenntnis 43 (3):279 - 294 (1995)
Partial functions are ubiquitous in both mathematics and computer science. Therefore, it is imperative that the underlying logical formalism for a general-purpose mechanized mathematics system provide strong support for reasoning about partial functions. Unfortunately, the common logical formalisms — first-order logic, type theory, and set theory — are usually only adequate for reasoning about partial functionsin theory. However, the approach to partial functions traditionally employed by mathematicians is quite adequatein practice. This paper shows how the traditional approach to partial functions can be formalized in a range of formalisms that includes first-order logic, simple type theory, and Von-Neumann—Bernays—Gödel set theory. It argues that these new formalisms allow one to directly reason about partial functions; are based on natural, well-understood, familiar principles; and can be effectively implemented in mechanized mathematics systems.
|Keywords||No keywords specified (fix it)|
|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
Elliott Mendelson (1964). Introduction to Mathematical Logic. Princeton, N.J.,Van Nostrand.
Alonzo Church (1940). A Formulation of the Simple Theory of Types. Journal of Symbolic Logic 5 (2):56-68.
Timothy Smiley (1960). Sense Without Denotation. Analysis 20 (6):125 - 135.
Joseph R. Shoenfield (1954). A Relative Consistency Proof. Journal of Symbolic Logic 19 (1):21-28.
Hugues Leblanc & Theodore Hailperin (1959). Nondesignating Singular Terms. Philosophical Review 68 (2):239-243.
Citations of this work BETA
Raymond D. Gumb (2002). The Lazy Logic of Partial Terms. Journal of Symbolic Logic 67 (3):1065-1077.
Similar books and articles
G. Longo & E. Moggi (1984). The Hereditary Partial Effective Functionals and Recursion Theory in Higher Types. Journal of Symbolic Logic 49 (4):1319-1332.
François Lepage (2000). Partial Monotonic Protothetics. Studia Logica 66 (1):147-163.
Solomon Feferman (1995). Definedness. Erkenntnis 43 (3):295 - 320.
Robert Boyer, The Addition of Bounded Quantification and Partial Functions to a Computational Logic and its Theorem Prover.
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 & Joshua D. Guttman (2000). A Set Theory with Support for Partial Functions. Studia Logica 66 (1):59-78.
Added to index2009-01-28
Total downloads16 ( #250,352 of 1,938,583 )
Recent downloads (6 months)1 ( #452,035 of 1,938,583 )
How can I increase my downloads?