{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,3]],"date-time":"2025-06-03T14:02:49Z","timestamp":1748959369741},"reference-count":12,"publisher":"Cambridge University Press (CUP)","issue":"3","license":[{"start":{"date-parts":[[2014,3,12]],"date-time":"2014-03-12T00:00:00Z","timestamp":1394582400000},"content-version":"unspecified","delay-in-days":4940,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["J. symb. log."],"published-print":{"date-parts":[[2000,9]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>Using recent results in topos theory, two systems of higher-order logic are shown to be complete with respect to sheaf models over topological spaces\u2014so-called \u201ctopological semantics\u201d. The first is classical higher-order logic, with relational quantification of finitely high type; the second system is a predicative fragment thereof with quantification over functions between types, but not over arbitrary relations. The second theorem applies to intuitionistic as well as classical logic.<\/jats:p>","DOI":"10.2307\/2586693","type":"journal-article","created":{"date-parts":[[2006,5,6]],"date-time":"2006-05-06T18:02:41Z","timestamp":1146938561000},"page":"1168-1182","source":"Crossref","is-referenced-by-count":4,"title":["Topological completeness for higher-order logic"],"prefix":"10.1017","volume":"65","author":[{"given":"S.","family":"Awodey","sequence":"first","affiliation":[]},{"given":"C.","family":"Butz","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2014,3,12]]},"reference":[{"key":"S0022481200011841_ref012","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0927-0"},{"key":"S0022481200011841_ref002","first-page":"21","volume-title":"Report CMU-PHIL-85","author":"Awodey","year":"1998"},{"key":"S0022481200011841_ref008","first-page":"302\u2013401","volume-title":"Applications of sheaves","volume":"753","author":"Fourman","year":"1977"},{"key":"S0022481200011841_ref001","unstructured":"Awodey S. , Logic in topoi: Functorial semantics for higher-order logic, Ph.D. thesis , The University of Chicago, 1997."},{"key":"S0022481200011841_ref003","doi-asserted-by":"publisher","DOI":"10.1016\/0022-4049(80)90080-8"},{"key":"S0022481200011841_ref004","first-page":"6\u201316","volume":"46","author":"Boileau","year":"1981","journal-title":"La logique des topos"},{"key":"S0022481200011841_ref005","unstructured":"Butz C. , Logical and cohomological aspects of the space ofpoints of a topos, Ph.D. thesis , Universiteit Utrecht, 1996."},{"key":"S0022481200011841_ref006","first-page":"17","volume-title":"Preprint 973","author":"Butz","year":"1996"},{"key":"S0022481200011841_ref007","first-page":"56\u201368","volume":"5","author":"Church","year":"1940","journal-title":"A foundation for the simple theory of types"},{"key":"S0022481200011841_ref009","first-page":"81\u201391","volume":"15","author":"Henkin","year":"1950","journal-title":"Completeness in the theory of types"},{"key":"S0022481200011841_ref010","doi-asserted-by":"publisher","DOI":"10.1016\/0001-8708(90)90013-D"},{"key":"S0022481200011841_ref011","volume-title":"Introduction to higher-order categorical logic","author":"Lambek","year":"1986"}],"container-title":["Journal of Symbolic Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0022481200011841","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2019,5,8]],"date-time":"2019-05-08T20:47:50Z","timestamp":1557348470000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0022481200011841\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2000,9]]},"references-count":12,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2000,9]]}},"alternative-id":["S0022481200011841"],"URL":"https:\/\/doi.org\/10.2307\/2586693","relation":{},"ISSN":["0022-4812","1943-5886"],"issn-type":[{"value":"0022-4812","type":"print"},{"value":"1943-5886","type":"electronic"}],"subject":[],"published":{"date-parts":[[2000,9]]}}}