Hostname: page-component-745bb68f8f-s22k5 Total loading time: 0 Render date: 2025-02-09T18:04:14.797Z Has data issue: false hasContentIssue false
  • English
  • Français

Higher-order semantics and extensionality

Published online by Cambridge University Press:  12 March 2014

Christoph Benzmüller ,
Chad E. Brown  and
Michael Kohlhase
Christoph Benzmüller
Affiliation:
Department of Computer Science, Saarland University, Saarbrücken, Germany, E-mail: [email protected], URL: http://www.ags.uni-sb.de/~chris
Chad E. Brown
Affiliation:
Department of Mathematics, Carnegie Mellon University, Pittsburgh, PA 15213, USA, E-mail: [email protected], URL: http://www.andrew.cmu.edu/~cebrown/
Michael Kohlhase
Affiliation:
School of Engineering and Sciences, International University Bremen, Bremen, Germany School of Computer Science, Carnegie Mellon University, Pittsburgh, USA, E-mail: [email protected], URL: http://www.cs.cmu.edu/~kohlhase
Get access Rights & Permissions [Opens in a new window]

Abstract.

In this paper we re-examine the semantics of classical higher-order logic with the purpose of clarifying the role of extensionality. To reach this goal, we distinguish nine classes of higher-order models with respect to various combinations of Boolean extensionality and three forms of functional extensionality. Furthermore, we develop a methodology of abstract consistency methods (by providing the necessary model existence theorems) needed to analyze completeness of (machine-oriented) higher-order calculi with respect to these model classes.

