Abstract
The purpose of this paper is to describe a “grand logic”, that is, a system of higher order logic capable of use as a general purpose foundation for mathematics. This logic has developed as the logic of a theorem proving system which has had a number of names in its career (EFTTP, Mark2, and currently Watson), and the suitability of this logic for computer-assisted formal proof is an aspect which will be considered, though not thoroughly. A distinguishing feature of this system is its relationship to Quine’s set theory NF and related untyped λ-calculi studied by the author.
The author gratefully acknowledges the support of US Army Research Office grant DAAG55-98-1-0263
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
A. Church. A formulation of the simple theory of types. Journal of Symbolic Logic, 5, 1940.
N. deBruijn, “Lambda-calculus with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem”, in Nederpelt, et. al., eds., Selected Papers on Automath, North Holland, 1994.
M. Gordon. A proof generating system for higher-order logic. Technical Report 103, University of Cambridge Computer Laboratory, January 1987.
M. Randall Holmes, “A functional formulation of first-order logic ‘with infinity’ without bound variables”, preprint, available at the Watson web page http://math.boisestate.edu/~holmes/proverpage.html
M. Randall Holmes, “Systems of combinatory logic related to Quine’s ‘New Foundations’”, Annals of Pure and Applied Logic, 53 (1991), pp. 103–33.
M. Randall Holmes, “Untyped λ-calculus with relative typing”, in Typed Lambda-Calculi and Applications (proceedings of TLCA’ 95), Springer, 1995, pp. 235–48.
M. Randall Holmes, Elementary Set Theory with a Universal Set, Academia-Bruylant, Louvain-la-Neuve, 1998.
M. Randall Holmes, “The Watson Theorem Prover”, preprint, available as part of the online documentation at the Watson web page http://math.boisestate.edu/~holmes/proverpage.html
Ronald Bjorn Jensen, “On the consistency of a slight (?) modification of Quine’s ‘New Foundations’”, Synthese, 19 (1969), pp. 250–63.
W. V. O. Quine, “New Foundations for Mathematical Logic”, American Mathematical Monthly, 44 (1937), pp. 70–80.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Randall Holmes, M. (2000). A Strong and Mechanizable Grand Logic. In: Aagaard, M., Harrison, J. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2000. Lecture Notes in Computer Science, vol 1869. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44659-1_18
Download citation
DOI: https://doi.org/10.1007/3-540-44659-1_18
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67863-2
Online ISBN: 978-3-540-44659-0
eBook Packages: Springer Book Archive