Skip to main content
SpringerLink
Log in

Formalizing basic first order model theory

  • Refereed Papers
  • Conference paper
  • First Online:
Book cover Theorem Proving in Higher Order Logics (TPHOLs 1998)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1479))

Included in the following conference series:

Abstract

We define the syntax of unsorted first order logic as a HOL datatype and define the semantics of terms and formulas, and hence notions such as validity and satisfiability. We prove formally in HOL some elementary metatheorems such as Compactness, Löwenheim-Skolem and Uniformity, via canonical term models. The proofs are based on those in Kreisel and Krivine's book on model theory, but the HOL formalization raises several interesting issues. Because of the limited nature of type quantification in HOL, many of the theorems are awkward to state or prove in their standard form. Moreover, simple and elegant though the proofs seem, there are surprising difficulties formalizing Skolemization, one of the more intuitively obvious parts. On the other hand, we significantly improve on the original textbook versions of the arguments, proving two of the main theorems together rather than by separate arguments.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. N. G. de Bruijn. Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem. Indagationes Mathematicae, 34, 381–392, 1972.

    Google Scholar 

  2. H. B. Enderton. A Mathematical Introduction to Logic. Academic Press, 1972.

    Google Scholar 

  3. A. D. Gordon and T. Melham. Five axioms of alpha-conversion. In J. von Wright, J. Grundy, and J. Harrison (eds.), Theorem Proving in Higher Order Logics: 9th International Conference, TPHOLs'96, Volume 1125 of Lecture Notes in Computer Science, Turku, Finland, pp. 173–190. Springer-Verlag, 1996.

    Google Scholar 

  4. M. J. C. Gordon and T. F. Melham. Introduction to HOL: A theorem proving environment for higher order logic. Cambridge University Press, 1993.

    Google Scholar 

  5. P. T. Johnstone. Notes on Logic and Set Theory. Cambridge University Press, 1987.

    Google Scholar 

  6. G. Kreisel and J.-L. Krivine. Elements of mathematical logic: model theory (Revised second ed.). Studies in Logic and the Foundations of Mathematics. North-Holland, 1971. First edition 1967. Translation of the French ‘Eléments de logique mathématique, théorie des modeles’ published by Dunod, Paris in 1964.

    Google Scholar 

  7. T. F. Melham. The HOL logic extended with quantification over type variables. In L. J. M. Claesen. and M. J. C. Gordon. (eds.), Proceedings of the IFIP TC10/WG10.2 International Workshop on Higher Order Logic Theorem Proving and its Applications, Volume A-20 of IFIP Transactions A: Computer Science and Technology, IMEC, Leuven, Belgium, pp. 3–18. North-Holland, 1992.

    Google Scholar 

  8. H. Persson. Constructive Completeness of Intuitionistic Predicate Logic: A Formalisation in Type Theory. Licentiate thesis, Department of Computing Science, Chalmers University of Technology and University of Göteborg, Sweden, 1996.

    Google Scholar 

  9. R. Pollack. The theory of LEGO: A Proof Checker for the Extended Calculus of Constructions. Ph. D. thesis, University of Edinburgh, 1994.

    Google Scholar 

  10. D. Prawitz. Natural deduction; a proof-theoretical study, Volume 3 of Stockholm Studies in Philosophy. Almqvist and Wiksells, 1965.

    Google Scholar 

  11. P. Rudnicki. An overview of the MIZAR project, 1992. Available by anonymous FTP from menaik.cs.ualberta.ca as pub/Mizar/Mizar_Over.tar.Z.

    Google Scholar 

  12. S. Shapiro. Foundations without Foundationalism: A case for second-order logic. Number 17 in Oxford Logic Guides. Clarendon Press, 1991.

    Google Scholar 

  13. A. Stoughton. Substitution revisited. Theoretical Computer Science, 17, 317–325, 1988.

    Article  MathSciNet  Google Scholar 

  14. A. Trybulec. The Mizar-QC/6000 logic information language. ALLC Bulletin (Association for Literary and Linguistic Computing), 6, 136–140, 1978.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Intel Corporation, EY2-03 5200 NE Elam Young Parkway, 97124, Hillsboro, OR, USA

    John Harrison

Authors
  1. John Harrison
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Jim Grundy Malcolm Newey

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Harrison, J. (1998). Formalizing basic first order model theory. In: Grundy, J., Newey, M. (eds) Theorem Proving in Higher Order Logics. TPHOLs 1998. Lecture Notes in Computer Science, vol 1479. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055135

Download citation

  • DOI: https://doi.org/10.1007/BFb0055135

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-64987-8

  • Online ISBN: 978-3-540-49801-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation