Abstract
We consider the EFO fragment of simple type theory, which restricts quantification and equality to base types but retains lambda abstractions and higher-order variables. We show that this fragment enjoys the characteristic properties of first-order logic: complete proof systems, compactness, and countable models. We obtain these results with an analytic tableau system and a concomitant model existence lemma. All results are with respect to standard models. The tableau system is well-suited for proof search and yields decision procedures for substantial fragments of EFO.
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
Andrews, P.B.: Classical type theory. In: Robinson, A., Voronkov, A. (eds.) Handbook of Automated Reasoning, vol. 2, pp. 965–1007. Elsevier Science, Amsterdam (2001)
Brown, C.E.: Automated Reasoning in Higher-Order Logic: Set Comprehension and Extensionality in Church’s Type Theory. College Publications (2007)
Börger, E., Grädel, E., Gurevich, Y.: The Classical Decision Problem. Springer, Heidelberg (1997)
Smullyan, R.M.: First-Order Logic. Springer, Heidelberg (1968)
Fitting, M.: First-Order Logic and Automated Theorem Proving. Springer, Heidelberg (1996)
Prawitz, D.: Hauptsatz for higher order logic. J. Symb. Log. 33, 452–457 (1968)
Brown, C.E., Smolka, G.: Terminating tableaux for the basic fragment of simple type theory. In: Giese, M., Waaler, A. (eds.) TABLEAUX 2009. LNCS (LNAI), vol. 5607, pp. 138–151. Springer, Heidelberg (2009)
Hindley, J.R.: Basic Simple Type Theory. Cambridge Tracts in Theoretical Computer Science, vol. 42. Cambridge University Press, Cambridge (1997)
Friedman, H.: Equality between functionals. In: Parikh, R. (ed.) Proc. Logic Colloquium 1972-73. Lectures Notes in Mathematics, vol. 453, pp. 22–37. Springer, Heidelberg (1975)
Statman, R.: Completeness, invariance and lambda-definability. J. Symb. Log. 47(1), 17–26 (1982)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2009 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Brown, C.E., Smolka, G. (2009). Extended First-Order Logic. In: Berghofer, S., Nipkow, T., Urban, C., Wenzel, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 2009. Lecture Notes in Computer Science, vol 5674. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-03359-9_13
Download citation
DOI: https://doi.org/10.1007/978-3-642-03359-9_13
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-03358-2
Online ISBN: 978-3-642-03359-9
eBook Packages: Computer ScienceComputer Science (R0)