Type
Research Article
Information
The Journal of Symbolic Logic , Volume 69 , Issue 4 , December 2004 , pp. 1027 - 1088
Copyright
Copyright © Association for Symbolic Logic 2004

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1]Andrews, Peter B., Resolution in type theory, this Journal, vol. 36 (1971), no. 3, pp. 414–432.Google Scholar
[2]Andrews, Peter B., General models and extensionality, this Journal, vol. 37 (1972), no. 2, pp. 395–397.Google Scholar
[3]Andrews, Peter B., General models descriptions and choice in type theory, this Journal, vol. 37 (1972), no. 2, pp. 385–394.Google Scholar
[4]Andrews, Peter B., letter to Roger Hindley dated 01 22, 1973.Google Scholar
[5]Andrews, Peter B., On connections and higher order logic, Journal of Automated Reasoning, vol. 5 (1989), pp. 257–291.CrossRefGoogle Scholar
[6]Andrews, Peter B., An introduction to mathematical logic and type theory: To truth through proof, second ed., Kluwer Academic Publishers, 2002.CrossRefGoogle Scholar
[7]Andrews, Peter B., Bishop, Matthew, and Brown, Chad E., TPS: A theorem proving system for type theory, Proceedings of the 17th international conference on automated deduction (Pittsburgh, USA) (McAllester, David, editor), Lecture Notes in Artifical Intelligence, no. 1831. Springer-Verlag, 2000, pp. 164–169.Google Scholar
[8]Andrews, Peter B., Bishop, Matthew, Issar, Sunil, Nesmith, Dan, Pfenning, Frank, and Xi, Hongwei, TPS: A theorem proving system for classical type theory, Journal of Automated Reasoning, vol. 16 (1996), no. 3, pp. 321–353.CrossRefGoogle Scholar
[9]Barendregt, Henk P., The lambda calculus, North-Holland, 1984.Google Scholar
[10]Benzmüller, Christoph, Equality and extensionality in automated higher-order theorem proving, Ph.D. thesis, Saarland University, 1999.Google Scholar
[11]Benzmüller, Christoph, Extensional higher-order paramodulation and RUE-resolution, Proceedings of the 16th international Conference on Automated Deduction (Trento, Italy) (Ganzinger, Harald, editor), Lecture Notes in Artificial Intelligence, vol. 1632, Springer-Verlag, 1999, pp. 399–413.Google Scholar
[12]Benzmüller, Christoph, Brown, Chad E., and Kohlhase, Michael, Semantic techniques for higher-order cut-elimination, manuscript, http://www.ags.uni-sb.de/~chris/papers/R19.pdf, 2002.Google Scholar
[13]Benzmüller, Christoph and Kohlhase, Michael, Extensional higher order resolution, in Kirchner and Kirchner [35], pp. 56–72.CrossRefGoogle Scholar
[14]Benzmüller, Christoph and Kohlhase, Michael, LEO—a higher order theorem prover, in Kirchner and Kirchner [35], pp. 139–144.Google Scholar
[15]Benzmüller, Christoph and Kohlhase, Michael, Model existence for higher-order logic, SEKI-Report SR-97-09, Saarland University, 1997.Google Scholar
[16]Bibel, Wolfgang and Schmitt, Peter (editors), Automated deduction—a basis for applications, Kluwer, 1998.Google Scholar
[17]Chierchia, Gennaro and Turner, Raymond, Semantics and property theory, Linguistics and Philosophy, vol. 11 (1988), pp. 261–302.CrossRefGoogle Scholar
[18]Church, Alonzo, A formulation of the simple theory of types, this Journal, vol. 5 (1940), pp. 56–68.Google Scholar
[19]de Bruijn, Nicolaas Govert, Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem, Indagationes Mathematicae, vol. 34 (1972), no. 5, pp. 381–392.Google Scholar
[20]Demarco, Mary, Intuitionistic semantics for heriditarily harrop logic programming, Ph.D. thesis, Wesleyan University, 1999.Google Scholar
[21]Dowek, Gilles, Hardin, ThéRèse, and Kirchner, Claude, HOL-λσ an intentional first-order expression of higher-order logic, Mathematical Structures in Computer Science, vol. 11 (2001), no. 1, pp. 1–25.CrossRefGoogle Scholar
[22]Fitting, Melvin, First-order logic and automated theorem proving, second ed., Graduate Texts in Computer Science, Springer-Verlag, 1996.CrossRefGoogle Scholar
[23]Fitting, Melvin, Types, tableaus, and Gödel's God, Kluwer, 2002.CrossRefGoogle Scholar
[24]Gödel, Kurt, Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I, Monatshefte der Mathematischen Physik, vol. 38 (1931), pp. 173–198, English version in [57].Google Scholar
[25]Gordon, M. J. C. and Melham, T. F., Introduction to HOL—a theorem proving environment for higher order logic, Cambridge University Press, 1993.Google Scholar
[26]Henkin, Leon, Completeness in the theory of types, this Journal, vol. 15 (1950), no. 2, pp. 81–91.Google Scholar
[27]Henkin, Leon, The discovery of my completeness proofs, The Bulletin of Symbolic Logic, vol. 2 (1996), no. 2, pp. 127–158.CrossRefGoogle Scholar
[28]Hindley, Roger J. and Seldin, Jonathan P., Introduction to combinators and lambda-calculs, Cambridge University Press, Cambridge, 1986.Google Scholar
[29]Hintikka, K. J. J., Form and content in quantification theory, Acta Philosophica Fennica, vol. 8 (1955), pp. 7–55.Google Scholar
[30]Honsell, Furio and Lenisa, Marina, Coinductive characterizations of applicative structures, Mathematical Structures in Computer Science, vol. 9 (1999), pp. 403–435.CrossRefGoogle Scholar
[31]Honsell, Furio and Sannella, Donald, Pre-logical relations, Proceedings of computer science logic (CSL ’99), Lecture Notes in Computer Science, vol. 1683, Springer-Verlag, 1999, pp. 546–561.Google Scholar
[32]Huet, Gérard P., Constrained resolution: A complete method for higher order logic, Ph. D. thesis, Case Western Reserve University, 1972.Google Scholar
[33]Huet, Gérard P., A mechanization of type theory, Proceedings of the 3rd international joint conference on artificial intelligence (Walker, Donald E. and Norton, Lewis, editors), 1973, pp. 139–146.Google Scholar
[34]Jensen, D. C. and Pietrzykowski, Thomasz, A complete mechanization of(ω)-order type theory, Proceedings of the ACM annual conference, vol. 1, 1972, pp. 82–92.Google Scholar
[35]Kirchner, Claude and Kirchner, Hélène (editors), Proceedings of the 15th Conference on Automated Deduction, Lecture Notes in Artificial Intelligence, vol. 1421, Springer-Verlag, 1998.CrossRefGoogle Scholar
[36]Kohlhase, Michael, A mechanization of sorted higher-order logic based on the resolution principle, Ph. D. thesis, Saarland University, 1994.Google Scholar
[37]Kohlhase, Michael, Higher-order tableaux, Theorem proving with analytic tableaux and related methods (Baumgartner, Peter, Hähnle, Reiner, and Posegga, Joachim, editors), Lecture Notes in Artificial Intelligence, vol. 918, Springer-Verlag, 1995, pp. 294–309.CrossRefGoogle Scholar
[38]Kohlhase, Michael and Scheja, Ortwin, Higher-order multi-valued resolution, Journal of Applied Non-Classical Logics, vol. 9 (1999), no. 4, pp. 155–178.CrossRefGoogle Scholar
[39]Lappin, Shalom and Pollard, Carl, Strategies for hyperintensional semantics, manuscript, King's College, London and Ohio State University, 2000.Google Scholar
[40]Lappin, Shalom and Pollard, Carl, A higher-order fine-grained logic for intensional semantics, manuscript, 2002.Google Scholar
[41]Larson, Richard and Segal, Gabriel, Knowledge of meaning, MIT Press, 1995.CrossRefGoogle Scholar
[42]Miller, Dale, Proofs in higher-order logic, Ph. D. thesis, Carnegie-Mellon University, 1983.Google Scholar
[43]Miller, Dale, A logic programming language with lambda-abstraction, function variables, and simple unification, Journal of Logic and Computation, vol. 4 (1991), no. 1, pp. 497–536.Google Scholar
[44]Mitchell, John C., Foundations for programming languages, Foundations of Computing, MIT Press, 1996.Google Scholar
[45]Nadathur, Gopalan and Miller, Dale, Higher-order logic programming, Technical Report CS-1994-38, Department of Computer Science, Duke University, 1994.Google Scholar
[46]Nipkow, Tobias, Paulson, Lawrence C., and Wenzel, Markus, Isabelle/HOL—a proof assistant for higher-order logic, Lecture Notes in Computer Science, vol. 2283, Springer-Verlag, 2002.Google Scholar
[47]Robinson, J. Alan and Voronkov, Andrei, Handbook of automated reasoning, MIT Press, 2001.Google Scholar
[48]Schröder, L. and Mossakowski, T., Hascasl: towards integrated specification and development of functional programs, Algebraic methodology and software technology, Lecture Notes in Computer Science, vol. 2422, Springer-Verlag, 2002, pp. 99–116.CrossRefGoogle Scholar
[49]Schröder, Lutz, Henkin models for the partial λ-calculus, manuscript, http://www.informatik.uni-bremen.de/~lschrode/hascasl/henkin.ps, 2002.CrossRefGoogle Scholar
[50]Schütte, Kurt, Semantical and syntactical properties of simple type theory, this Journal, vol. 25 (1960), pp. 305–326.Google Scholar
[51]Siekmann, Jörg, Benzmüller, Christoph, et al., Proof development with OMEGA, Proceedings of the 18th international conference on automated deduction (Copenhagen, Denmark) (Voronkov, Andrei, editor), Lecture Notes in Artificial Intelligence, vol. 2392, Springer-Verlag, 2002, pp. 144–149.Google Scholar
[52]Smullyan, Raymond M., A unifying principle for quantification theory, Proceedings of the National Academy of Sciences, vol. 49 (1963), pp. 828–832.CrossRefGoogle Scholar
[53]Smullyan, Raymond M., First-order logic, Springer-Verlag, 1968.CrossRefGoogle Scholar
[54]Takahashi, Moto-o, Cut-elimination in simple type theory with extensionality, Journal of the Mathematical Society of Japan, vol. 19 (1967), pp. 399–410.CrossRefGoogle Scholar
[55]Takeuti, Gaisi, Proof theory, North-Holland, 1987.Google Scholar
[56]Tomason, R., A model theory for proposistional attitudes, Linguistics and Philosophy, vol. 4 (1980), pp. 47–70.Google Scholar
[57]van Heijenoort, Jean, From Frege to Gödel: a source book in mathematical logic 1879–1931, 3rd printing, 1997 ed., Source books in the history of the sciences series, Harvard University Press, Cambridge, MA, 1967.Google Scholar
[58]Wolfram, David A., A semantics for λ-PROLOG, Theoretical Computer Science, vol. 136 (1994), no. 1, pp. 277–289.CrossRefGoogle Scholar