{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,10]],"date-time":"2025-10-10T02:01:37Z","timestamp":1760061697159},"reference-count":6,"publisher":"Wiley","issue":"1","license":[{"start":{"date-parts":[[2006,11,13]],"date-time":"2006-11-13T00:00:00Z","timestamp":1163376000000},"content-version":"vor","delay-in-days":5064,"URL":"http:\/\/onlinelibrary.wiley.com\/termsAndConditions#vor"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Mathematical Logic Qtrly"],"published-print":{"date-parts":[[1993,1]]},"abstract":"<jats:title>Abstract<\/jats:title><jats:p>We investigate Hilbert's \u03f5\u2010calculus in the context of intuitionistic type theories, that is, within certain systems of intuitionistic higher\u2010order logic. We determine the additional deductive strength conferred on an intuitionistic type theory by the adjunction of closed \u03f5\u2010terms. We extend the usual topos semantics for type theories to the \u03f5\u2010operator and prove a completeness theorem. The paper also contains a discussion of the concept of \u201cpartially defined\u201d \u03f5\u2010term. MSC: 03B15, 03B20, 03G30.<\/jats:p>","DOI":"10.1002\/malq.19930390137","type":"journal-article","created":{"date-parts":[[2007,6,3]],"date-time":"2007-06-03T01:49:49Z","timestamp":1180835389000},"page":"323-337","source":"Crossref","is-referenced-by-count":15,"title":["Hilbert's \u03f5\u2010operator in intuitionistic type theories"],"prefix":"10.1002","volume":"39","author":[{"given":"John L.","family":"Bell","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"311","published-online":{"date-parts":[[2006,11,13]]},"reference":[{"key":"e_1_2_1_2_2","doi-asserted-by":"publisher","DOI":"10.1002\/malq.19570030104"},{"key":"e_1_2_1_3_2","volume-title":"Toposes and Local Set Theories: An Introduction","author":"Bell J. L.","year":"1988"},{"key":"e_1_2_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01049178"},{"key":"e_1_2_1_5_2","volume-title":"Topos Theory","author":"Johnstone P. T.","year":"1977"},{"key":"e_1_2_1_6_2","first-page":"36","volume-title":"Categorical Topology and its Relation to Analysis, Algebra and Combinatorics","author":"Lambek J.","year":"1989"},{"key":"e_1_2_1_7_2","volume-title":"Mathematical Logic and Hilbert's \u03b5\u2010symbol","author":"Leisenring A. C.","year":"1969"}],"container-title":["Mathematical Logic Quarterly"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/api.wiley.com\/onlinelibrary\/tdm\/v1\/articles\/10.1002%2Fmalq.19930390137","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/pdf\/10.1002\/malq.19930390137","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,10,25]],"date-time":"2023-10-25T21:00:58Z","timestamp":1698267658000},"score":1,"resource":{"primary":{"URL":"https:\/\/onlinelibrary.wiley.com\/doi\/10.1002\/malq.19930390137"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[1993,1]]},"references-count":6,"journal-issue":{"issue":"1","published-print":{"date-parts":[[1993,1]]}},"alternative-id":["10.1002\/malq.19930390137"],"URL":"https:\/\/doi.org\/10.1002\/malq.19930390137","archive":["Portico"],"relation":{},"ISSN":["0942-5616","1521-3870"],"issn-type":[{"value":"0942-5616","type":"print"},{"value":"1521-3870","type":"electronic"}],"subject":[],"published":{"date-parts":[[1993,1]]}}}