{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,6]],"date-time":"2026-06-06T00:55:45Z","timestamp":1780707345052,"version":"3.54.1"},"reference-count":58,"publisher":"Cambridge University Press (CUP)","issue":"4","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":3388,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2004,12]]},"abstract":"<jats:title>Abstract.<\/jats:title><jats:p>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.<\/jats:p>","DOI":"10.2178\/jsl\/1102022211","type":"journal-article","created":{"date-parts":[[2005,3,2]],"date-time":"2005-03-02T21:48:42Z","timestamp":1109800122000},"page":"1027-1088","source":"Crossref","is-referenced-by-count":63,"title":["Higher-order semantics and extensionality"],"prefix":"10.1017","volume":"69","author":[{"given":"Christoph","family":"Benzm\u00fcller","sequence":"first","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Chad E.","family":"Brown","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Michael","family":"Kohlhase","sequence":"additional","affiliation":[],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200007398_ref029","first-page":"7\u201355","article-title":"Form and content in quantification theory","volume":"8","author":"Hintikka","year":"1955","journal-title":"Acta Philosophica Fennica"},{"key":"S0022481200007398_ref027","doi-asserted-by":"publisher","DOI":"10.2307\/421107"},{"key":"S0022481200007398_ref025","volume-title":"Introduction to HOL\u2014a theorem proving environment for higher order logic","author":"Gordon","year":"1993"},{"key":"S0022481200007398_ref023","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-010-0411-4"},{"key":"S0022481200007398_ref020","unstructured":"Demarco Mary , Intuitionistic semantics for heriditarily harrop logic programming, Ph.D. thesis , Wesleyan University, 1999."},{"key":"S0022481200007398_ref018","first-page":"56\u201368","volume":"5","author":"Church","year":"1940","journal-title":"A formulation of the simple theory of types"},{"key":"S0022481200007398_ref012","unstructured":"Benzm\u00fcller 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."},{"key":"S0022481200007398_ref015","volume-title":"SEKI-Report SR-97-09","author":"Benzm\u00fcller","year":"1997"},{"key":"S0022481200007398_ref009","volume-title":"The lambda calculus","author":"Barendregt","year":"1984"},{"key":"S0022481200007398_ref003","first-page":"385\u2013394","volume":"37","author":"Andrews","year":"1972","journal-title":"General models descriptions and choice in type theory"},{"key":"S0022481200007398_ref002","first-page":"395\u2013397","volume":"37","author":"Andrews","year":"1972","journal-title":"General models and extensionality"},{"key":"S0022481200007398_ref001","first-page":"414\u2013432","volume":"36","author":"Andrews","year":"1971","journal-title":"Resolution in type theory"},{"key":"S0022481200007398_ref031","first-page":"546\u2013561","volume-title":"Proceedings of computer science logic","volume":"1683","author":"Honsell","year":"1999"},{"key":"S0022481200007398_ref033","first-page":"139\u2013146","volume-title":"Proceedings of the 3rd international joint conference on artificial intelligence","author":"Huet","year":"1973"},{"key":"S0022481200007398_ref037","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-59338-1_43"},{"key":"S0022481200007398_ref005","doi-asserted-by":"publisher","DOI":"10.1007\/BF00248320"},{"key":"S0022481200007398_ref058","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(93)00130-W"},{"key":"S0022481200007398_ref016","volume-title":"Automated deduction\u2014a basis for applications","author":"Bibel","year":"1998"},{"key":"S0022481200007398_ref030","doi-asserted-by":"publisher","DOI":"10.1017\/S096012959900287X"},{"key":"S0022481200007398_ref004","unstructured":"Andrews Peter B. , letter to Roger Hindley dated 01 22, 1973."},{"key":"S0022481200007398_ref010","unstructured":"Benzm\u00fcller Christoph , Equality and extensionality in automated higher-order theorem proving, Ph.D. thesis , Saarland University, 1999."},{"key":"S0022481200007398_ref032","unstructured":"Huet G\u00e9rard P. , Constrained resolution: A complete method for higher order logic, Ph. D. thesis , Case Western Reserve University, 1972."},{"key":"S0022481200007398_ref038","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.1999.10510980"},{"key":"S0022481200007398_ref017","doi-asserted-by":"publisher","DOI":"10.1007\/BF00632905"},{"key":"S0022481200007398_ref021","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129500003236"},{"key":"S0022481200007398_ref040","unstructured":"Lappin Shalom and Pollard Carl , A higher-order fine-grained logic for intensional semantics, manuscript, 2002."},{"key":"S0022481200007398_ref007","first-page":"164\u2013169","volume-title":"Proceedings of the 17th international conference on automated deduction","author":"Andrews","year":"2000"},{"key":"S0022481200007398_ref013","doi-asserted-by":"crossref","unstructured":"Benzm\u00fcller Christoph and Kohlhase Michael , Extensional higher order resolution, in Kirchner and Kirchner [35], pp. 56\u201372.","DOI":"10.1007\/BFb0054248"},{"key":"S0022481200007398_ref053","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-86718-7"},{"key":"S0022481200007398_ref024","first-page":"173\u2013198","article-title":"\u00dcber formal unentscheidbare S\u00e4tze der Principia Mathematica und verwandter Systeme I","volume":"38","author":"G\u00f6del","year":"1931","journal-title":"Monatshefte der Mathematischen Physik"},{"key":"S0022481200007398_ref006","doi-asserted-by":"publisher","DOI":"10.1007\/978-94-015-9934-4"},{"key":"S0022481200007398_ref028","volume-title":"Introduction to combinators and lambda-calculs","author":"Hindley","year":"1986"},{"key":"S0022481200007398_ref008","doi-asserted-by":"publisher","DOI":"10.1007\/BF00252180"},{"key":"S0022481200007398_ref019","first-page":"381\u2013392","article-title":"Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with an application to the Church-Rosser theorem","volume":"34","author":"de Bruijn","year":"1972","journal-title":"Indagationes Mathematicae"},{"key":"S0022481200007398_ref026","first-page":"81\u201391","volume":"15","author":"Henkin","year":"1950","journal-title":"Completeness in the theory of types"},{"key":"S0022481200007398_ref014","unstructured":"Benzm\u00fcller Christoph and Kohlhase Michael , LEO\u2014a higher order theorem prover, in Kirchner and Kirchner [35], pp. 139\u2013144."},{"key":"S0022481200007398_ref022","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-2360-3"},{"key":"S0022481200007398_ref045","volume-title":"Technical Report CS-1994-38","author":"Nadathur","year":"1994"},{"key":"S0022481200007398_ref034","first-page":"82\u201392","article-title":"A complete mechanization of(\u03c9)-order type theory","volume":"1","author":"Jensen","year":"1972","journal-title":"Proceedings of the ACM annual conference"},{"key":"S0022481200007398_ref035","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054239"},{"key":"S0022481200007398_ref039","volume-title":"Strategies for hyperintensional semantics","author":"Lappin","year":"2000"},{"key":"S0022481200007398_ref041","doi-asserted-by":"crossref","DOI":"10.7551\/mitpress\/4076.001.0001","volume-title":"Knowledge of meaning","author":"Larson","year":"1995"},{"key":"S0022481200007398_ref042","unstructured":"Miller Dale , Proofs in higher-order logic, Ph. D. thesis , Carnegie-Mellon University, 1983."},{"key":"S0022481200007398_ref047","volume-title":"Handbook of automated reasoning","author":"Robinson","year":"2001"},{"key":"S0022481200007398_ref048","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45719-4_8"},{"key":"S0022481200007398_ref049","doi-asserted-by":"crossref","unstructured":"Schr\u00f6der Lutz , Henkin models for the partial \u03bb-calculus, manuscript, http:\/\/www.informatik.uni-bremen.de\/~lschrode\/hascasl\/henkin.ps, 2002.","DOI":"10.1007\/978-3-540-45220-1_40"},{"key":"S0022481200007398_ref050","first-page":"305\u2013326","volume":"25","author":"Sch\u00fctte","year":"1960","journal-title":"Semantical and syntactical properties of simple type theory"},{"key":"S0022481200007398_ref051","first-page":"144\u2013149","volume-title":"Proceedings of the 18th international conference on automated deduction","volume":"2392","author":"Siekmann","year":"2002"},{"key":"S0022481200007398_ref043","first-page":"497\u2013536","article-title":"A logic programming language with lambda-abstraction, function variables, and simple unification","volume":"4","author":"Miller","year":"1991","journal-title":"Journal of Logic and Computation"},{"key":"S0022481200007398_ref052","doi-asserted-by":"publisher","DOI":"10.1073\/pnas.49.6.828"},{"key":"S0022481200007398_ref054","doi-asserted-by":"publisher","DOI":"10.2969\/jmsj\/01940399"},{"key":"S0022481200007398_ref056","first-page":"47\u201370","article-title":"A model theory for proposistional attitudes","volume":"4","author":"Tomason","year":"1980","journal-title":"Linguistics and Philosophy"},{"key":"S0022481200007398_ref057","volume-title":"From Frege to G\u00f6del: a source book in mathematical logic 1879\u20131931","author":"van Heijenoort","year":"1967"},{"key":"S0022481200007398_ref055","volume-title":"Proof theory","author":"Takeuti","year":"1987"},{"key":"S0022481200007398_ref011","first-page":"399\u2013413","volume-title":"Proceedings of the 16th international Conference on Automated Deduction","volume":"1632","author":"Benzm\u00fcller","year":"1999"},{"key":"S0022481200007398_ref044","volume-title":"Foundations for programming languages","author":"Mitchell","year":"1996"},{"key":"S0022481200007398_ref046","volume-title":"Isabelle\/HOL\u2014a proof assistant for higher-order logic","volume":"2283","author":"Nipkow","year":"2002"},{"key":"S0022481200007398_ref036","unstructured":"Kohlhase Michael , A mechanization of sorted higher-order logic based on the resolution principle, Ph. D. thesis , Saarland University, 1994."}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200007398","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,4,6]],"date-time":"2020-04-06T02:27:39Z","timestamp":1586140059000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200007398\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2004,12]]},"references-count":58,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2004,12]]}},"alternative-id":["S0022481200007398"],"URL":"https:\/\/doi.org\/10.2178\/jsl\/1102022211","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2004,12]]}}}